我要投搞

标签云

收藏小站

爱尚经典语录、名言、句子、散文、日志、唯美图片

当前位置:2019跑狗图高清彩图 > 指称语义 >

形式语义教材-Ch1 基本理论

归档日期:07-16       文本归类:指称语义      文章编辑:爱尚语录

  1941年Church 创建了Lambda 演算理论。它是一个形式系统,可作为计算模型,如同 Turing 机可作为计算模型一样。Lambda 演算形式系统主要由两部分组成:其一是合法表 达式的形式系统,其二是变换规则的形式系统. Lambda 演算系统可有多种。其主要区别在于构成Lambda 演算形式系统的两个组成 部分的具体定义上。不同的Lambda 演算系统会得到一些不同的定理。Lambda 演算系统 如同Turing 机系统一样,可描述任何一部分递归函数的计算过程。因此,Lambda 演算系统 也可视为一种算法语言系统。其中的Lambda 表达式相当于语言的一个程序。程序如何 执行,由Lambda 演算系统的机制来确定。Lambda 演算理论是函数式语言的基础,也是指 称语义学的理论基础。 1.2 Lambda 演算 纯Lambda 表达式(以后简称λ 表达式)是最小的一种表达式,主要由变量名和抽象符 以及括号等符号构成。若用X表示变量,用Exp表示纯Lambda表达式之集,则Exp 集的定义如下。 定义1.2.1. λ表达式 Exp,其中x 是变量名。 若E1Exp,E2Exp, 则E1 E2 Exp。 是变量,则x.E Exp。 Exp。若用BNF表示法,则可描述如下(x Var, E1E2 从上述定义可知纯_表达式是非常小的表达式,以致于不能再小。但它将成为_演算系统的基础。那么一个作为计算模型的形式系统应具备什么样的条件呢?很显然它起 码应具备二个条件:其一是它有很强的功能,以致于能够描述复杂的计算过程;其二是它应 非常小,以致于其语义是非常清楚的。当然实用性的系统,则应根据需求扩充相应的内容,但其前提是它们可变换为纯_表达式的形式。 在我们这里Lambda 演算系统主要是作为函数式语言和指称语义描述语言的基础。 设L为被描述的语言,L0 为描述L语义的语言,则我们称L0 为元语言。显然,元语言不能 是很复杂的,否则又可提出L0 语言的语义是什么?因此,元语言的基础应非常简单。而所 使用的实际元语言则应从简单语言逐步扩充而来,而且其语义是很清楚的。 在我们的_表达式中没有常量部分,而且变量是广义的,即它代表的也可以是一函 数。称形如(E1E2)的表达式为施用型表达式,称形如 .E的表达式为抽象型表达式。表达式(E1E2)相当于通常的函数调用f(E),其中f 是函数名。现在不一样的是E1 不一定是 一个函数名,可以是复杂的表达式,但必须是抽象表达式或代表函数的变量名,如 (X.f(X))((Y.Y)20 ),其中有三个施用型子表达式; (X.f(X))((Y.Y)20 抽象表达式主要是用来表示无名函数。通常的方法是首先定义函数名,然后再使用它,因此函数都有名,而抽象表达式则表示一无名函数。假设有函数说明func 然也可把上述函数的定义写成:f=X.X+1,并且也能方便地表示哪个是函数名,哪个是形参名,哪部分是函数体,其中表示其后的变量为形参变量。这种说明是定义了一个函数名 f。如果不想定义函数名,那么应该怎么办?这好办,只要直接用表达式X.X+1 即可了。这 就是抽象表达式的直接出因。我们称x.E中的E表达式为上述抽象表达式的体部分。 为了简单起见,以后将(XY)简写成XY。严格说的话,不能写成XY形式,因为这种写法, 使实现系统将无法识别XY是一个标识符还是两个标识符。但如果假设变量名均由一个 字母组成,则写成XY形式也能够分辨出来是X和Y的两个名字。因此我们以后在一般情 况下将写成XY的形式。 定义1.2.2. (记法约定) E1E2 E3...En (((E1E2)E3)...)En (左结合规则) x1x2...xn.E x1....xn.E1E2...En x1....xn.(E1E2...En) 1.2.1.下面是一些简单的_表达式例: x.y.xy (x.xy)y x.x xy.x xy.y (x.xx)(x.xx) xy.x(y) xy x(x.xy 单从表达式看,看不出任何意义,因为其中既没有常量也没有函数名,不知道是如何计算的。但不久我们将会看到这样一个非常简单的系统能够描述复杂的计算和推理过程。 定义1.2.3. 子表达式 设E是表达式,并用SUB(E)表示E的子表达式集,则定义 SUB(x)={ SUB(E1E2)=SUB(E1) SUB(E2){E1E2} SUB(x.E)={x.E} SUB(E) SUB( SUB(E)定义 1.2.4. 作用域 设有表达式x .E,则定义x 的作用域为其中的体表达式E部分。如若在E中包含 一个子表达式x.E1,则外层x 的作用域将不包含该子表达式部分。 定义 1.2.5. 自由出现 设x是表达式E中x 的一次出现,则称该出现为x 的一自由出现,如果在E中没有一 个子表达式x.E1 包含该x出现。非自由出现称为约束出现。 定义 1.2.6. 自由变量 称变量x 为表达式E的自由变量,如果E中至少有一个x 的自由出现。若用Free(E) 表示E的自由变量的集合,则E的自由变量集的具体定义如下: Free(x) Free(E1E2) Free(E1)Free(E2)Free(x Free(E)如果表达式E不包含自由变量,则称E为闭型表达式,否则称为开型表达式。下面将 定义所谓的代换[E0/x]E,它表示用表达式E0 去代换表达式E中所有x 的自由出现。解释 Lambda 演算系统的最基本的概念之一是这里所说的代换,因此,要确切地理解Lambda 算系统必须要熟悉代换的精确概念.定义 1.2.7. 代换[E0/x]E E1E2情形 E0/x](E1 E2 )〒([E0/x]E1) x.E情形:[E0/x xFree(E)yFree(E0)时:[E0/x](y.E)〒z.[E0/x][z/y]E xFree(E)yFree(E0))时 :[E0/x](y.E)〒y.[E0/x]E 给了一个表达式即可根据Lambda演算系统所定义的变换规则进行一系列的变换,其 结果有二种可能:一是不能进一步的归约;二是变换无终止地进行下去(相当于程序不终 止)。Lambda 变换是保结构和保值的变换,其中保结构是指变换后得到的仍然是-表达 不同的Lambda演算系统具有不同的变换规则,有的可能只有二个变换规则,有的可能 有三个变换规则,有的甚至可能有更多的变换规则。有的具有相同个数的变换规则,但变 换规则的内容可不一样。我们这里介绍的Lambda 变换规则只是其中的一种。 定义1.2.8. -表达式,x是变量,则称下面变换为 变换(其中Y不在 Free( x.E 从定义可看出α变换是保结构的一种变换,也是保值的。α 变换后所得新表达式的区 别仅在于更换了形参的名字。 Y.(ZY)2.X.((Y.YX)X) 非法α变换 非法α变换 定义 1.2.9. -表达式,则称下面变换为β变换(称β 变换规则的左部表达式为 变换是最重要的一变换,可没有其他一些变换,但不能没有β变换。因此,所有 不同 Lambda 演算系统都有这一β 变换。β 变换规则实际上是定义了函数调用的语义, 因为β 变换规则的左部是一函数调用部分。( x.E)E0 中的(x.E )为被调用函数,x 函数的形参,E0为实参。而[E0/x]E则表示把实参E0 代入到函数体E中的形参x 变换规则可以看出,和该变换密切相关的是演算系统关于代换[E0 义。因为不同的Lambda演算系统可能有不同的定义。它们的区别之一在于所定义的代 换系统是否在代换时完全自动地进行改名(避免名字冲突)。如果代换系统没有自动改名 的功能,则β 变换规则应加一条限制,即不允许名字有冲突,因为如果有名字冲突的 话,该变换将不能是保值变换。我们所定义的代换系统具有自动改名的功能,因此,对 ABC定义 1.2.10. 变换假设 x.Mx 是一个表达式,且满足条件xFree(M),则称下面变换为η 变换: (x.M 故有(x.Mx)=M,也就是说η 变换规则左右部表达式是等值表达式。有些Lambda演算 系统就没有这一种变换规则,也就是说η 变换不是演算系统所必需的变换规则。 (Y.YYX)非法变换 定义 1.2.11. Lambda 归约 基统称为归约基。 定义1.2.12. 范式 假设E是一个表达式,且其中没有任何一个归约基,则称该表达式为范式。如果一个 表达式经过有限次变换能归约成范式,则称该表达式有范式. 1.2.5.下面是范式例 XXX.XX X(X.XX)X.X(Y.XY) X.X((Y.X)Y)不是范式现在要考虑的问题是,表达式是否都有范式?若有,是否唯一?范式应该如何求?下面将 说明以下一些问题:归约过程不唯一;表达式不一定都有范式;如果有范式一定唯一;如果有 范式,则最左归约法一定能求出范式。 首先考虑归约过程问题。在一个表达式中可包含多个归约基,因此,归约过程不唯一, 而且不同的归约过程也可能得到不同的计算结果。当然也可能都得到同一个结果。图 1.2.1 是有多个归约过程,但得到同一结果的例子。 考虑有多个归约过程,并且不同归约过程得到不同结果的例: (x.y)(( x.xx)( x.xx)) 如果先归约(x.xx)( x.xx),则将无休止地变换下去,但如果先归约(x.y)(....)部分, 则归约 一次即可得到范式Y。这个题的特点是函数(x.y)并不真正用到实参值, 因此会得到上述 结论。如果一定要首先计算实参然后再计算函数体的值, 那么就会出现以上问题。下面 是无范式的例子: (X.XX)(X.XX) X.XX)(X.XX) ..(不终止)(X.XXX)( X.XXX) X.XXX)(X.XXX)( X.XXX) ........(不终止)x(.aa) (b.b)(x (a.a)) (b.b)(x(a.a) 定义1.2.13. :经过有限次α变换,X变换为Y。 定理 1.2.14. Church-Rosser 若有AX和 AY成立,则定存在Z使得下式成立: 证明.(略)定理 1.2.15. 范式唯一性 如果把可通过α 变换互换的表达式视为一种表达式,那么有下面结论,即假设E是 表达式且有范式,则该表达式的范式一定只有一种(唯一)。 证明:假设表达式A有两个范式X和Y,则根据Church-Rosser 定理,一定有表达式 Z,使得下式成立: XZ,YZ。因为X和Y是范式,只能X 变换是双向的,因此有X Y,也就是说范式X和Y是同一种。定义 1.2.16. 标准归约 如果每次归约最左的归约基, 则称这种归约为标准归约。其中最左是按归约基中 符号的出现顺序而言的。 定理1.2.17. 如果表达式E有范式,则按标准归约过程一定能求到其范式。 证明:略。 1.3 Lambda 演算可作为计算模型 前面介绍了Lambda 演算系统的基本概念。Lambda 演算系统主要由表达式和变换 规则组成。 变换的主要作用是用来导出表达式的范式。Turing 机系统能够描述部分递 归函数的计算过程的事实,在可计算理论里已得以证实。那么Lambda 演算系统有无同 样的功能 这就是将要回答的问题,其结论是能。在Turing 机系统里有所谓的带,它是Turing 机的操作对象,操作结果将改变带的 内容。带由很多有序方格组成,在每个方格里可写所允许的符号。带的内容究竟表示什 么意思?系统本身并不知道,系统只知道在什么状态下做什么动作。系统只提供一种用 于演算的形式规则,带的内容究竟表示什么意思只有用户自己才知道。 在Lambda演算系统中, -表达式相当于Turing 机中的带,它们扮演着操作对象的 角色。纯-表达式的结构非常简单,但它的功能和当代计算机的功能是一样大的。我们将 非严格地证明Lambda 演算系统可模拟部分递归函数的计算过程,主要说明以下几点:可 模拟非负整数;可模拟函数 可模拟复合函数;可模拟条件函 数if_then_else ;可模拟递归。 在这里将用如下-表达式来模拟整数n: ab.a(a(......(a(a(ab)))) 其中a的个数为n个。我们将它简写成ab.a 是给定n元函数,则称表达式 m1m2... mn (m1,m2, mn)作为简单二元函数的代表考虑+、、and、or、

  主 要是不满足关系的自反性。 是任意的集合,且用pow( )表示由S的所有子集组成的集合即S 集,则(pow(S),)将构成一个半序集。其中表示通常的集合包含关系,具体定义如下: 定义1.5.3.上界,下界 设(D,)是任一半序集,且D D,d0D,则子集D的上界和下界的定义如下: 上界 :若对任意dD,都有dd0,则称d0 为D的上界。 下界 :若对任意dD,都有d0 为D的下界。定义1.5.4. 最小上界,最大下界 设(D,)是任一半序集,且D D,则子集D的最小上界和最大下界的定义如下:最小上界: 设d是D的一个上界。若对D的任一上界d,都有关系dd 成立,则 最大下界:设d是D的一个下界。如果对于D的另一个任意下界d,都有关系d d,则称d为D的最大下界,并记为D 定理1.5.5.唯一性 设(D,)是任一半序集,且D D。若D存在最小上界,则定唯一。最大下界也同样如此。 证明: 假设D有二个最小上界d1 和d2,则由于d1 是最小上界,有d1d2。同理, 由于d2 是D的最小上界,有d2d1。但因为(D,)是半序集,具有反对称性质,因 此有d1=d2。 定义1.5.6. 设(D,)是一半序集,

  是D上的一序列,简记为{Xi 则递增链和递减链的定义分别如下: 若对任意i都有XiXi+1,则称序列{Xi}为递增链。 若对任意i都有Xi+1Xi,则称序列{Xi}为递减链。 链{Xi}的最小上界表示成{Xi} 定义1.5.7.完全半序集( CPO集) 设(D,)是一半序集,若满足下面两个条件,则称(D,)为完全半序集:一是D有最小 元;二是对于D上的任一递增链{Xi}都有其最小上界 {Xi} 我们将会看到完全半序集(或后面要讲的完全格)是重要的集合。在形式地描述语言的语义时,总假定所考虑的集合满足完全半序集的条件,并把这种定义了关系的集合称为 论域。 若D表示开区间(a,b)实数集,则(D,)不是完全半序集。定义1.5.8. 格,完全格 设(D,)是半序集,则格和完全格的定义分别如下:(1)若D的任一非空有穷子集S ,则称(D,)为格;(2)若D的任一子集S都有最小上界 定理1.5.9.设(D,)是完全格,则D的任一子集S,都有最大下界。 证明: 留给读者。 定理1.5.10. 证明:留给读者。这条定理表示完全格的要求比完全半序集的要求还高。目前所见到的论域的数学模 型主要有两种,其一是完全半序集,其二是完全格.我们这里则采用完全半序集这一数学模 定义1.5.11.平坦集 设(D,)是一半序集,若满足下面两个条件,则称(D,)为平坦半序集,或简称为平坦 D有最小元(记为);(2)只有下面关系:,d, dd。其中d 是D上的元素。 以后将会看到平坦集是非常有用的一种域。从下面定理将会知到任何平坦集都是完 全半序集,因此有时将域定义成平坦集以得到所需的完全半序集。任给集合D,则构造平 坦集的方法非常简单,只要引进一个最小元(记为D),并在集合D{D}上定义平坦关系 即可。以后将符号D 来表示按上述方法用D和构成的平坦集。定理1.5.12. 设(D,)是一平坦集,则(D,)定是完全半序集(CPO集)。 证明:平坦集有最小元,因此只需证明D上的任何一个链{Xi}都有最小上界。事实 上,D上的任何链只能是下面三种情形之一: 其中第一种情形的最小上界为,第二种情形的最小上界为d,第三种情形的最小上界也是d,故定理得证。 定理1.5.13. 假设(D,)是完全半序集,Xij(i,j

  0)是D中元素,且当ik,jl 时有XijXkl,则有: Xij i+1,j)可导出 Xi, 定存在。同理,可证明Xij 存在。其次证明等式,由XijXij可导出Xij Xij ,进而再可导出Xij 同理可证明上述关系的逆关系,从而证明:Xij 。其次,证明本定理中的第二个等式,即 Xij i,j:XijXkk ,由此可导出Xij 进而又可导出Xij k:XkkXij 故可导出关系Xkk 现在开始我们把论域理解为完全半序集。这一节考虑如何从已知论域构造出新的论域的(完全半序集)问题。主要考虑Scott 所给出的论域的构造符,+,*,等。论域理论中 的最主要问题是论域的递归定义。Scott 首先解决了这个问题和函数的递归定义问题,从 而为指称语义学奠定了坚实的理论基础。由于篇幅所限,我们将省略有关论域的递归定义 理论方面的内容。有兴趣者可参考有关文献。 定义1.5.14. 元组域 Product[D1D2...Dn] 设(Di,1)是半序集,i=1,..,n,则定义(D1...Dn,)域如下: [D1...Dn] (d1,...dn)(d1,d2...dn)iff dii di 称(D1D2..Dn,)或[D1D2..Dn]为n元组域(或乘积域或卡氏域). 定理1.5.15. 设(D1D2...Dn,)是按上述定义构造出来的n 元组域,且对每个i,(Di,i)是完 元组域也是完全半序集。证明:

本文链接:http://capstonebake.com/zhichenyuyi/278.html