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

函数式编程语言、编程和程序验证 计计算机科学与技术术学院 陈陈意云 2010.7 内 容 提 要 学习函数式语言是因为课程实践所用工具中， 需要用函数式风格编程。另外，需要对比函数式 程序和命令式程序在程序验证上的区别 函数式编程语言概述 演算简介 函数式语言SML及编程简介 函数式语言SML的模块系统 函数式程序的验证 函数式编程语言概述 函数式编程是一种编程范型 它把计算看作是对数学函数的求值，避免了状态和 易变数据结构 函数是构造程序的基本成分，语言还提供构造更为 复杂的函数的机制，语言禁止使用赋值语句 函数式编程的根基是演算 演算是1930年代在调查函数定义、函数应用和递 归时研发的一个形式系统，是等价于图灵机的一种 抽象的计算模型 许多函数式编程语言都可看成是在演算基础上精 心制作出的结果 函数式编程语言概述 函数式与命令式的比较 函数式编程强调函数应用，而命令式编程风格强调 状态的改变 命令式程序的“函数”有副作用，如改变全局变量 命令式程序缺乏引用透明性，副作用是其根源 引用透明性：可自由地将（子）表达式替换为它的 值而不改变程序（表达式） 函数式程序中，函数的结果仅依赖于提供给它的参 数 没有副作用使得理解程序和预测程序的行为变得容 易，这是研究函数式语言的一个关键动机 函数式编程语言概述 函数式语言的用途 历史上，（纯）函数式语言一直被学术界（而不是 商用软件研发）重视 现在，Scheme, OCaml和Haskell等函数式语言已经 出现在工业和商业应用中 通过领域专用编程语言，函数式编程有更广阔的天 地，如Mathematica（符号数学）、R（统计）、J 和K（金融分析） 函数式编程的风格也可用于不是专为函数式编程设 计的语言中，如Javascript融入了函数式编程的功 能，类似的还有Perl语言 演 算 简 介 1、表示法 表示法的主要特征 抽象：用于定义函数 应用：将所定义的函数作用于变元 抽象的例子 （自然数类型上的几个例子） 恒等函数：x : nat.x / 命令式表示Id(x : nat) = x 后继函数：x : nat.x 1 / 函数式无需给函数命名 常函数：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、演算 演算是关于表达式的一个推理系统，下面用 等式公理系统（公理语义）来描述 约束变元改名公理（公理） x:.M y:.yxM，M中无自由出现的y NxM表示M中自由出现的x用表达式N代换的结果 例如 x:.x y:.y 函数应用公理（公理） (x:.M)N N/xM 例如 (x:nat.x+4) 4 4/x(x+4) 4 + 4 演 算 简 介 自反公理、对称性规则、传递性规则 同余规则 相等的函数作用于相等的变元产生相等的结果 等式证明规则允许推导任何一组等式前提的逻 辑推论 还可以定义演算的操作语义和指称语义 M1 = M2, N1 = N2 M1 N1 = M2 N2 演 算 简 介 简单例子 ( x. ( y. z. ( x + y ) + z ) 3 ) 4 5 = ( x. z. ( x + 3 ) + z ) 4 5 = ( z. ( 4 + 3 ) + z ) 5 = ( 4 + 3 ) + 5 = 12 演 算 简 介 复杂例子：高阶函数应用到函数，得到函数 Curry, f : . x:. y:. f x, y add p:nat nat. (Proj1 p) + (Proj2 p) Curry(add) = x:nat. y:nat. x + y 演算过程在下页，给Curry加上角标是避免引入多态 该例体现函数式语言区别命令式语言的优点 函数作为编程语言的第一类实体，即对它们的使用 没有限制 可以动态地构造新函数 演 算 简 介 复杂例子：高阶函数应用到函数，得到函数 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. Proj1x, y + Proj2 x, y = x:nat. y:nat. x + y 函数式语言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等 函数式语言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可使程序简洁，免去重复计算公共子表达式 函数式语言SML及编程简介 例3（记录类型） type student = name : string; age : int; score : real type student 记录是具有标签的元组 函数式语言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是类型变量，类型变量以撇号开始 函数式语言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 函数式语言SML及编程简介 表的简介 表（list）是相同类型元素的有限序列 如：3, 5, 9, (1, “one”), (2, “two”), (3, “three”) 表的构造符 空表： 在已有的表前加入一个元素：: 9 : = 9, 5 : 9 = 5, 9 基本的表函数 null（测试空表）、hd（返回表头元素）、tl（返 回非空表的表尾）、length（返回表长） 函数式语言SML及编程简介 例5（表类型）计算表的长度 fun length = 0 | length (x : xs) = 1 + length xs; val length = fn : a list - int length 3, 5, 9length “one”, “two”, “three” 3 : int 3 : int 竖线“ | ”将函数声明分成两子句，各处理一个模式 length是一个多态类型的函数 list相当于一个类型构造符 函数式语言SML及编程简介 例6（表类型）插入排序 fun insert(x, ) : real list = x | insert(x, y : ys) = if x val insert = fn : real real list - real list 排序需要用到两个变元的比较运算，关系运算“ val map = fn : (a - b) - (a list - b list) 算子map把函数 f 应用到表的每个元素上，即 map f x1, , xn = f x1, , f xn map f的结果是一个新函数 函数式语言SML及编程简介 例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) 称为闭包，是语言实现中的概念 函数式语言SML的模块系统 模块化关心的是程序的组织，而不是计算本身，模块 化结构使得程序易于理解、编写和维护等 SML模块所涉及的主要构造是结构、基调和函子 结构：由一组类型、值和结构的声明组成 基调：是结构的“类型”或“界面”，规范结构必须包 含的声明 函子：从结构到结构的函数 类比：（模块化） 结构 （核心语言） 值 基调 类型 函子 函数 函数式语言SML的模块系统 例9：使用模块系统的一个简单例子 signature SIG = /* 描述有类型t和值x的结构类 */ sig type t val x : t end; structure S : SIG = /* 符合上述基调的一个结构*/ struct type t = int val x : t = 3 end; 可以用基调来规范结构的部分成员 函数式语言SML的模块系统 例9：使用模块系统的一个简单例子 structure S : SIG = /* 符合上页基调的一个结构*/ struct type t = int val x : t = 3 end; functor F(S : SIG) : SIG = struct type t = S.t S.t val x : t = (S.x, S.x) end 函数式程序的验证 程序验证就是证明程序具有所期望的性质，它 是提高软件可信程度的重要方法 1、模型检测 通过遍历系统所有状态空间，能够对有穷状态系统 进行自动验证，并自动构造不满足验证性质的反例 问题：难以解决状态空间爆炸问题，不能输出显式 的证据 2、形式程序验证（formal program verification） 命令式语言的程序验证起源于Hoare逻辑 函数式程序验证因不涉及程序状态，要简单得多 函数式程序的验证 例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阶乘 和已经熟悉的证明方式没有什么区别 函数式程序的验证 例11：用结构归纳验证表并置前后的表长关系 fun length = 0 | length(x:xs)= 1 + length xs; fun ys= ys /*是中缀的函数名*/ | (x:xs) ys= x : (xsys); 要证的性质是length(xsys) = length(xs) + length(ys) 1、基本情况 length( ys) = length ys = 0 + length ys 算术 = length + length ys length 成立 函数式程序的验证 例11：用结构归纳验证表并置前后的表长关系 fun length = 0 | length(x:xs) = 1 + length xs; fun ys = ys | (x:xs) ys = x : (xsys); 要证的性质是length(xsys) = length(xs) + length(ys) 2、归纳步骤 length(x:xs)ys) = length(x:(xsys) = 1 + length(xsys)length = 1 + length xs + length ys归纳假设 = (1 + length xs) + length ys结合律 = length(x:xs) + length yslength 成立 函数式程序的验证 良基关系 集合A的良基关系是A上的二元关系，它具有这样 的性质：A上不存在无穷递减序列a0 a1 a2 例：在自然数上，如果j i +1，则i j，则这 个关系是一个良基关系 良基关系的一些特点 良基关系不一定有传递性 良基关系都是非自反的，即对任何aA，a a不成 立；否则会出现无穷