函数式编程语言、编程和程序验证.ppt

《函数式编程语言、编程和程序验证.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、函数式编程语言、编程和程序验证计算机科学与技术学院陈意云2010.7内容提要学习函数式语言是因为课程实践所用工具中，需要用函数式风格编程。另外，需要对比函数式程序和命令式程序在程序验证上的区别函数式编程语言概述演算简介函数式语言SML及编程简介函数式语言SML的模块系统函数式程序的验证函数式编程语言概述函数式编程是一种编程范型它把计算看作是对数学函数的求值，避免了状态和易变数据结构函数是构造程序的基本成分，语言还提供构造更为复杂的函数的机制，语言禁止使用赋值语句函数式编程的根基是演算演算是1930年代在调查函数定义、函数应用和递归时研发的一个形式系

2、统，是等价于图灵机的一种抽象的计算模型许多函数式编程语言都可看成是在演算基础上精心制作出的结果函数式编程语言概述函数式与命令式的比较函数式编程强调函数应用，而命令式编程风格强调状态的改变命令式程序的“函数”有副作用，如改变全局变量命令式程序缺乏引用透明性，副作用是其根源引用透明性：可自由地将（子）表达式替换为它的值而不改变程序（表达式）函数式程序中，函数的结果仅依赖于提供给它的参数没有副作用使得理解程序和预测程序的行为变得容易，这是研究函数式语言的一个关键动机函数式编程语言概述函数式语言的用途历史上，（纯）函数式语言一直被学术界（而不是商用软件研发）重

3、视现在，Scheme,OCaml和Haskell等函数式语言已经出现在工业和商业应用中通过领域专用编程语言，函数式编程有更广阔的天地，如Mathematica（符号数学）、R（统计）、J和K（金融分析）函数式编程的风格也可用于不是专为函数式编程设计的语言中，如Javascript融入了函数式编程的功能，类似的还有Perl语言演算简介1、表示法表示法的主要特征抽象：用于定义函数应用：将所定义的函数作用于变元抽象的例子（自然数类型上的几个例子）恒等函数：x:nat.x//命令式表示Id(x:nat)=x后继函数：x:nat.x1//函数式无

4、需给函数命名常函数：x:nat.10x:nat.xtrue不是良形的表达式表示法写出的表达式叫做表达式或项演算简介项x:.M和谓词演算公式x:A.的比较是一个约束算子x是一个占位符，约束变元，可以重新命名约束变元而不改变表达式的含义在x:.x+y中，x的出现是约束的，y的出现是自由的不含自由变元的表达式称为闭表达式应用：用项的并置来表示函数应用，例：(x:nat.x)5(x:nat.x)55/*应用下页介绍的公理*/演算简介2、演算演算是关于表达式的一个推理系统，下面用等式公理系统（公理语义）来描述约束变

5、元改名公理（公理）x:.My:.yxM，M中无自由出现的yNxM表示M中自由出现的x用表达式N代换的结果例如x:.xy:.y函数应用公理（公理）(x:.M)N[N/x]M例如(x:nat.x+4)4[4/x](x+4)4+4演算简介自反公理、对称性规则、传递性规则同余规则相等的函数作用于相等的变元产生相等的结果等式证明规则允许推导任何一组等式前提的逻辑推论还可以定义演算的操作语义和指称语义M1=M2,N1=N2M1N1=M2N2演算简介简单例子(x.(y.z.(x+y)+z)3)45=(x.

6、z.(x+3)+z)45=(z.(4+3)+z)5=(4+3)+5=12演算简介复杂例子：高阶函数应用到函数，得到函数Curry,f:.x:.y:.fx,yaddp:natnat.(Proj1p)+(Proj2p)Curry(add)=x:nat.y:nat.x+y演算过程在下页，给Curry加上角标是避免引入多态该例体现函数式语言区别命令式语言的优点函数作为编程语言的第一类实体，即对它们的使用没有限制可以动态地构造新函数演算简介复杂例子：高阶函数应用到函数，得到函数Curry(add)(f:natna

7、tnat.x:nat.y:nat.fx,y)add=x:nat.y:nat.addx,yx:nat.y:nat.(p:natnat.(Proj1p)+(Proj2p))x,y=x:nat.y:nat.Proj1x,y+Proj2x,y=x:nat.y:nat.x+y函数式语言SML及编程简介使用StandardML语言，简称SML例1（整型）：辗转相除法求最大公约数fungcd(m,n)=/*函数声明表达式*/ifm=0thennelsegcd(nmodm,m);>valgcd=fn:intint->in

8、t/*SML的回应*/gcd(13,78)/*函数应用表达式*/>13:int程