函数式编程语言、编程和程序验证 计算机科学与技术学院 陈意云 2010.7.

Presentation on theme: "函数式编程语言、编程和程序验证 计算机科学与技术学院 陈意云 2010.7."— Presentation transcript:

1 函数式编程语言、编程和程序验证 计算机科学与技术学院 陈意云 2010.7

2 内 容 提 要 学习函数式语言是因为课程实践所用工具中， 需要用函数式风格编程。另外，需要对比函数式 程序和命令式程序在程序验证上的区别
内 容 提 要 学习函数式语言是因为课程实践所用工具中， 需要用函数式风格编程。另外，需要对比函数式 程序和命令式程序在程序验证上的区别 函数式编程语言概述 演算简介 函数式语言SML及编程简介 函数式语言SML的模块系统 函数式程序的验证

3 函数式编程语言概述 函数式编程是一种编程范型 它把计算看作是对数学函数的求值，避免了状态和易变数据结构
函数是构造程序的基本成分，语言还提供构造更为复杂的函数的机制，语言禁止使用赋值语句 函数式编程的根基是演算 演算是1930年代在调查函数定义、函数应用和递归时研发的一个形式系统，是等价于图灵机的一种抽象的计算模型 许多函数式编程语言都可看成是在演算基础上精心制作出的结果 3

4 函数式编程语言概述 函数式与命令式的比较 函数式编程强调函数应用，而命令式编程风格强调状态的改变
命令式程序的“函数”有副作用，如改变全局变量 命令式程序缺乏引用透明性，副作用是其根源 引用透明性：可自由地将（子）表达式替换为它的值而不改变程序（表达式） 函数式程序中，函数的结果仅依赖于提供给它的参数 没有副作用使得理解程序和预测程序的行为变得容易，这是研究函数式语言的一个关键动机 4

5 函数式编程语言概述 函数式语言的用途 历史上，（纯）函数式语言一直被学术界（而不是商用软件研发）重视
现在，Scheme, OCaml和Haskell等函数式语言已经出现在工业和商业应用中 通过领域专用编程语言，函数式编程有更广阔的天地，如Mathematica（符号数学）、R（统计）、J和K（金融分析） 函数式编程的风格也可用于不是专为函数式编程设计的语言中，如Javascript融入了函数式编程的功能，类似的还有Perl语言 5

6  演 算 简 介 1、表示法 表示法的主要特征 抽象的例子 （自然数类型上的几个例子） 表示法写出的表达式叫做表达式或项
 演 算 简 介 1、表示法 表示法的主要特征 抽象：用于定义函数 应用：将所定义的函数作用于变元 抽象的例子 （自然数类型上的几个例子） 恒等函数：x : nat.x // 命令式表示Id(x : nat) = x 后继函数：x : nat.x  1 // 函数式无需给函数命名 常函数：x : nat.10 x : nat.x  true 不是良形的表达式 表示法写出的表达式叫做表达式或项 6

7  演 算 简 介 项x : .M 和谓词演算公式x : A. 的比较 应用：用项的并置来表示函数应用，例： 是一个约束算子
 演 算 简 介 项x : .M 和谓词演算公式x : A. 的比较 是一个约束算子 x是一个占位符，约束变元，可以重新命名约束变元而不改变表达式的含义 在x:.x + y中，x的出现是约束的， y的出现是自由的 不含自由变元的表达式称为闭表达式 应用：用项的并置来表示函数应用，例： (x : nat.x) 5 (x : nat.x) 5  5 /*应用下页介绍的公理*/ 7

8  演 算 简 介 2、演算 演算是关于表达式的一个推理系统，下面用等式公理系统（公理语义）来描述 约束变元改名公理（公理）
 演 算 简 介 2、演算 演算是关于表达式的一个推理系统，下面用等式公理系统（公理语义）来描述 约束变元改名公理（公理） 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 8

9  演 算 简 介 自反公理、对称性规则、传递性规则 同余规则 等式证明规则允许推导任何一组等式前提的逻辑推论
 演 算 简 介 自反公理、对称性规则、传递性规则 同余规则 相等的函数作用于相等的变元产生相等的结果 等式证明规则允许推导任何一组等式前提的逻辑推论 还可以定义演算的操作语义和指称语义 M1 = M2, N1 = N2 M1 N1 = M2 N2 9

10  演 算 简 介 简单例子 ( x. ( y. z. ( x + y ) + z ) 3 ) 4 5
 演 算 简 介 简单例子 ( x. ( y. z. ( x + y ) + z ) 3 ) 4 5 = ( x. z. ( x + 3 ) + z ) 4 5 = ( z. ( ) + z ) 5 = ( ) + 5 = 12 10

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

12  演 算 简 介 复杂例子：高阶函数应用到函数，得到函数 Curry(add)
 演 算 简 介 复杂例子：高阶函数应用到函数，得到函数 Curry(add)  (f:nat  nat  nat. x:nat. y:nat. f x, y) add = x:nat. y:nat. add x, y  x:nat. y:nat. (p:nat  nat. (Proj1 p) + (Proj2 p)) x, y = x:nat. y:nat. Proj1x, y + Proj2 x, y = x:nat. y:nat. x + y 12

13 函数式语言SML及编程简介 使用Standard ML语言，简称SML 例1（整型）： 辗转相除法求最大公约数
fun gcd(m, n) = /*函数声明表达式 */ if m = 0 then n else gcd(n mod m, m); > val gcd = fn : int  int -> int /* SML的回应 */ gcd(13, 78) /*函数应用表达式*/ > 13 : int 程序由一个或多个表达式构成 程序都可以翻译成类型化的表达式，在此不介绍 SML还有其他基本类型：real, bool, string等 13

14 函数式语言SML及编程简介 例2（积类型）：把分数n/d约分到最简分式
fun fraction(n, d) = /*(n, d)是int  int的元素 */ let val com = gcd(n, d) in (n div com, d div com) end; > val fraction = fn : int  int -> int  int 引入let后，表达式的一般形式是 let D1 D2 … Dn in E end let 引入的声明相当于命令式语言的局部声明，let声 明可以嵌套，联立的let可用来声明相互递归的函数 使用let可使程序简洁，免去重复计算公共子表达式 14

15 函数式语言SML及编程简介 例3（记录类型） type student = { name : string; age : int;
score : real } > type student 记录是具有标签的元组 15

16 函数式语言SML及编程简介 例4（多态类型） fun gcd(m, n) = if m = 0 then n
else gcd(n mod m, m); 其中的if … then …else 是一个内部定义的多态函数 if … then …else = fn : bool  a  a  a 其中a是类型变量，类型变量以撇号开始 16

17 函数式语言SML及编程简介 例4（多态函数）取二元组的第1元和第2元 fun fst(x, y) = x;
> val fst = fn : a  b  a fun snd(x, y) = y; > val snd = fn : a  b  b 17

18 函数式语言SML及编程简介 表的简介 表（list）是相同类型元素的有限序列
如：[3, 5, 9], [ (1, “one”), (2, “two”), (3, “three”) ] 表的构造符 空表：[ ] 在已有的表前加入一个元素：:: 9 :: [ ] = [9], 5 :: [9] = [5, 9] 基本的表函数 null（测试空表）、hd（返回表头元素）、tl（返回非空表的表尾）、length（返回表长） 18

19 函数式语言SML及编程简介 例5（表类型）计算表的长度 fun length [ ] = 0
| length (x :: xs) = 1 + length xs; > val length = fn : a list -> int length [3, 5, 9] length [“one”, “two”, “three”] > 3 : int > 3 : int 竖线“ | ”将函数声明分成两子句，各处理一个模式 length是一个多态类型的函数 list相当于一个类型构造符 19

20 函数式语言SML及编程简介 例6（表类型）插入排序 fun insert(x, [ ]) : real list = [ x ]
| insert(x, y :: ys) = if x <= y then x :: y :: ys else y :: insert(x, ys); > val insert = fn : real  real list -> real list 排序需要用到两个变元的比较运算，关系运算“<=”不是多态的，因此insert不是多态函数 在第1行上给出函数的结果类型就是为了避免类型推断出现错误 20

21 函数式语言SML及编程简介 例7（表类型）基于表的一个高阶函数 fun map f [ ] = [ ]
| map f (x :: xs) = (f x) :: map f xs; > val map = fn : (a -> b) -> (a list -> b list) 算子map把函数 f 应用到表的每个元素上，即 map f [x1, …, xn] = [f x1, …, f xn] map f的结果是一个新函数 21

22 函数式语言SML及编程简介 例8 静态作用域（静态绑定） let val x = 2
例8 静态作用域（静态绑定） let val x = 2 fun f y = x + y /* x是函数f的非局部变量*/ fun F (g, x) = g 2 in F(f, 1) 按静态作用域和动态作用域，结果分别为4和3 f函数所引用的x绑定到2，这样的绑定成为f的环境 在计算F(f, 1)时，必须把f和它的环境ef一起传递，以保证f不管在何处计算都有正确的计算环境 二元组(f, ef) 称为闭包，是语言实现中的概念 22

23 函数式语言SML的模块系统 模块化关心的是程序的组织，而不是计算本身，模块 化结构使得程序易于理解、编写和维护等
结构：由一组类型、值和结构的声明组成 基调：是结构的“类型”或“界面”，规范结构必须包含的声明 函子：从结构到结构的函数 类比：（模块化） 结构 ～（核心语言） 值 基调 ～ 类型 函子 ～ 函数 23

24 函数式语言SML的模块系统 例9：使用模块系统的一个简单例子 signature SIG = /* 描述有类型t和值x的结构类 */ sig
type t val x : t end; structure S : SIG = /* 符合上述基调的一个结构*/ struct type t = int val x : t = 3 可以用基调来规范结构的部分成员 24

25 函数式语言SML的模块系统 例9：使用模块系统的一个简单例子 structure S : SIG = /* 符合上页基调的一个结构*/
type t = int val x : t = 3 end; functor F(S : SIG) : SIG = type t = S.t  S.t val x : t = (S.x, S.x) end 25

26 函数式程序的验证 程序验证就是证明程序具有所期望的性质，它是提高软件可信程度的重要方法 1、模型检测
通过遍历系统所有状态空间，能够对有穷状态系统进行自动验证，并自动构造不满足验证性质的反例 问题：难以解决状态空间爆炸问题，不能输出显式的证据 2、形式程序验证（formal program verification） 命令式语言的程序验证起源于Hoare逻辑 函数式程序验证因不涉及程序状态，要简单得多 26

27 函数式程序的验证 例10：用数学归纳法验证计算阶乘的函数 fun facti(n, p) =
if n = 0 then p else facti(n -1, n * p); 要证明的性质是p. facti(n, p) = n!  p 1、基本情况，要证p. facti(0, p) = 0!  p 因为facti(0, p) = p = 1  p = 0!  p，成立 2、归纳步骤，要证p. facti(n+1, p) = (n+1)!  p facti(n+1, p) = facti(n, (n+1) * p) [facti] = n!  ((n+1)  p) [归纳假设] = (n!  (n+1))  p [结合律] = (n+1)!  p [阶乘] 和已经熟悉的证明方式没有什么区别 27

28 函数式程序的验证 例11：用结构归纳验证表并置前后的表长关系 fun length [ ] = 0
| length(x::xs) = 1 + length xs; fun [ ys = ys | ys = x :: = length(xs) + length(ys) 1、基本情况 length([ = length ys = 0 + length ys [算术] = length [ ] + length ys [length] 成立 28

29 函数式程序的验证 例11：用结构归纳验证表并置前后的表长关系
fun length [ ] = 0 | length(x::xs) = 1 + length xs; fun [ ys = ys | ys = x :: = length(xs) + length(ys) 2、归纳步骤 = = [length] = 1 + length xs + length ys [归纳假设] = (1 + length xs) + length ys [结合律] = length(x::xs) + length ys [length] 成立 29

30 函数式程序的验证 良基关系 例：在自然数上，如果j  i +1，则i  j，则这个关系是一个良基关系 良基关系的一些特点
集合A的良基关系是A上的二元关系，它具有这样的性质：A上不存在无穷递减序列a0  a1  a2  … 例：在自然数上，如果j  i +1，则i  j，则这个关系是一个良基关系 良基关系的一些特点 良基关系不一定有传递性 良基关系都是非自反的，即对任何aA，a  a不成立；否则会出现无穷递减序列a  a  a  … 每个非空子集都有一个极小元 30

31 函数式程序的验证 良基归纳 令是集合A上的一个良基关系， 令P是A上的某个性质，
若每当所有的P(b) (b  a)为真则P(a)为真，即 a.( b. (b  a  P(b))  P(a) ) 那么，对所有的aA，P(a)为真 31

32 函数式程序的验证 例12：用良基归纳法 y. facti(n, p) = fact(n)  p 其中 fun facti(n, p) =
if n = 0 then p else facti(n -1, n  p); fun fact(n) = if n = 0 then 1 else fact(n -1)  n; 自然数集合，使用的良基关系是： 若i = j – 1，则i  j 按良基归纳的概念进行证明 32

33 函数式程序的验证 fun facti(n, p) = if n = 0 then p else facti(n -1, n  p);
fun fact(n) = if n = 0 then 1 else fact(n -1)  n; 待证：y. facti(n, p) = fact(n)  p 证明： 1、若n=0，则 facti(n, p) = p = 1  p = fact(n)  p 2、若n>0，则 facti(n, p) = facti(n -1, n  p) [facti] = fact(n-1)  (n  p) [归纳假设] = (fact(n-1)  n)  p [结合律] = fact(n)  p [fact] 33