软件开发形式化方法教材.pdf

发布时间：2022-06-08 发布人：admin 分类：说明书资料大小：0.97M 资料格式：pdf 举报版权申诉

wupengyuan-3329762-4744302543304258361.pdf-第1页.png

第1页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第2页.png

第2页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第3页.png

第3页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第4页.png

第4页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第5页.png

第5页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第6页.png

第6页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第7页.png

第7页 / 共142页

wupengyuan-3329762-4744302543304258361.pdf-第8页.png

第8页 / 共142页

形式语义（第一章理论基础）.pdf

形式语义学（第二章函数式抽象语言）.pdf

形式语义学（操作语义）.pdf

形式语义学（指称语义学）.pdf

形式语义学（公理语义）.pdf

第一章理论基础本章的主要内容包括： [1] Lambda 演算基础 1.1 Lambda 演算基础 [2] 完全半序集 [3] 连续函数 [4] 最小不动点 1.1 Lambda 演算基础 1941 年 Church 创建了 Lambda 演算理论。它是一个形式系统，可作为计算模型，如同 Turing 机可作为计算模型一样。Lambda 演算系统主要由两部分组成:其一是表达式，其二是变换规则。Lambda 演算系统可有多种，其主要区别就在于构成 Lambda 演算系统的两个组成部分的具体定义上。我们将会看到 Lambda 演算系统可描述任何一部分递归函数的计算过程。Lambda 演算理论是函数式语言的理论基础。 1.1.1 Lambda 表达式定义 1.1.1 (表达式)：若用 x 表示变量，用 Exp 表示纯 Lambda 表达式之集，则 Exp 的定义如下： (1) x ∈Exp ； (2) 若 E1∈Exp，E2∈Exp，则 E1E2 ∈Exp； (3) 若 E ∈Exp，则 λx.E∈Exp； (4) 若 E ∈Exp，则 (E)∈Exp。其中形如 (E1E2) 的表达式被称为施用表达式，而称形如（λx.E）的表达式为抽象表达式。施用表达式(E1E2)对应于通常的函数调用f(E)，而抽象表达式（λx.E）则对应于函数定义。若用BNF表示法，则表达式结构可描述如下(x∈Var，E∈Exp ): E ::= x | E1 E2 | λx.E | ( E ) 从上述定义可知道，Lambda 表达式是非常小的表达式，以至于不能再小。但它将成为 Lambda 演算系统的基础。那么一个作为计算模型的形式系统应具备什么样的条件 ? 很显然它起码应具备二个条件:其一是它有很强的功能，以至于能够描述复杂的计算过程；其二是它应非常小，以至于其语义是非常清楚的。抽象表达式λx.E 用来表示无名函数。通常的方法是首先定义函数名，然后再使用它，因此函数都有名，而抽象表达式则表示一无名函数。假设有函数定义： - 1 -

func f(x)= x+1 则它定义了这样一个函数，既函数名是 f,自变量（形参）是 x，而函数值是 x+1 的值。当然我们也可用别的方式定义出上述函数，例如 func f = λx.x+1 这种表示法也能方便地表示哪个是函数名，哪个是自变量名，哪部分是函数体，其中λ表示其后的变量为自变量。假设有 f(a*b),则它应等价于(λx.x+1)(a*b),而其中(λx.x+1)和(a*b)都是表达式，这样在 Lambda 表达式的定义中出现了 E1E2 形式的表达式。从语义角度来说其中的 E1 必须是函数，而 E1E2 的含义是把函数作用与表达式 E2。我们称λx.E 中的 E 表达式为函数λx.E 的体部分，而称 x 为该函数的自变量。定义 1.1.2 (记法约定)：为了节省括弧做如下约定 (1) E1 E2 E3...En = (((E1 E2)E3)...)En (左结合规则) (2) λx1...λ.xn.E = λx1.(...(λxn.En)...)) (3) λx1 x2...xn.E = λx1.λx2....λ.xn.E (4) λx1...λ.xn.E1 E2...En = λx1...λ.xn.(E1 E2...En) 例 1.1.1 下面是一些简单的 Lambda 表达式例: λx.λy.xy λxy.x λxy.x(y) (λx.xy)y λx.x λxy.y xy (λx.xx)(λx.xx) x(λx.xy ) 单从 Lambda 表达式结构看，看不出任何意义，因为其中既没有常量也没有函数名，不知道是如何计算的。究竟如何计算表达式值，将由 Lambda 演算的第二组成部分，即 Lambda 变换部分来决定。作个比喻的话 Lambda 表达式相当于程序，而 Lambda 变换部分则相当于程序的解释系统。后面将逐步介绍 Lambda 变换部分。定义 1.1.3 (子表达式)：设 E 是表达式，并用 sub(E)表示 E 的子表达式集，则定义 sub(x)={x} sub(E1E2)= sub(E1)∪ sub(E2)∪{E1E2} sub(λx.E)= λx.E}∪ sub(E) sub((E))={E} ∪ sub(E) 定义 1.1.4 (作用域)：设有表达式λx.E，则定义λx 的作用域为其中的体表达式 E。如若在 E 中包含一个子表达式λx.E1，则外层λx 的作用域将不包含该子表达式 E1 部分，即外层λx 对 E1 无效。定义 1.1.5 (自由出现)：设 x′是表达式 E 中 x 的一次出现，则称该出现为 x 的一自由出现，如果在 E 中没有一个子表达式λx.E1 包含该 x′出现。称非自由出现为约束出现。例如假设有 λx.x( λx.x y x)x x 定义 1.1.6 (自由变量)：称变量 x 为表达式 E 的自由变量，如果 E 中至少有一个 x 的自由出现。若用 Free(E)表示 E 的自由变量之集，则 Free(E)的具体定义如下: - 2 -

Free(x) = {x} Free(E1E2)= Free(E1)∪Free(E2) Free(λx.E)= Free(E)-{x} Free((E))= Free(E) 下面将定义所谓的代换[E0/x]E，它表示用表达式 E0 去代换表达式 E 中所有 x 的自由出现。解释 Lambda 演算系统的最基本的概念之一是这里所说的代换，因此，要确切地理解 Lambda 演算系统必须要熟悉代换的精确概念. 定义 1.1.7 (代换[E0/x]E): (1) E ≡ x 情形 (2) E ≡ y 情形 (3) E ≡ E1 E2情形 (4) E ≡ λx.E′情形 (5) E ≡ λy.E′情形(x≠y): x∈ Free(E′)∧y∈Free(E0)时:[E0/x](λy.E′)= λz.[E0/x][z/y]E′ :[E0/x]x= E0 :[E0/x]y= y ，(x≠y) :[E0/x](E1 E2)=([E0/x]E1)([E0/x]E2) :[E0/x](λx.E′)=λx.E′ x∉Free(E′)∨y∉Free(E0))时:[E0/x](λy.E′)= λy.[E0/x]E′ 关于代换的符号表示法有多种，例如还有 E[E0/x]，E[x←E0] ，E{E0/x} 等。 1.1.2 Lambda 变换给了一个表达式即可根据 Lambda 演算系统所定义的变换规则进行一系列的变换，其结果有两种可能:一是不能进一步的归约；二是变换无终止地进行下去(相当于程序不终止)。不同的 Lambda 演算系统具有不同的变换规则，有的可能只有两个变换规则，有的可能有三个变换规则，有的甚至可能有更多的变换规则。这里将介绍的 Lambda 变换规则是最常见的一种。定义 1.1.8 (α变换)：设 E 是 Lambda 表达式，x 是变量，则称下面变换为 α变换（其中 Y 不在 Free(λx.E)中）。 λx.E ⎯→⎯α λy.[y/x] E α变换后所得新表达式的区别仅在于更换了抽象表达式的λ变量名，因此通常也称α变换为改名变换。例 1.1.1 1. λx.(Zx) ⎯→⎯α λy.(Zy) 2. λx.((λY.Yx)x) ⎯→⎯α λz.((λY.Yz)z) 3. λx.(Z(λY.x)) ⎯→⎯α λy.(Z(λy.y)): 非法α变换 4. λx.(ZY) ⎯→⎯α λY.(ZY) : 非法α变换定义 1.1.9 (β变换)：设 (λx.E)和 E0 为 Lambda 表达式，则称下面变换为β变换： - 3 -

(λx.E)E0 称β变换规则的左部表达式为β基。从形式上看每个β变换归约掉一个λ。 β⎯ →⎯ [E0/x] E β变换是最重要的一个变换，可没有其他一些变换，但不能没有β变换。因此，所有不同 Lambda 演算系统都有这一β变换。β变换规则实际上是定义了函数调用的语义，因为β变换规则的左部是一个"函数调用"部分。( λx.E)E0 中的(λx.E )为被调用函数，x 为函数的自变量，E0 为实参表达式，而[E0/x]E 则表示把实参 E0 代入到函数体 E 中的形参 x 中，这正是熟知的函数调用过程。例 1.1.2 β⎯ →⎯ Ay 1. (λx.xy)A β⎯ →⎯ Ax 2. (λy.yx)A β⎯ →⎯ AA 3. (λx.xx)A 4. (λx.(λy.(λz.xyz)))ABC β⎯ →⎯ (λy.(λz.Ayz)))BC β⎯ →⎯ (λz.ABz)))C β⎯ →⎯ ABC 定义 1.1.10 (η变换)：假设 λx.Mx 是一个表达式，且满足条件 x∉Free(M)，则称下面变换为η变换: (λx.M x) η⎯ →⎯ M 不难看出η变换是一种简化规则，也是一种保值变换。保值的依据是函数的等价性定义，即 ∀(x)[f(x)=h(x)]⊃f=h。事实上我们有 ∀(y)[(λx.Mx)y = My ] 故有(λx.Mx)=M，也就是说η变换规则的左右部表达式是等值表达式。有些Lambda演算系统没有这一种变换规则，也就是说η变换不是演算系统所必需的变换规则。例 1.1.3 λx .(λy.yyy)x λx .(λy.yyx)x η⎯ →⎯ (λy.yyy) η⎯ →⎯ (λy.yyx) 非法η变换定义 1.1.11 （Lambda 归约）： (1) 称β变换的左部施用表达式(λx.E)E0为β基。 (2) 称η变换的左部抽象表达式(λx.Mx)为η基。 (3) β基和η基统称为归约基。 (4) 对表达式中的某一归约基实施某种变换称之为归约。定义 1.1.12 （范式）：假设 E 是一个 Lambda 表达式，且其中没有任何一个归约基，则称该表达式为范式。如果一个表达式经过有限次变换能归约成范式，则称该表达式有范式，否则称无范式。例 1.1.4 下面是范式和非范式例 (1) x (2)xx (3)λx.xx (4) x(λx.xx) …… 范式例 - 4 -

(1) λx.x((λy.x)y) （2）λx.x(λy.xy)…………… 非范式例现在要考虑的问题是，表达式是否都有范式?若有，是否唯一?范式应该如何求?下面将说明以下一些问题： (1) 归约过程不唯一； (2) 表达式不一定都有范式； (3) 如果有范式一定唯一； (4) 如果有范式则最左归约法一定能求出范式。首先考虑归约过程问题。在一个表达式中可包含多个归约基，因此，归约过程不唯一，而且不同的归约过程也可能得到不同的计算结果。当然也可能都得到同一个结果。图 1.1.1 是有多个归约过程，但得到同一结果的例子。 ( λy.y((x((λa.a)))(λb.b) ( λy.y((λa.xa)(λa.a)))(λb.b) ( λb.b((λa.xa)(λa.a)) (λb.b)(x (λa.a)) (λa.xa)(λa.a) (λb.b)(x(λa.a)) x(λ.aa) 考虑有多个归约过程，并且不同归约过程得到不同结果的例: 图 1.1.1 归约过程例图 (λx.y)((λx.xx)(λx.xx)) 如果先归约(λx.xx)(λx.xx)，则将无休止地变换下去，但如果先归约(λx.y)(....)部分，则归约一次即可得到范式 y。这个题的特点是函数(λx.y)并不真正用到实参值，因此会得到上述结论。如果一定要首先计算实参然后再计算函数体的值，那么就会出现以上问题。下面是无范式的例子: (1) (λx.xx)( λx.xx) β⎯ →⎯ (λx.xx)( λx.xx) β⎯ →⎯ ..(不终止) (2) (λx.xxx)(λx.xxx)(λx.xxx) β⎯ →⎯ (λx.xxx)(λx.xxx)(λx.xxx) β⎯ →⎯ ........(不终止) 定义 1.1.13 （变换符号约定）： (1) x ⇒ y :经过有限次变换(α,β,η)，x变换为y。 (2) x ⇒r y :经过有限次归约(β,η)，x变换为y。 (3) x ⇒α y :经过有限次α变换，x变换为y。定理 1.1.14 （Church-Rosser）：如果 A⇒x 和 A⇒y 成立，则一定存在 z 使得 x⇒z 和 y⇒z 成立。证明.(略) - 5 - 批注 [½ð³ÉÖ²1]:

定理 1.1.15 （范式唯一性）：如果把通过α变换可互换的表达式视为一种表达式，那么如果 Lambda 表达式 E 存在其范式，则其范式一定唯一。证明：假设表达式 E 有两个范式 x 和 y，则根据 Church-Rosser 定理，一定存在表达式 z，使得 x⇒z 和 y⇒z 成立。因为 x 和 y 是范式，只能 x⇒αz，y⇒αz 。而α变换是双向的，因此有 x⇒αy，也就是说范式 x 和 y 是同一种 Lambda 表达式。定义 1.1.16 (标准归约)：如果每次归约最左的归约基，则称这种归约为标准归约。定理 1.1.17 ：如果表达式 E 有范式，则按标准归约一定能求到其范式。证明:略。 1.1.3 Lambda 演算能力前面介绍了 Lambda 演算系统的基本概念。Lambda 演算系统主要由 Lambda 表达式和 Lambda 变换规则组成。Lambda 变换的主要作用是用来导出表达式的范式。Turing 机系统能够描述部分递归函数的计算过程的事实，在可计算理论里已得以证实。那么 Lambda 演算系统有无同样的功能 ? 这就是将要回答的问题，其结论是能。在 Turing 机系统里有所谓的"带"，它是 Turing 机的操作对象，操作结果将改变带的内容。带由很多有序方格组成，在每个方格里可写所允许的符号。带的内容究竟表示什么意思?系统本身并不知道，系统只知道在什么状态下做什么动作。系统只提供一种用于演算的形式规则，带的内容究竟表示什么意思只有用户自己才知道。在 Lambda 演算系统中， Lambda 表达式相当于 Turing 机中的带，它们扮演着操作对象的角色。Lambda 表达式的结构非常简单，但它的功能和当代计算机的功能是一样大。我们将非严格地证明 Lambda 演算系统可模拟部分递归函数的计算过程，主要说明以下几点:可模拟非负整数；可模拟函数 +、*、and、or、＜、≤ 等；可模拟复合函数；可模拟条件函数 if_then_else ；可模拟递归。 [模拟自然数] 在这里将用如下λ-表达式来模拟整数 n: λab.a(a(......(a(a(ab)))) 其中a的个数为n个。我们将它简写成λab.anb，注意anb是右结合的简写。若用 n 表示整数n 的相应模拟表达式（函数），则有 0 = λab.b 1 = λab.ab 2 = λab.a(ab) = λab.a2b (右结合) n = λab.(a(a(a...(ab)......)) = λab.anb (右结合) [模拟算术运算] 设 f 是给定 i 元函数，并且下式成立 - 6 -

f 1m 2m ... mi = ,m f(m 21 ,...,mi ) （*）则称 f (Lambda 表达式)为 f 的模拟函数。假设用 PLUS 和 MULT 分别表示+和*的模拟函数，则根据（*）的定义应分别满足条件： PLUS m n = nm + nm * MULT m n = 事实上，只要将模拟函数PLUS和 MULT分别定义为 PLUS = λxy.λab.(xa)((ya)b) MULT = λxy.λa.x(ya) 即可满足（*）条件，因为有 PLUS m n = (λy.λab.( m a)((ya)b)) n = λab.( m a)(( n a)b) = λab.(λb.amb)(an b) = λab.am+n b = nm + MULT m n = (λy. λa. m (ya)) n = λa. m ( n a) = λa.( λab.am b)( λb.an b) = λa.( λb.( λb.a n b)m b) = λab.am n b = nm × [模拟逻辑运算] 我们将逻辑运算 and、or 和 not 的模拟函数分别表示为 AND、OR 和 NOT。首先要模拟逻辑值 true 和 false。若用 T 和 F 来表示相应模拟函数，则只要将它们定义为如下即可: T = λab.a (取第一个) F = λ ab.b (取第二个) 注意它们和整数的模拟数并不矛盾。其次，我们来构造逻辑运算and、or和not的模拟函数 AND、OR和NOT，它们需满足下面条件: AND x y = if x=T and y=T then T else F OR x y = if x=T or y=T then T then F NOT x = if x=F then T then F 事实上只要令 AND = λxy.(xyF) OR = λxy.(xTy) - 7 -

NOT = λx.(xFT) = (λy.TyF)T = (λy.y)T = T 即可满足上述条件，因为有 AND T T = (λxy.xyF)TT AND T F = (λxy.xyF)TF 同样可以证明有 (AND T F = F)。再考虑 OR 的问题，需要证明： AND F T = (λxy.xyF)FT AND F F = (λxy.xyF)FF = (λy.TyF)F = (λy.y)F = F = (λy.FyF)T = (λy.F)F = F = (λy.FyF)T = (λy.F)T = F OR T T=T, OR T F=T, OR F T=T, OR F F=F = (λy.TTy)T = (λy.T)T = T 事实上有 OR T T = (λxy.xTy)TT OR F T = (λxy.xTy)FT 用同样的方法可以证明有 (NOT T = F)(NOT F=T)。 = (λy.FTy)T = (λy.y)T = T = (λy.FTy)T = (λy.y)T = T OR F T = (λxy.xTy)FT OR F F = (λxy.xTy)FF = (λxy.xTy)FF = (λy.y)F = F [模拟关系运算] 最后考虑关系运算<和≤ 的模拟。为此首先定义一函数 ISZERO，它是一元函数，如果自变元值为0 ，则回送 T 值，否则回送 F 值。该函数的具体定义如下: ISZERO = λx.x(TF)T 其中x取 0 或1 。事实上有 ISZERO 0 = 0 (TF)T=(λab.b)(TF)T=(λb.b)T=T ISZERO 1 = 1 (TF)T=(λab.ab)(TF)T=(λb.(TF)b)T=(TF)T=F 因此 ISZERO是0 的判定函数。另外再假定 MINUS 是减法运算的模拟函数，即有 MINUS 1n 2n = 2 1 n n − ，当 n1 ≤ n2 = 0 ，当 n1 < n2 若用LT和 LE分别表示 < 和 ≤ 的模拟函数，则只要利用 ISZERO 和 MINUS 把LT和 LE 定义成如下即可: LE = λm n. ISZERO( MINUS( MINUS m n )( MINUS( MINUS m n )1 )) LT = λm n. AND( LE m n)( NOT (EQ m n)) - 8 -

分享到：

赞收藏

资料库

软件开发形式化方法教材.pdf

相关推荐

课程资源

热门标签

最新资料