5章节 函数式程序设计语言.pptVIP

第5章 函数式程序设计语言;问题是程序状态的易变性(Mutability)和顺序性(Sequencing) Backus在图灵奖的一篇演说《程序设计能从冯·诺依曼风格下解放出来吗？》中极力鼓吹发展与数学连系更密切的函数式程序设计语言;5.1 过程式语言存在的问题;例：有副作用的函数 int sf_fun(int x) static int z = 0； //第一次装入赋初值 return x + (z++)； sf_fun(3) = {3 |4 | 5 | 6 | 7 …} //随调用次数而异，不是数学意义的确定函数。;（2）顺序性更难数学模型;5.2 λ演算;λ演算使函数概念形式化，是涉及变量、函数、函数组合规则的演算。 λ演算基于最简单的定义函数的思想： 一为函数抽象λx.E， 一为函数应用(λx.E)(a)。 一切变量、标识符、表达式都是函数或(复合)高阶函数。如λx.C(C为常量)是常函数。;λ演算公式举例;由于λ演算中一切语义概念均用λ表达式表达。 为了清晰采用命名替换使之更易读。 T = λx.λy.x //逻辑真值 F = λx.λy.y //逻辑假值 1 = λx.λy.x y //数1 2 = λx.λy.x(x y) //数2 zerop = λn.n(λx.F)T //判零函数 注：zerop中的F、T可以用λ表达式展开;形式语法;基本函数;基本操作函数 not=λz.((zF)T)=λz.((zλx.λy.y)(λx.λy.x)) and=λa.λb.((ab)F) = λa.λb.((ab)λx.λy.y)) or = λa.λb.((aT)b) = λa.λb.((a λx.λy.x)b);例：3+4就写add 3 4， add 3返回“加3函数”应用到4上当然就是7。写全了是： （λx.λy.λa.λb.((x a)(y a) b )） (λp.λq.(p(p(p q)))(λs.λt.(s(s(s(s t))) ?λa.λb.(a(a(a(a(a(a(a b)))))));归约与范式;（1）β归约：β归约的表达式是一个λ应用表达式(λx.M N)， 其左边子表达式是λ函数表达式，右边是任意λ表达式。β归约以右边的λ表达式置换函数体M中λ指明的那个形参变量。形式地，我们用[N/X,M]表示对（λx.M N）的置换（规则略）。 关键的问题是注意函数体中要置换的变量是否自由出现，如： ((λx.x(λx.(xy)))(zz)) =(zz)(λx.((zz)y)) //错误，第二x个非自由出现。 =(zz)(λx.(xy)) //正确 ;例5-5 高层表示的β归约;(2)η归约是消除一层约束的归约:λx.Fx = F (3)α换名:归约中如发生改变束定性质， 则允许换名(λ后跟的变量名)， 以保证原有束定关系。 例如： (λx. (λy.x)) (z y) //(zy)中y是自由变量 = λy.(zy) //此时(zy)中y被束定了， 错误！ = (λx.(λw.x))(zy) //因(λy.x)中函数体 无y， 可换名 = λw.(zy) // 正确！;(4)归约约定 顺序:每次归约只要找到可归约的子公式即可归约， λ演算没有规定顺序。 范式:符号归约当施行（除α规则外）所有变换规则后没有新形式出现，则这种λ表达式叫范式。 解释:范式即λ演算的语义解释， 形如 x x，(y (λx.z))就只能解释为数据了。 上述基本函数均为范式， 在它的上面取上有意义的名字可以构成上一层的函数， 如：pred =λn.(subtract n 1);（5） 综合规约例题：以λ演算规约3**2 3**2=**(3)(2) =λx.λy.(y x)(3)(2) β(λy.(y 3))(2) β((2)3) = (λf.λc.f ( f c ) ) (3) βλc.(( 3 ( 3 c ) ) = λc.(λf.λc.(f(f(f(c)))))(3 c)) // 有c不能置换c αλc.(λf.λz.(f (f (f (z)))))(3 c) βλc.(λz.((3 c)((3 c)((3 c)(z))))) // 再展3;=λc.λz.((( λf.λc.(f(f(f(c)))c)((3c)((3c)(z)))) αλc.λz.(((