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

1、第一章理论基础§ 1.1引言1941年church创建了 lambda演算理论。它是一个形式系统，af作为计算模型，如同 turing机可作为计算模彻一样。lambda演算形式系统主要由两部分纟11成:其一是合法表 达式的形式系统，其二是变换规则的形式系统.lambda演算系统可有多种。其主要区别在于构成lambda演算形式系统的两个组成 部分的具体定义上。不同的lambda演算系统会得到一些不同的定理。lambda演算系统 如同turing机系统一样，可描述任何一部分递归函数的计算过程。因此,lambda演算系统 也可视为一种算法语言系统。其屮的lambda表达式相当于语言的一个程

2、序。程序如何 执行，由lambda演算系统的机制來确定。lambda演算理论是函数式语言的基础，也是指 称语义学的理论基础。§ 1.2 lambda 演算纯lambda表达式(以后简称x表达式)是最小的一种表达式，主要由变量名和抽象符 号入以及括号等符号构成。若用x表示变量，用exp表示纯lambda表达式之集，则exp 集的定义如下。定义1.2.1. x表达式(1) x eexp，其中x是变量名。(2) 若 eieexp, e2eexp，贝ij el e2 expy(3) 若 e eexp, x是变量，wjxx.e gexp。 若 e eexp，贝(j (e ) eexp。若用bn

3、f表示法，则可描述如下(x evar, e eexp ):e :=x | e1e2 | xx.e |(e)从上述定义可知纯表达式是非常小的表达式，以致于不能再小。但它将成为人_演 算系统的基础。那么一个作为计算模型的形式系统应具备什么样的条件呢?很显然它起码应具备二个条件:其一是它有很强的功能，以致于能够描述复杂的计算过程;其二是它应 非常小，以致于其语义是非常清楚的。当然实用性的系统，则应根据需求扩充相应的内容， 但其前提是它们可变换为纯?1_表达式的形式。在我们这里lambda演算系统主要是作为函数式语言和指称语义描述语言的基础。没l为被描述的语言,l0为描述l语义的语言，则我们称l0为元

4、语言。显然，元语言不能 是很复杂的，否则又可提山l0语言的语义是什么？因此，元语言的基础应非常简单。而所 使用的实际元语言则应从简单语言逐步扩充而来，而且其语义是很清楚的。在我们的人_表达式屮没有常量部分，而且变量是广义的，即它代表的也可以是一函 数。称形如(e1e2)的表达式为施用型表达式，称形如xx.e的表达式为抽象型表达式。表 达式(e1e2)相当于通常的函数调用f(e)，其中f是函数名。现在不一样的是e1不一定是 一个函数名,可以是s杂的表达式，但必须是抽象表达式或代表函数的变量名，如 (zx.f(x)(?iy.y)20 )，其中有三个施用型子表达式；(入y.y)20 f(x) (xx

5、.f(x)( (xy.y)20 )抽象表达式主要是用來表示无名蚋数。通常的方法是首先定义蚋数名，然后再使用它， 因此函数都有名，而抽象表达式则表示一无名函数。假设有函数说明fuikf(x)=x+l，则显 然也可把上述函数的定义写成:f=xx.x+l，并且也能方便地表示哪个是函数名，哪个是形参 名，哪部分是函数体，其中x表示其后的变量为形参变量。这种说明是定义了一个函数名 f。如果不想定义函数名，那么应该怎么办?这好办，只要直接用表达式xx.x+1即可了。这 就是抽象表达式的直接出因。我们称xx.e中的e表达式为上述抽象表达式的体部分。为了简单起见，以后将(xy)简写成xy。严格说的话，不能写成

6、xy形式，因为这种写 法，使实现系统将无法识别xy是一个标识符还是两个标识符。但如果假没变量名均由一 个字母组成，则写成xy形式也能够分辨出来是x和y的两个名字。因此我们以后在一 般情况下将写成xy的形式。定义1.2.2.(记法约定)(1) el e2 e3.en=(el e2)e3)en (左结合规则)(2)入xl.a.xn.e=xx 1 .(.(xxn.en).)(3)入xl x2.xn.e=xxl.xx2.x.xn.e(4) xxl.a.xn.e1 e2en=xxl.x.xn.(el e2.en)xx.x(xx.xx)(xx.xx) x(入x.xy)例1.2.1.下面是一些简单的表达式例

7、: xx.xy.xy(xx.xy)y入 xy.x人 xy.y入 xy.x(y)xy单从表达式看，看不出任何意义，因力其中既没有常量也没有函数名，不知道是如何计 算的。但不久我们将会看到这样一个非常简单的系统能够描述杂的计算和推理过程。定义1.2.3.子表达式设e是表达式，并用sub(e)表示e的子表达式集，则定义sub(x)= x sub(e1 e2)=sub(e1)u sub(e2)ue1 e2sub(xx.e)=xx.e usub(e)sub(e) )= e u sub(e)定义1.2.4.作用域设有x表达式xx .e，则定义xx的作用域为其中的体表达式e部分。如若在e中包含 一个子表达式

8、xx.el，则外层xx的作用域将不包含该子表达式部分。定义1.2.5.自由出现设x1是表达式e中x的一次出现，则称该出现为x的一自由出现，如果在e中没有一 个子表达式xx.el包含该x出现。非自由出现称为约束出现。定义1.2.6.自由变量称变量x为表达式e的自由变量，如果e屮至少有一个x的自由出现。若用free(e) 表示e的自由变量的集合，则e的自由变集的具体定义如下：free(x)= x free(el e2)= free(el)ufree(e2)free(入x .e)= free(e ) x free( (e)= free(e)如果表达式e不包含自由变量，则称e为闭型表达式，否则称为开型

9、表达式。下面将 定义所谓的代换eo/xe，它表示用表达式e0去代换表达式e中所有x的自由岀现。解释 lambda演算系统的最基本的概念之一是这里所说的代换，因此，要确切地理解lambda演 算系统必须要熟悉代换的精确概念.定义 1.2.7.代换eo/xe:eo/x jx: eo:eo/x yzy (x关y):eo/x (e1 e2 )z(e0/xel)( e0/xe2) :eo/x (入x .ezx.e*e = x情形(2) ey情形(3) e = e1 e2 情形(4) e = xx.e情形(5) 入y.e情形(x¥y):x e free(e)八y e free(eo)时 xfre

10、e(e')v y 茫 free(eo)时:eo/x(xy.e,)zxz.eo/xz/ye, :reo/xl(xy.e,)zxy.eo/xle,给了一个表达式即可根据lambda演算系统所定义的变换规则进行一系列的变换，其 结果有二种可能:一是不能进一步的归约;二是变换无终止地进行下去(相当于程序不终 止)。lambda变换是保结构和保值的变挽，其中保结构是指变换后得到的仍然是x-表达 式。不同的lambda演算系统具有不同的变换规则，有的可能只有二个变换规则，有的可能 有三个变换规则，有的其至可能有更多的变换规则。有的具有相同个数的变换规则，但变 换规则的内容可不一样。我们这里介绍的l

11、ambda变换规则只是其中的一种。定义1.2.8. a变换设e是x-表达式，x是变fi,则称下而变换为a变换(其中y不在free(xx.e) 中)。入x.e xyjy/xl e从定义可看出a变换是保结构的一种变换,也是保值的。a变换后所得新表达式的区 别仅在于更换了形参的名字。例 1.2.2.(y1 xx.(zx) xy.(zy)2ax.(y.yx)x)xz.(?ty.yz)z)3. 入x.(z(?iy.x)a > xy.(z(zy.y ):非法 u 变换4. 入x.(zy)a > xy.(zy):非法 u 变换定义1.2.9. (p变换)设(xx.e)和e0力x-表达式，则称下而

12、变换为p变换(称变换规则的左部表达式力 p基)o(xx.e)eoleo/x e3变换是最重要的一变换，可没有其他一些变换，但不能没有p变换。因此，所有 不同lambda演算系统都有这一 p变换。p变换规则实际上是定义了函数调用的语义， 因为0变换规则的左部是一"函数调用"部分。(xx.e)eo中的(xx.e)为被调用函数，x为函数的形参，e0力实参。而leo/xje则表示把实参e0代入到函数体e中的形参x巾，这 正是熟知的函数调用过程。由p变换规则可以看出，和该变换密切相关的是演算系统关于代换e0 / x e的定 义。因为不同的lambda演算系统可能有不同的定义。它们的区

13、别之一在于所定义的代 换系统是否在代换吋完全自动地进行改名(避免名字冲突)。如果代换系统没有自动改名 的功能，则(3变换规则应加一条限制，即不允许名字有冲突，因为如果有名字冲突的 话，该变换将不能是保值变换。我们所定义的代换系统具有自动改名的功能，因此，对 于p变换规则不需要加上述限制。例 1.2.31. (xx.xy)a ay2. (xy.yx)a ax3. (xx.xx)a aa4. (xx.(xy.(入z.xyz)abc 入y.(?iz.ayz)bc(xz.abz) c abc定义1.2.10. ii变换假设xx.mx是一个表达式，且满足条件xgfree(m),则称下而变换为n变换:(x

14、x.m x) mn变换也是一种保值变换。其主要依据是函数的外延(保値)等价性定义，即 vf(x)=h(x)f=h。事实上我们有v(y) (xx.mx)y = my 故有(xx.mx) =m，也就是说n变换规则左右部表达式是等值表达式。有竖lambda演算 系统就没有这一种变换规则，也就是说n变换不是演算系统所必需的变换规则。例 1.2.4.xx .( xy.yyy)x(xy.yyy)xx .( xy.yyx)x(xy.yyx)非法变换定义 1.2.11. lambda 归约(1) p变换的左部表达式(xx.e)eo称之为爲基。(2) n变换的左部表达式(xx.mx)称之为n基。(3) 把(3基

15、和n基统称为归约基、(4) 对表达式中的某一归约基施行某种变换称之为归约.定义1.2.12. 范式假设e是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。如果一个 表达式经过有限次变换能归约成范式，则称该表达式有范式.例1.2.5.下而是范式例 x axx 人x.xx x(xx.xx) axx.x(xy.xy)入x.x(xy.x)y)不是范式现在要考虑的问题是，表达式是否都有范式?若有，是否唯一?范式应该如何求?下面将 说明以下一些问题:归约过程不唯一;表达式不一定都有范式;如果有范式一定唯一;如果有 范式，则最左归约法一定能求山范式。首先考虑归约过程问题。在一个表达式屮可包含多个归

16、约基，因此，归约过程不唯一， 而且不同的归约过程也可能得到不同的计算结果。当然也可能都得到同一个结果。图 1.2.1是有多个归约过程，但得到同一结果的例子。考虑有多个归约过程，并且不同归约过程得到不同结果的例: (xx.y)( xx.xx)(入x.xx)如果先归约(xx.xx)( xx.xx)，则将无休止地变换下去，但如果先归约(xx.y)(.)部分，则归约 一次即可得到范式y。这个题的特点是函数(:u.y)并不真正用到实参值，因此会得到上述 结论。如果一定要首先计算实参然后再计算函数体的值，那么就会出现以上闷题。卜面 是无范式的例子： (xx.xx)( xx.xx) xx.xx)(入x.xx

17、)ax.xxxx xx.xxx) (入x.xxxx 入x.xxxx xx.xxx)(不终止)定义 1.2.13.(1) x=>y :经过有限次变换()，x变换为y。(2) x=>ry :经过有限次归约(p , n )，x变换为y。(3) x=>ay :经过有限次a变换，x变换为y。定理 1.2.14. church-rosser若有a=>x和a=>y成立，则定存在z使得下式成立:x=>z和y=>zo 证明(略)定理1.2.15.范式唯一性如果把可通过a变换互换的表达式视为一种表达式，那么有下面结论，即假设e是 表达式且有范式，则该表达式的范式一定只有一

18、种(唯一)。证明：假设表达式;a有两个范成x和y，则根掘church-rosser定理，一定有表达成 z,使得下式成立:x=>z, yzo因为x和y是范式，只能x=>az,y=>az。而a变换 是双向的，因此有x=>ay，也就是说范式x和y是同一种。定义1.2.16.标准归约如果每次归约最左的归约基，则称这种归约为标准归约。其屮最左是按归约基屮入 符号的山现顺序而言的。定理 1.2.17.如果表达式e有范式，则按标准归约过程一定能求到其范式。证明:略。§1.3 lambda演算可作为计算模型前面介绍了 lambda演算系统的基本概念。lambda演算系统主要由

19、x表达成和x变换 规则组成。x变换的主要作用是用來导出表达式的范式。turing机系统能够描述部分递 归函数的il算过程的事实，在可il算理论里已得以证实。那么lambda演算系统有无同 样的功能？这就是将要回答的问题，其结论是能。在turing机系统里有所谓的"带' 它是turing机的操作对象，操作结果将改变带的 內容。带由很多有序方格组成，在每个方格里可写所允许的符号。带的内容究竞表示什 么意思?系统本身并不知道，系统只知道在什么状态下做什么动作。系统只提供一种用 于演算的形式规则，带的内容究竟表示什么意思只有用户自己才知道。在lambda演算系统中，x-表达式相当于t

20、uring机中的带，它们扮演着操作对象的 角色。纯x-表达式的结构非常简单，但它的功能和当代计算机的功能是一样大的。我们将 非严格地证明lambda演算系统可模拟部分递归函数的计算过程，主要说明以下几点:可 模拟非负整数;可模拟函数+、*、and、or、等；可模拟复合函数;可模拟条件函 数if_then_else ;可模拟逆归。在这里将用如卜x-表达式来模拟整数m xab.a(a(a(a(ab)其中a的个数为n个。我们将它简写成xab.anb(定要注意anb是右绍合的简写)。若用n表 示整数£的相应x-表达式，则有0 = xab.b1 = xab.ab2 = xab.a(ab) =

21、xab.ab (右结合)n 二入ab.(a(a(a(ab) = xab.anb (右结合)设f是给定n元函数，则称表达式f为f的x-表达式，如果下式成立f ml m2.mn z f(ml,m2,.,mn)作为简单二元函数的代表考虑+、x、and、or、等运算。我们将对这些运算构 造满足上述条件的v表达式。首先考虑算术运算+和*的模拟闷题。假设所求+和x的模拟函数分别为plus和 mult，则它们应满足下面条件：time m n m x n事实上，只要令plus和mult的x-表达式分别为如下即可: plus= xxy. ab.(x a)(y a)b)timexxy. xa.x(y a)闪为有p

22、lus m n z(xy. xab.(ma)(ya)b)n=xab.(ma)(na)b)zxab.(xb.amb)(anb)zzab.anunb m + nmult m n z(xy. xa.m(ya)nzxa.m(na)=xa.( xab.amb)( xb.an b) =xa.( xb.( xb.anb)mb) zxab.amnb z mxn下而考虑布氺运算的模拟问题。假设布尔运算and、or和not的模拟函数分别为 and、or和not。首先模拟布尔值true和false。若用t和f来表示相应模拟函数，则 它们可定义成如下：t 二xab.a (取第一个)f zxab.b (取第二个)注意它

23、们和整数的模拟数并不矛盾。接着考虑and、oi和not的模拟。它们的模拟函数 and、or和not只耑满足下面条件：and x yzifx=t & y=t then telsefor xyzifx=t or y=t then telsefnot xzifx=f then t else f事实上只要令andsxxy.(xyf), or 二人xy.(xty)，notsxx.(xft) 即可满足上述条件，读者不妨验证一下。最后考虑关系运算和的模拟。首先定义一函数iszero,它是一元函数，如果 ii变元值为0,则回送t值，否则回送f依。该函数的具体定义如下：iszero = xx.x(tf)

24、t其中x取5或。我们假定minus是减法运算的x-表达式：minus n 1 n2 z nl - n2，当nl>n2 =0，当 nl<n2若用lt和le分别表示 <和彡的x-表达式，则只要如下定义lt和le即可：le z xm n. iszero( minus( minus m n )( minus( minus m n )1 ) lt = xin n. and( le m n)( not (eq m n)其中eq是等式运算的x-表达式：eq =入 mn.and ( le m n)( le n m)用lambda表达式模拟复合函数和条件函数首先考虑下面简单的复合函数例子： f

25、(x,y) = h( g(x), r(y)_并假定h，g和表达式分别为h, g和r (己知)，即有h m n z h(m, n) g m = g(m) r n = r(n)fjl在我巧造表达式使得f mn = f(m，n)成立。事实上，只要令 f =xxy.h(g a：)(r y)则有：f m n z h(g m)(r n)=h g(m) r(n)= h(g(m)，r )z f(m,n)下而考虑用v表达式模拟if-then-else的问题，这是很简单的问题。假设有 条件函数：f(x,y) zif b(x,y) then g(x,y) else h(x,y)则只要如下定义f即可：f =入xy.(

26、b xy )( g xy )( h xy )。用入表达式模拟不动点算子u假设有递归函数f的定义f( x ) = if b(x) then el(x) else e2( f(x)则该递归方程定义了函数f。但递归方程可能有很多解，那么应取哪个为所要解?.其方法 之一是取最小不动点作为解。若有f(a)=a，则称该a为函数f的不动点，不动点算子u的性 质#对任一函(有f动点)有我们要模拟不动点算子构造的v表达 式ag有性质:af=f(af)。事实上，只要令/=xh.( a.r.h(r r)( xr.h(r r)则有juf = (zr.f(r r)( xr.f(r r)=f(xr.f(r r)( xr.

27、f(r r)_= f(ao因此，确实是不动点算子p的模拟函数。因为我们还没有讲到不动点的概念，因此， 不能说明更多的內容。§ 1.4 lambda演算系统的扩充前面介绍了最基本的lambda演算系统，同时表明了它能够描述部分递归函数的计 算过程。其中实际上只有一种操作，即函数的施用，也就是p归约。但其中连常数都没 有，因此，用起来很不方便，所以想扩充原来的lambda演算系统。扩充lambda演算系统的路子可很多，但可把它们分为以下三类:扩充v表达式：扩充x-变换系统；扩充数据类型。有的可能只扩充了某一方而，有的则也可能同时扩充了几个方而。下而我们不妨考 虑这样一种扩充，即引进两种类

28、型int和bool,于是变成了多类lambda演算系统。 另外，就足扩充v表达首先将引进标准函数(如add,mul，and，or，eq.)，这些标准函 数名代表系统所规定好的并完成指定操作的v表达式。其次增加条件表达式(e0-e1, e2)其中表达式e0的值应是bool类型的，如果取true值，则计算表达式e1的值，否则计 算e2的值。关于条件表达式我们已知能把它变为原lambda演算的表达式，因此其语义 不必再赘述。条件表达式的最一般形式有下面两种：1 ( e0->el，e0->e2，.，e0->en，e)2 ( e0-> e1 ,e0-> e2,.,e0-&g

29、t; en)其中1的®后一种情形是代表"否则"情形，即当eo的值不等于任何ei的值时该条件表达式 的位为e"的值。条件表达式21则表示如果e0的值不等于任何ei的伉，那么就算错误。再是增加let表达式:let x=e0 in eb。它的意思是“令eb屮变量x的值为e0的 值”。它的精确语义是什么？下面式子回答这个问题：(let x=e0 in eb)= (xx .eb)e0。被扩充的x-表达式的巴克斯范式的具体定义如下：e := false | true | n | x | f | (e) | el e2 | xx.e | (eo->e1,e2)|

30、 letx=eo in eb其中的f表示称准函数名，n是正整数。为了简单起见有时将省略类型名。现在有两种变 量，一是x变量，一是let变量。其屮人变量相当于过程式语言屮的形参变量，而let变量则 相当于过程体闪的临时变量。let x=e0 in eb的简单意思是n令eb屮的x为e0 "。下而是从扩展v表达式到原x-表达式的转换方法.tran :extlamexp -*lamexptran【false】=xab.btran【true】=入ab.atran【n 】=xab.anbtran【f 】=lambda(f)tran【(e)】=(tran【e 】)tran【x 】=xtran【el

31、 e2 】=(tran【el 】)(tran【e2 】)tran【xx. e 】=xx. (tran【e 】)tran【(eo一el, e2)】=(tran【eo】)(tran【el】)(tran【k2】) tran【let x =e0 in eb 】z (xx .tran【eb】 )(tran【eo】)这里需要说明的是，let表达式不但能定义一个变量，而且也可定义函数。换句话 说，let变量的值可以是一个函数。比如let u =xxy.(add y (sub y 1) in u 2 3 该表达式的计算结果是4。事实上有let u =?ixy.(add x (sub y 1) in u 2 3

32、=(xu.u 2 3)( xxy.add x (sub y 1)=(xxy.add x (sub y 1) 2 3 z (xy.add 2 (sub y 1) 3 =add 2 (sub 3 1)z add 2 2 =4§ 1.5前面介绍了最简单的形式系统一lambda演算系统，该系统能够描述很复杂的计算过 程，但用起来十分麻烦，它相当于单类代数。但通常的程序设计语言是多类型的，即相 当于多类代数，因此扩充系统是非常必要的。这里说的类型不是具体程序设计语言的类型，而是用来描述语言中类型的数学模型， 其最简单的理解恐怕是集合。但纯集合的概念不能很好地解决在程序的形式描述中所遇 到的问题

33、。最主要而复杂的问题是递归（函数的递归，类型的递归等）的形式描述。其中要求论域 满足一些性质，因此我们将要研宂有关论域的基本问题。论域理论是较复杂的问题，不是 一两句话能说得清楚的。随立场的不同对数据类型所采用的数学模型可能是不一样的,scott所建立的论域理论为形式语义学奠定了坚实的理论基础。他的出发点是把论域视为完全半序集(或完全 格)。定义1.5.1.半序集设d是任一集合，<是定义在d上的关系。若关系<是半序关系，则称(d，<)为半序 集。半序关系要满足下面三个性质：1) 自反性：vxed.(x彡x)2) 传递性：vx，y，zgd.( xy & y<zx&

34、lt;z )3) 反对称性:vx，y ed.( xy&yx o x=y )半序集的主要特点是，半序关系并不要求对于任意两个元素都成立，即有些元素之间 也可能根本不存在关系。因此，被称为半序关系(或偏序关系)。当考虑函数时，因为函数有 值，而值则有大小关系，因此函数的定义域和值域为半序集是起码的条件。例 1.5.1.(1) 数学上的<和>等构成半序关系，但<和等不能构成半序关系。其中<和主 要是不满足关系的自反性。(2) 设s是任意的集合，且用pow( s )表示由s的所有子集组成的集合即s的幂集，则(pcw(s)，彡)将构成一个半序集。其巾彡表示通常的集合包含关

35、系，具 体定义如下：vs, sepow(s), s彡siff s£s定义1.5.2. 全序集设(d，彡)是半序集。若d中的任意两个元素a和b都有半序关系a<b或b<a,则 称(d,<)为全序集。定义1.5.3.上界，下界设(d，<)是任一半序集，且d，do ed,则子集d1的上界和下界的定义如下：上界：若对任意ded，都有d<do,则称do为d1的上界。下界：若对任意ded，都有do<d*.则称do为ev的下界。定义1.5.4.最小上界，最大下界设(d,<)是任一半序集，且d'gd,则子集ev的最小上界和最大下界的定义如下： 最小上界

36、：设d是d"的一个上界。若对d的任一上界d，都有关系成立，则称d为d1的最小上界，并记为ud1。最大下界：设d是u的一个下界。如果对于d"的另一个任意下界d，都有关系d,则称d为d的最大下界，并记为nd1。定理1.5.5.唯一性设（d,）是任一半序集，且dgd。若cv存在最小上界，则定唯一。最大下界也同 样如此。证明：假设d*有二个最小上界dl和d2,则由于dl是最小上界，有dkd2。同理， 由于d2是d1的最小上界，有d2彡dl。但因为（d，彡）是半序集，彡具有反对称性质，因 此有dl=d2。定义1.5.6. 链设（d,）是一半序集，（）,乂1,.，11,.是d上的一序列

37、，简记为 xi ,则递增链和递 减链的定义分别如下：1）s对任意i都有xixi+1,则称序列xi为递増链集:一是d有最小元2）若对任意i都有xi+lxi,则称序列xi为递减链 链xi的最小上界表示成uxi或uixi或llxi定义1.5.7.完全半序集（0集设（d，）是一半序集，若满足下面两个条件，则利 二是对于d上的任一递增链xi j都有其最小上界lrm我们将会看到完全半序集（或后而要讲的完全格）是重要的集合。在形式地描述语言 的语义时，总假定所考虑的集合满足完全半序集的条件，并把这种定义了关系的集合称为 论域。例 1.5.2.（1）若d是任一有穷整数集，则（d，）将构成完全半序集。（2）有最

38、小元的有穷半序集是完全半序集。（3）若d表示开区间（a，b）实数集，则（d,）不是完全半序集。定义1.5.8.格，完全格设（d，彡）是半序集，则格和完全格的定义分别如下:若d的任一非空有穷子集s都 有最小上界us，则称（d，）为格;（2）若d的任一子集s都有最小上界lis，则称（d，匀为完 全格。定理 1.5.9.设（d，幻是完全格，则d的任一子集s，都有最大下界。证明：留给读者。定理 1.5.10.设（d，s）是完全格，则（d，s）是完全半序集。证明:留给读者。这条定理表示完全格的要求比完全半序集的要求还高。目前所见到的论域的数学模 型主要有两种，其一是完全半序集，其二是完全格.我们这里则采

39、用完全半序集这一数学模 型。定义1.5.11.平坦集设（d，s）是一半序集，若满足下面两个条件，则称（dx）力平坦半序集，或简称为平坦集:（1） d有最小元（记为丄）;（2 ）只有下面关系丄<丄.丄1，d<do其中d是d上的元素。以后将会看到平坦集是非常有用的一种域。从卜面定理将会知到任何平坦集都是完 全半序集，因此有时将域定义成平坦集以得到所需的完全半序集。任给集合d，则构造平 坦集的方法非常简单，只要引进一个最小元（记为丄d），并在集合丄d上定义平坦关系即 可。以后将符号d1来表示按上述方法用d和丄构成的平坦集。定理 1.5.12.设（d，幻是一平坦集，则（d，s）定是完全半序

40、集（cpo集）。证明:平坦集有最小元，因此只需证明d上的任何一个链xi都有最小上界。事实 上,d上的任何链只能是下面三种情形之一：（1）丄丄丄，>（2）<丄，丄，丄，d，d，d，.>（3）<d ,d ,d，d,d,d，>其中第一种惜形的最小上界为丄，第二种惜形的最小上界为d，第三种惜形的最小上界也是 d，故定理得证。定理 1.5.13.假设（d，彡）是完全半序集，xij（i，jo）是d巾元素，且当时有xijsxkl，则有：ui ujxij = ujiii xij = uk xkk证明:首先证明存在性。显然从（xid<xi+n河导出ujxi，kujxi + l

41、，j。因此ujxij 是d上的一个链，而d是完全半序集，故uiujxij定存在。同理，可证明ujllixij和 uk xkk存在。其次证明等式，巾xijxij可导出xij彡ui xij，进而再可导出ujxij<ujuixij, uiujxij < ujuixij同理可证明上述关系的逆关系，从而证明:uiiijxij= ujuixij。其次，证明本定理中的第 二个等式，即ujuixij = ukxkk。首先有vi，j:xij<ukxkk，由此可导出lhxijsilkxkk， 进而又可导出ujllixij <llk xkk。卜面证明上式的逆关系。显然有vlcxkk彡ujui

42、xij， 故可导出关系uk xkk < ii j hi xij。现在开始我们把论域理解为完全半序集。这一节考虑如何从已知论域构造出新的论 域的（完全半序集）问题。主要考虑scott所给出的论域的构造符x，+，*，->等。论域理论中 的最主要问题是论域的递归定义。scott首先解决了这个问题和函数的递归定义问题，从 而为指称语义学奠定了坚实的理论基础。巾于篇幅所限，我们将省略有关论域的递归定义 理论方面的内容。有兴趣者可参考有关文献。定义 1.5.14.元组域 productdlxd2x.xdn设（di，i）是半序集，i=l,.，n，则定义（01.011，）域如下： dlx.xdn

43、z （dl，.d2）| diedi，i=l，.n （dl,.dn）（dl',d2,.dn,） iftdiidi* l«n,称（d 1xd2x.xdn，）或d 1xd2x.xdnj为n元组域（或乘积域或卡氏域）.定理 1.5.15.设（0102.011，）是按上述定义构造出来的11元组域，且对每个i，（di，i）是完 全半序集，则该n元组域也是完全半序集。证明：1）可证明（di xd2x.，xdn，彡）是半序集。2）它有最小元（丄d1，.，丄dn）.3）为简单起见考虑n=2情形。证明di xd2上的任何一链 （di,dmi） 都有最小上界 u（d*i,d-i）0事实上可以证明下

44、面式子成立：u（cfi，d，.i）=（ii（ri，lld，.i）首先由d1和d2的完全半序性，可导出ud*i和ud”i的存在性。由（dwqildmd'i） 可导出 ii （t i，d" i）彡（u d. i，u d” i）。即（u df i，u d" i）是链（ti，d"i）的上界。下面证明（1111111"0的最小性。假设（cf，d"）是链（d*i，dni）的一个上界，即有 u （! i，d" i） （dd"），则立得vi:（d4，dni）彡（dd”），进而又可得u （f i 彡d和u d" i彡d 最终

45、可得（u（ri，ud”i）（cr，d"）。证毕。定义 1.5.16.联合域 sumdl+d2+.+dnl设（dj，s）是半序集，j=l，.，n，则定义（dl+.+dn，）域为如下: dl+“.+dn = （j，dj）| djedj,j=l,.n u1丄彡丄，丄彡（j，dj），其巾（i，di）彡（j，dj） iff i=j & di i dj称（d1+d2+.+dn，）或d1+d2+.+dn j为联合域（或直接合域）。定理 1.5.17.设（dl+d2+.+dn，）是按上述定义方法定义出来的联合域，而且对每个j,（dj，j）都是 完全半序集，则该联合域（dl+.+dn，彡）也是

46、完全半序集。证明:首先证明彡是dl+d2+.+dn上的半序关系。事实上根据定义，对于任一 i和di edi都有（诚）（诚），故关系彡有自反性;其次，如果有（诚1）彡（诚2）和（帥2）彡（诚3），则由 定义可推山dilidi2和出2）?山3，而 已知是半序关系，故可推出dilidi3。进而再推 山仏出1）汰出3），即关系彡具有传递性。反对称性的证明也类似。其次可证明 （dl+d2+.+dn，）有最小元丄。最后要证明的是（01+02+.+0丨1，）上的任何一链乂1都 有最小上界ii xi。事实上链xi可分为以下儿种情形： 丄，丄，丄，丄， 丄，丄，.，丄，(k，dkl)，(k，dk2)， dkid

47、k (k，dkl)，(k，dk2)，(k，dk3)， dki e dk其屮笫一种情形的最小上界为丄，第二和第三种情形的最小上界力(k，ii xi)，注意(dk，卸是 完全半序集，因此ii xi存在，其中xi表示dki。故定理得证。定义 1.5.18.序列域 squences d*设(d，<)是半序集，则序列域(d'，<)的定义如下： d*=<dl，d2，."，dn|n>0，died，i=l，2,3”. <<<< ><dl,d2,.,dn>, (diedi)<dl”x <dr,.,dm*> if

48、f n=m& djdj,(j=l,2,3,.)定理 1.5.19.设(d<)是按上述方法定义的序列域，且(do是完全半序集，则该序列域(d*<)也是 完全半序集.证明:首先可证明(d»是半序集滿次可证明有最小元<最后要证明(d<)上的任 何链sj，usj存在。事实上，该链有以下三种惜形：1. <<，<，<，.2. < <，.”<dl i”.”dln，<d21，.，d2n，.3. < <dl i，.，dln，<d21，.，d2n，<d31，."d3n，.显然，第一种情形有最

49、小上界<第二和第三种情形有最小上界<uidi 1，.，uidin。可以 证明对于每一个k，都存在uidik，故得结论<uidil存在，于是定理得证。定义 1.5.20.函数空间 functioindl->d2设(dl，$)和(d2，q)是半序集，则函数域(d1 d2，彡)定义如下: 01->02=1是01到02的全函数 f h iff vxedlf(x) <2 h(x) 1定理 1.5.21.设(di d21，< )是按上述方法构造的全函数域，且(d1，q)和(d2，q)是完全半序集，则 (d1 d2，<)是完全半序集。证明:首先易证(d卜d2,

50、彡)是半序集;其次q是d1 d2的最小元，其屮q是处处无 定义的函数，即有dcd1.丄d :最后假设fi id1d2j上的任一链，往证fi 链定有最小上 界ii fi。我们首先定义函数f=xx.u fi(x),(xedl)，s然，对于任一 xedl，f(x)均有意义。 证明f是fi链的上界，为此要证明对于一切i>0,xedl，都有fi(x)公f(x)。事实上，有fl(x)<2 u fi(x)=f(x)故f的上界性被证。下而证明f是最小的上界。假设h是fi的一个上界，即对一切i有fi ho 往证 fho 事实上，对于一切 xedl，有 f(x)= lifi(x) <uh(x)

51、= h(x)。定理 1.5.22.设fi是(id1d2j，<)上任一链(di和d2为完全半序集)，则有(ii fi)(x)=11 fi（x），（x edl）o证明:由前定理己得知f=xx.u fi（x）是链fi的最小上界，即有ii f,=fo故有下而推导 （ii fl）（x） = f（x） = ii fl（x）o§ 1.6连续函数在考虑函数时，为了方便起见，将偏函数（部分函数）开拓成全函数。其办法是这样，即 假设有偏函数f :d1 d2,则首先扩充d2域为d2=d2 u 丄，并使得当f（x）无定义时令 其值为丄。比如假没有f（x，y）=y/x，其中x和y取实数。s然当x=0时，

52、f（x，y）没有定义，因此 f是实数域real上的偏函数，而不是全函数。这吋函数f可开拓为如下：f:real1 x real 丄一 real1 f（x，y）=丄当x=丄或y=l=丄 当x=0 =y/x否则这样定义出来的函数f,首先是全函数（处处有定义），其次它与原函数一致，只是原函数没有 定义时取值丄罢了。因为f（a，b）的值也可能是另一函数h的实参值，即可能出现h（f（a，b）情 形，如果f（a，b）的值原是无定义的，那么开拓后取值丄，因此出现函数h的实参值为丄的情形， 这样我们不仅要扩充函数的侪域，而且还要扩充函数的定义域。以后考虑的都是全函数。定义1.6.1.自然开拓函数设d1，且当（d

53、l,d2，.，dn）屮有一个dj的值为丄j时 1132，.，加）取值丄，则称函数£为自然开拓函数。定义1.6.2.单调函数设fe d卜d2j，且d1和d2是半序集.若全函数f满足下面关系，则称f为单调函数： vx,yedlxy o f（x）f（y）定义1.6.3.严格函数设fedld2,dl和d2是半序集，且分别有最小元丄1和丄2。若f满足条件f（丄1）=丄2, 则称f为严格函数。简言之，严格函数把定义域中的最小元映射为值域中的最小元。定义1.6.4.连续函数设fedl d21，且d1和d2是完全半序集，若函数f满足下而条件，则称f为连续函 数：ui f（xi）= f（uixi）函数

54、的连续性是非常重要的性质。在程序语义的形式描述屮，对于数学模型的基本要 求是:所用到的函数为连续函数，而且所用到的域（定义域，值域）为完全半序集。其原因是 在程序的递归描述中，需要用到s小不动点的概念，而连续函数正是有s小不动点的函数， 同时它还能提供计算最小不动点的具体公式。定理 1.6.5.设fedl->d2kl f是连续函数，则f 一定为单调函数。其中d1和d2是完全半序集，证明:假设有x，yed1，且有x<y,往证f(x)f(y)y考虑链<，丫,丫，.，则根据连续 函数的定义，应有等式uf(xi) = f(iixi)对于本例来说该等式的左右部具体分别如下：uf(xi)

55、=f(x)uf(y) f(uxi)=f(xu y)zf(y)从上面两个式子可以看出如果有f(y)<f(x)，即f不单调，则得u f(xi)二f(x)。这样我们得 山结论lif(xi)f(lixi)。这与f的连续性相矛盾，故证毕。从本定理可以知道，连续函数都把定义域上的链映射为值域上的链，即如果<xl，.，xn. 是d1上的一个链，则<f(xl)，.，f(xn)，.也是d2上的一个链。定理 1.6.6.(1)若函数是严格函数，则f定是单调函数。若函数是常函数即有f(d)=c，则f定是单调函数。其中c是某固定的 常量，dedi1任意。证明:假设f是严格函数，即有f(丄0=丄2。往

56、证f是单调函数。事实上，假设“edi1， 并且a<b，则可分为以下两种情形來讨论(下面d为非丄元素)：1) a=±i情形。这吋有f(a)=f(丄1)=丄2彡f(b)，故有单调性。2) a=d惜形。这时由di1的平坦性定有a=b，故有f(a)=f(b)，即有f的单调性。常函数 的单调性的证明更简单，因对于任意a<b，都有f(a)=f(b)，即有f(a)<f(b).本定理中函数f的定义域和值域都是平坦集，它是完全半序集的特例。现在要问的是 如果把函数域都改成完全半序集，那么结论是否也同样成立?其回答是否定的，为此来再看 一下本定理证明中的第二种情形，即a<b但a关丄情形。在那里dii的平坦性保证了 a=b, 从而也保证了单调性。但现在没有平坦性，因此不能保证上述什么内容。事实上我们川直 接给出很多例子，其中只要对于使得a<b成立的某矣丄0定义函数f的值，使得 f(a)>f(b)成立即可。需要注意的是平坦域的多元组域01±乂02±><.乂011±并不构成平坦域，因此上述域上 的严格函数f未必是单调函数。但如果把函数f定义为fd1±xd2±x.xdn±l±上的严格函