类型化演算的模型.ppt

《类型化演算的模型.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第5章类型化演算的模型PCF语言的三部分组成带函数和积类型的纯类型化演算自然数类型和布尔类型不动点算子第3章对代数数据类型进行了透彻的研究第4章研究简单类型化演算本章研究不动点算子上一章的模型不能解释不动点算子5.1引言本章的主要内容基于完全偏序集合的，带不动点算子的类型化演算的论域理论模型。不动点归纳法，这是一种对递归定义进行推理的证明方法计算的适当性和完全抽象定理，它将PCF（及其衍生）的操作语义和基于论域的指称语义联系起来5.2论域理论模型和不动点5.2.1递归定义和不动点算子在类型化演算中，如果想加递归定义letrecf:=MinN只要加

2、上不动点算子fix就够了下面用fix归约的性质来启发fix的语义解释5.2论域理论模型和不动点使用fixnatnat，阶乘函数可以写成fact=deffixnatnatF，其中F是表达式F=deff:natnat.y:nat.ifEq?y0then1elseyf(y-1)factnfixFn=(f:(natnat)(natnat).f(fixf))Fn=F(fixF)n(f:natnat.y:nat.ifEq?y0then1elseyf(y-1))(fixF)n=ifEq?n0then1elsen(fixF)(n-1)5.

3、2论域理论模型和不动点考虑fixF的有限步展开，用另一种方式来理解fix[n+1]F=F(fix[n]F)fix[0]F=diverge（表示处处无定义的函数）fix[n]F描述F体的计算最多使用n次的递归计算(fix[2]F)0=1，(fix[2]F)1=1，(fix[2]F)n对n2没有定义把函数看成二元组的集合后，fix[n1]F=(fix[n]F){n,n}是真包含所有的fix[i]F(in)，即{0,0!}{0,0!,1,1!}{0,0!,1,1!,2,2!}…5.2论域理论模型和不动点让fact=

4、n(fix[n]F)是有直观的计算意义的尚不足以让人相信，对任意的F，n(fix[n]F)就是F的不动点需要强加一些相对自然的条件到F才能保证这一点当用集合包含对部分函数排序时，n(fix[n]F)将是F的最小不动点5.2论域理论模型和不动点用集合之间的包含关系来定义部分函数之间的偏序在类型化演算的论域理论模型中，类型指称值的偏序集合，叫做论域{0,1,1,1,2,1}常函数1阶乘函数{0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}........................5.2论域理论模

5、型和不动点和递归相联系的一个特别问题是如何给计算不终止的项以合理解释?letrecf:natnat=x:nat.f(x1)inf3延伸“自然数”论域，包含一个额外的值nat，用以表示类型nat上的不终止的计算任何部分数值函数可以看成值域为自然数加nat上的一个全函数论域上的这种序可用来刻画称之为“信息量”或“定义度”的特征5.2论域理论模型和不动点5.2.2完全偏序集合、提升和笛卡儿积偏序集合D，：有自反、反对称和传递关系的集合D任何集合可以看成有离散序的偏序集合，离散序是指xy当且仅当xy上界：如果D，是偏序集合，那么子集SD

6、的上界是元素xD，使得对任何yS都有yx最小上界：S的一个上界，它小于（）S的任何其它上界5.2论域理论模型和不动点有向集合：在偏序集合D，中，对于子集SD,如果每个有限集合S0S都有上界在S中,那么子集S称作有向的有向集合都是非空集合如果SD是线性序，那么S一定是有向的偏序集合{a0,b0,a1,b1,a2,b2,…}，其中对所有的ij都有aiaj,bj并且biaj,bja0a1a2b0b1b2ai和bi没有最小上界5.2论域理论模型和不动点完全偏序集合（简称CPO）偏序集合D，每个有向集合SD都有最小上界，写成∨S例：使

7、用离散序，任何集合都可以看成CPO例：任何有限偏序集合都是CPO例：考虑普通算术序，自然数集合不是CPO例：有理数的非平凡闭区间不是CPO，所有小于的有理数的最小上界是无理数如果S，TD都是有向的，并且S的每个元素都小于或等于T的某个元素，那么∨S∨T25.2论域理论模型和不动点有最小元的CPODD，有一个元素a，使得对D的任何元素b都有ab最小元（也叫底元）用D表示提升集合提升CPOD，得到有底元的CPOD…01234CPON的图形表示5.2论域理论模型和不动点引理假定D和E都是CPO。如果D和E都是有底元的，那么它们的积DE也是一

8、个有底元的CPO。而且，如果SDE是有向的，那么