北航研究生课程_程序语言设计原理教程_第11章

第11章函数式程序设计语言•过程式程序设计语言由于数据的名值分离，变量的时空特性导致程序难于查错、难于修改•命令式语言天生带来的三个问题只解决了一半•滥用goto已经完全解决•悬挂指针没有完全解决•函数副作用不可能消除•问题是程序状态的易变性(Mutability)和顺序性(Sequencing)•Backus在图灵奖的一篇演说《程序设计能从冯·诺依曼风格下解放出来吗？》中极力鼓吹发展与数学连系更密切的函数式程序设计语言11.1过程式语言存在的问题（1）易变性难于数学模型•代数中的变量是未知的确定值，而程序设计语言的变量是对存储的抽象•根本解决：能不能不要程序意义的“变量”只保留数学意义的“变量”？•能不能消除函数的副作用？例：有副作用的函数intsf_fun(intx)staticintz=0；//第一次装入赋初值returnx+(z++)；sf_fun(3)={3|4|5|6|7…}//随调用次数而异，不是数学意义的确定函数。（2）顺序性更难数学模型•顺序性影响计算结果，例如，前述急求值、正规求值、懒求值同一表达式就会有不同的结果。有副作用更甚，因而难于为程序建立统一的符号数学理论。•应寻求与求值顺序无关的表达方式•理想的改变途径•没有变量，就没有破坏性赋值，也不会有引起副作用的全局量和局部量之分。调用通过引用就没有意义。循环也没有意义，因为只有每次执行循环改变了控制变量的值，循环才能得到不同的结果。•那么程序结构只剩下表达式、条件表达式、递归表达式。λ演算•λ演算是符号的逻辑演算系统，它正好只有这三种机制，它就成为函数式程序设计语言的模型•λ演算是一个符号、逻辑系统，其公式就是符号串并按逻辑规则操纵•Church的理论证明，λ演算是个完备的系统，可以表示任何计算函数，所以任何可用λ演算仿真实现的语言也是完备的。•λ演算使函数概念形式化，是涉及变量、函数、函数组合规则的演算。•λ演算基于最简单的定义函数的思想：一为函数抽象λx.E，一为函数应用(λx.E)(a)。•一切变量、标识符、表达式都是函数或(复合)高阶函数。如λx.C(C为常量)是常函数。11.2.1术语和表示法(1)λ演算有两类符号：•小写单字符用以命名参数，也叫变量。•外加四个符号：(、)、。、λ。•大写单字符、特殊字符（如+、-、*、/）、大小写组成的标识符代替一个λ表达式。（2）公式•变量是公式，如y。•如y是变量F是公式，则λy.F也是公式。•如F和G都是公式，则(FG)也是公式。（3）λ表达式•形如λy.F为λ函数表达式，以关键字λ开始，变量y为参数。•形如(FG)为λ应用表达式•为了清晰，λ表达式可以任加成对括号。λ演算公式举例x变量、公式、表达式。(λx.((y)x))函数，体内嵌入应用。(λz.(y(λz.x)))函数，体内嵌入应用，再次嵌入函数。((λz.(zy))x)应用表达式。λx.λy.λz.(xλx.(uv)w)复杂表达式(4)简略表示•缩写与变形表达下例各表达均等效：λa.λb.λc.λz.E=λabcz.E=λ(abcz).E=λ(a，b，c，z).E=λa.(λb.(λc.(λz.E)))•命名:以大写单字符或标识符命名其λ表达式G=(λx.(y(yx)))((λx.(y(yx)))(λx.(y(yx))))=(GG)=H由于λ演算中一切语义概念均用λ表达式表达。为了清晰采用命名替换使之更易读。T=λx.λy.x//逻辑真值F=λx.λy.y//逻辑假值1=λx.λy.xy//数12=λx.λy.x(xy)//数2zerop=λn.n(λx.F)T//判零函数注：zerop中的F、T可以用λ表达式展开(5)形式语法核心的λ演算没有类型，没有顺序控制等概念，程序和数据没有区分。语法极简单：λ-表达式::=变量|λ变量.λ-表达式|(λ-表达式λ-表达式)|(λ-表达式)变量::=字母11.2.2约束变量和自由变量(λx.((bx)x))自由变量约束变量（λx.λy.(axy)(b(λy.(xy))))λ表达式中的作用域复盖（λx.(λx.(xa))(xb)(xc)）PMNROQ第1个x约束于P第2个x约束于O第3个x在M中自由，约束于O，P第4个x在N中自由，约束于P第5个x在R中自由，在Q中这5个x均约束出现,b，c自由出现。11.2.3基本函数•TRUE和FALSE的λ表达式T=λx.λy.xF=λx.λy.y•整数的λ表达式：0=λx.λy.y1=λx.λy.xy2=λx.λy.x(xy)n=λx.λy.x(x(…(xy))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)以下是算术操作函数举例：+=add=λx.λy.λa.λb.((xa)(ya)b)*=multiply=λx.λy.λa.((x(ya)))**=sqr=λx.λy.(yx)identity=λx.x//同一函数succ=λn.(λx.λy.nx(xy))//后继函数zerop=λn.n(λx.F)T=λn.n(λz.λx.λy.y)(λx.λy.y)//判零函数例：3+4就写add34，add3返回“加3函数”应用到4上当然就是7。写全了是：（λx.λy.λa.λb.((xa)(ya)b)）(λp.λq.(p(p(pq)))(λs.λt.(s(s(s(st)))λa.λb.(a(a(a(a(a(a(ab)))))))11.2.4归约与范式归约将复杂的表达式化成简单形式，即按一定的规则对符号表达式进行置换。例：归约数1的后继(succ1)=(λn.(λx.λy.nx(xy))1)=(λx.λy.1x(xy))=(λx.λy.(λp.λq.pq)x(xy))=(λx.λy.(λq.xq)(xy))=(λx.λy.x(xy))=2注：succ和1都是函数(1是常函数)，第一步是λn束定的n被1置换。展开后，x置换p，(xy)置换q，最后一行不能再置换了，它就是范式，语义为2。（1）β归约：β归约的表达式是一个λ应用表达式(λx.MN)，其左边子表达式是λ函数表达式，右边是任意λ表达式。β归约以右边的λ表达式置换函数体M中λ指明的那个形参变量。形式地，我们用[N/X,M]表示对（λx.MN）的置换（规则略）。关键的问题是注意函数体中要置换的变量是否自由出现，如：((λx.x(λx.(xy)))(zz))=(zz)(λx.((zz)y))//错误，第二x个非自由出现。=(zz)(λx.(xy))//正确例11-5高层表示的β归约•(λn.addnn)3=add33//3置换n后取消λn=6•(λf.λx.f(fx))succ7=λx.succ(succx)7=succ(succ7)=succ(8)=9注：add，3，succ，7，9是为了清晰没进一步展开为λ表达式。但β归约有时并不能简化，如：(λx.xx)(λx.xx)，归约后仍是原公式，这种λ表达式称为不可归约的。对应为程序设计语言中的无限递归。(2)η归约是消除一层约束的归约:λx.Fx=F(3)α换名:归约中如发生改变束定性质，则允许换名(λ后跟的变量名)，以保证原有束定关系。例如：(λx.(λy.x))(zy)//(zy)中y是自由变量=λy.(zy)//此时(zy)中y被束定了，错误！=(λx.(λw.x))(zy)//因(λy.x)中函数体无y，可换名=λw.(zy)//正确！(4)归约约定•顺序:每次归约只要找到可归约的子公式即可归约，λ演算没有规定顺序。•范式:符号归约当施行（除α规则外）所有变换规则后没有新形式出现，则这种λ表达式叫范式。•解释:范式即λ演算的语义解释，形如xx，(y(λx.z))就只能解释为数据了。上述基本函数均为范式，在它的上面取上有意义的名字可以构成上一层的函数，如：pred=λn.(subtractn1)（5）综合规约例题：以λ演算规约3**23**2=**(3)(2)=λx.λy.(yx)(3)(2)β(λy.(y3))(2)β((2)3)=(λf.λc.f(fc))(3)βλc.((3(3c))=λc.(λf.λc.(f(f(f(c)))))(3c))//有c不能置换cαλc.(λf.λz.(f(f(f(z)))))(3c)βλc.(λz.((3c)((3c)((3c)(z)))))//再展3=λc.λz.(((λf.λc.(f(f(f(c)))c)((3c)((3c)(z))))αλc.λz.(((λf.λw.(f(f(f(w)))c)((3c)((3c)(z))))βλc.λz.(((λw.(c(c(c(w))))((3c)((3c)(z))))//同理展开第二个c,第三个c=λc.λz.(((λw.(c(c(c(w))))((λp.(c(c(c(p)))))((λq.(c(c(c(q)))))(z))))βλc.λz.(((λw.(c(c(c(w))))((λp.(c(c(c(p)))))(((c(c(c(z))))))βλc.λz.(((λw.(c(c(c(w))))(((c(c(c(c(c(c(z)))))))))))βλc.λz.(c(c(c(c(c(c(c(c(c(z))))))))))=911.2.5Church-Rosser定理按照λ演算的运算规则，谁先归约最后归约出的结果是一样的。例:不同归约次序的正规λ演算得同一结果((λx.(xy))(λu.(uv)))(λp.(pq)r)((λu.(uv))y)(λp.(pq)r)（(λx.(xy))(λu.(uv)))(rq)(yv)(λp.(pq)r)((λu.(uv))y)(rq)((λu.(uv))y)(rq)(yu)(rq)(yu)(rq)(yu)(rq)•(1)严格函数归约直到不可归约时正常终止，除开不可归约函数而外，有些函数尽管在符号上可归约，语义上无任何意义，到机器上不可执行的。这就是所谓停机问题，一般说来，停机问题是不可判定的，但我们在表示上给它以符号，例如：dividem0=表示该函数非正常终止，是一个不代表任何值的值。不终止的计算结果值为若f=则称f为严格函数若f=v,v为确定的值，则f为非严格函数正是由于有非严格函数的存在，就产生了求值次序的问题-•非严格函数取决于次序的例子例：λ演算不同求值次序的归约(λn.multiplynn)add34)//先做右端子表达式=(λn.muliplynn)7//急求值=multiply77=49=mutiply(add34)(add34)//先做β归约=mutiply7(add34)=mutiply77=49//正规求值若为mutiply(add34)(add34)//两个表达式一样，后一个不归约，取前一个的值。=mutiply77=49//懒求值•重述Church-Rosser定理如按正规求值次序对某表达式E求值结果为正常值v，则按其他求值次序可能是v也可能是。若按正规求值结果为即非正常终止，则按任何求值规则结果也为•正规求值是由外向里Outside_in求值急求值是由里向外Inside_out求值11.2.6增强λ演算只用最底层λ演算是极其复杂的。用高层命名函数，语义清晰。不仅如此，保留一些常见关键字，语义更清晰。例如，我们可以定义一个if_then_else为名的函数：if_then_else=λp.λm.λn.pmn，当p为'真'时，执行m否则为n。我们先验证其真伪。例：当条件表达式为真时if_then_else函数的归约(if_then_else)TMN=(λp.λm.λn.pmn)TMN=(λm.λn.(Tmn))MN=(λm.λn.(λx.λy.x)mn)MN=(λm.λn.(λy.m)n)MN=(λm.λn.