第五章 函数式程序设计语言.ppt

第五章 函数式程序设计语言 过程式程序设计语言由于数据的名值分离， 变量的时空特性导致程序难于查错、难于修改 命令式语言天生带来的三个问题只解决了一半 滥用goto已经完全解决 悬挂指针没有完全解决 函数副作用不可能消除 问题是程序状态的易变性(Mutability)和顺序性(Sequencing) Backus在图灵奖的一篇演说《程序设计能从冯·诺依曼风格下解放出来吗？》中极力鼓吹发展与数学连系更密切的函数式程序设计语言 5.1 过程式语言存在的问题 （1）易变性难于数学模型 代数中的变量是未知的确定值，而程序设计语言的变量是对存储的抽象 根本解决： 能不能不要程序意义的“变量”只保留数学意义的“变量”？ 能不能消除函数的副作用？ （2）顺序性更难数学模型 顺序性影响计算结果， 例如， 前述急求值、正规求值、懒求值同一表达式就会有不同的结果。有副作用更甚， 因而难于为程序建立统一的符号数学理论。 应寻求与求值顺序无关的表达方式 理想的改变途径 没有变量， 就没有破坏性赋值， 也不会有引起副作用的全局量和局部量之分。 调用通过引用就没有意义。 循环也没有意义， 因为只有每次执行循环改变了控制变量的值， 循环才能得到不同的结果。 那么程序结构只剩下表达式、条件表达式、递归表达式。 5.2 λ演算 λ演算是符号的逻辑演算系统， 它正好只有这三种机制， 它就成为函数式程序设计语言的模型 λ演算是一个符号、逻辑系统，其公式就是符号串并按逻辑规则操纵 Church的理论证明， λ演算是个完备的系统， 可以表示任何计算函数， 所以任何可用λ演算仿真实现的语言也是完备的。 λ演算使函数概念形式化，是涉及变量、函数、函数组合规则的演算。 λ演算基于最简单的定义函数的思想： 一为函数抽象λx.E， 一为函数应用(λx.E)(a)。 一切变量、标识符、表达式都是函数或(复合)高阶函数。如λx.C(C为常量)是常函数。 5.2.1 术语和表示法 (1)λ演算有两类符号： 小写单字符用以命名参数， 也叫变量。 外加四个符号： ( 、) 、。、λ。 大写单字符、 特殊字符（如+、-、*、/）、大小写组成的标识符代替一个λ表达式。 （2）公式 变量是公式，如y。 如y是变量F是公式， 则λy.F也是公式。 如F和G都是公式， 则(FG)也是公式。 （3）λ表达式 形如λy.F为λ函数表达式， 以关键字λ开始， 变量y为参数。 形如(FG)为λ应用表达式 为了清晰，λ表达式可以任加成对括号。 λ演算公式举例 (4) 简略表示 形式语法 5.2.2 约束变量和自由变量 λ表达式中的作用域复盖 基本函数 TRUE 和FALSE的λ表达式 T = λx.λy.x F = λx.λy.y 整数的λ表达式： 0=λx.λy.y 1=λx.λy.x y 2=λx.λy.x(x y) n=λx.λy.x(x(…(x y)) n个 基本操作函数 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) 归约与范式 （1）β归约：β归约的表达式是一个λ应用表达式(λx.M N)， 其左边子表达式是λ函数表达式，右边是任意λ表达式。β归约以右边的λ表达式置换函数体M中λ指明的那个形参变量。形式地，我们用[N/X,M]表示对（λx.M N）的置换（规则略）。 关键的问题是注意函数体中要置换的变量是否自由出现，如： ((λx.x(λx.(xy)))(zz)) =(zz)(λx.((zz)y)) //错误，第二x个非自由出现。 =(zz)(λx.(xy)) //正确 例11-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