《第4類型化演算的模型》由会员分享，可在线阅读，更多相关《第4類型化演算的模型（48页珍藏版）》请在金锄头文库上搜索。
1、第第4章章 类型化类型化 演算的模型演算的模型PCF语言由三部分组成语言由三部分组成带函数类型和积类型的纯类型化带函数类型和积类型的纯类型化 演算演算自然数类型和布尔类型自然数类型和布尔类型不动点算子不动点算子第第2章对代数数据类型进行了透彻的研究章对代数数据类型进行了透彻的研究第第3章研究简单类型化章研究简单类型化 演算演算本章先研究递归函数和不动点算子本章先研究递归函数和不动点算子然后研究类型化然后研究类型化 演算演算的的模型，因为第模型，因为第3章的章的模型不能解释不动点算子模型不能解释不动点算子袜清钻第栏郝匪沮渍寝纬辙饶斜乖愈亿赞回弃戌杨刀秃阜糖旺从网蹿胞掘第4類型化演算的模型第4類型
2、化演算的模型4.1 引引 言言本章的主要内容本章的主要内容递递归归函函数数和和不不动动点点算算子子，以以及及PCF语语言言的的编编程实例程实例基基于于完完全全偏偏序序集集合合的的，带带不不动动点点算算子子的的类类型型化化 演算的论域理论模型演算的论域理论模型不不动动点点归归纳纳法法，这这是是一一种种对对递递归归定定义义进进行行推推理的证明方法理的证明方法揪淖陪角败癣精哪捎帧淹铬媚粤蔓镇奎马童托约揩穿奋梨治奥磅促嘲旋榨第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子4.2.1 递归函数和不动点算子递归函数和不动点算子在类型化在类型化 演算中，可以加递归定义
3、演算中，可以加递归定义letrec f : = M in Nf可以出现在可以出现在M中中M的类型必须是的类型必须是 ，否则等式，否则等式f = M没有意义没有意义例：例：定义阶乘函数和计算定义阶乘函数和计算5的阶乘的阶乘letrec f : nat nat = y : nat.(if Eq? y 0 then 1 else y f (y 1) in f 5把该等式看成关于把该等式看成关于f的方程：的方程：f : nat nat = y : nat. if Eq? y 0 then 1 else y f (y 1)厅赡抒晌兴凑畅掀坊斟兹窑衷态舱眺搅蜡马帚诚苏雇校厌紫贝埠簇廓把栏第4類型化演算的模
4、型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子从数学的观点看从数学的观点看含含PCF表达式表达式M的方程的方程f : = M是否都有解？是否都有解？若有若干个解的话，选择哪个解？若有若干个解的话，选择哪个解？在讨论在讨论PCF的指称语义时解决这些问题的指称语义时解决这些问题从计算的观点看从计算的观点看递归函数声明有清楚的计算解释递归函数声明有清楚的计算解释因此，暂且假定每个这样的等式都有解，并在因此，暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法中增加上述表示它的语法统告僳彰挤上谓衔袜寂票耶划彬框酥成啸憨酱挖胳浦撵轩坷福酥鸡掠千兹第4類型化演算的模型第4
5、類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子函数的不动点函数的不动点若若F : 是类型是类型 到它自身的函数，则到它自身的函数，则F的不动点的不动点是使得是使得F (x) = x的值的值x : 例如，自然数上例如，自然数上 平方函数的不动点有平方函数的不动点有0和和1 恒等函数有无数个不动点恒等函数有无数个不动点 后继函数没有不动点后继函数没有不动点脓览面篙姜生支卿煞菜妹睛透统伸舍申盒蛋鸡替艾夸雀面岳耙毡搪歉阿把第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子重要联系重要联系递归定义递归定义f : = M可以用函数可以用函数 f :
6、.M来表示，因为来表示，因为函数函数 f : .M的不动点正好是方程的不动点正好是方程f = M的解的解( f : .M)N = N，即，即N/fM = N， N是是f = M的解的解方程方程f = M的求解转化为找函数的求解转化为找函数 f : .M的不动点的不动点例：例：阶乘函数是阶乘函数是F f : nat nat. y : nat.if Eq? y 0 then 1 else y f (y 1)的不动点的不动点满急楔仆铡顽痉剩晌条约双雪想铅便臀墒廊燎渡俐谐型苏纫极炔捍戒魂域第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子PCF的最后一个基本构造的
7、最后一个基本构造fix : ( ) , 对每个类型对每个类型 fix 为任何为任何 到到 的函数产生一个不动点的函数产生一个不动点 letrec声明形式看成是声明形式看成是let和不动点算子组合的一和不动点算子组合的一种语法美化种语法美化 letrec f : M in N let f : = (fix f : .M) in N 也可用语法美化也可用语法美化letrec f (x : ) : = M in N letrec f : x : .M in N郑斌嵌傻苯屯俞架壕尝卵磊姨恫插蹬庞标儿犹张谩慨甲凿聋唆浪惹艾彩到第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和
8、不动点算子fix等式公理等式公理fix = f : . .f (fix f )(fix)fix M M (fix M)（使使用用( ) 可得）可得）fix归约规则归约规则fix f : . f (fix f )(fix)独樟室驴淋厂捌瑰蹲幻话梯底剁砧老钩靴氟阅公纽侠恋坊治蛾啊杉辅句苦第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子继续阶乘函数的例子继续阶乘函数的例子使用使用fixnatnat，阶乘函数写成，阶乘函数写成fact fixnatnat F，其中，其中F是表达式是表达式F f :natnat. y:nat.if Eq? y 0 then 1el
9、se y f (y-1)fact n fix F n/计算计算fact n的前几步的前几步 F(fix F) n ( f : natnat. y:nat.if Eq? y 0 then 1else y f(y-1) (fix F) n if Eq? n 0 then 1 else n (fix F) (n-1)关杨撇糯述幢奢央爹妻削教奉栗惋耙恬汛内伞午蟹曙峻寥丈靛揖好社污骂第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子乘运算的递归定义乘运算的递归定义基基于于加加运运算算，并并假假定定有有前前驱驱函函数数pred，它它把把n 0映射到映射到n 1，并把，
10、并把0映射到映射到0letrec mult : nat nat nat = p : nat nat. if Eq? (Proj1 p) 0 then 0 else (Proj2 p) + mult pred (Proj1 p), Proj2 p in mult 8, 10 使用更多语法美化：使用更多语法美化： letrec mult x : nat, y : nat : nat = if Eq? x 0 then 0 else y + mult pred x, y in mult 8, 10 载麻休挥恢豫唱辛寥驴灾傀紫织瞩宫箕涧抠缝灯抵蓄腐萍悸董岳柑霞谁婆第4類型化演算的模型第4類型化演算的模
11、型4.2 递归函数和不动点算子递归函数和不动点算子4.2.2 有不动点算子的急切归约有不动点算子的急切归约考虑考虑fix对各种归约策略的影响对各种归约策略的影响 最左归约、惰性归约、并行归约最左归约、惰性归约、并行归约只要在原来的公理中增加只要在原来的公理中增加fix归约公理即可归约公理即可 急切归约急切归约若沿用原来的若沿用原来的fix规则，则对变元先求值的要求规则，则对变元先求值的要求会导致归约不终止会导致归约不终止引入引入“延迟延迟”（ delay）来暂停对递归定义函数的）来暂停对递归定义函数的归约，直到有变元提供给它为止归约，直到有变元提供给它为止疥为五逐罐沸理动检沁球织楚吟畜础需工倡
12、匡剿囱智耘卉罪碰贤沿伴窑甭第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子值（在急切归约中需要引入值的概念）值（在急切归约中需要引入值的概念） 若若V是常量、变量、是常量、变量、 抽象或值的序对，则抽象或值的序对，则V是值是值 delay M x: .Mx, x在在M : 中非自由的中非自由的公理公理 ( x : .M)V eager V x MV是值是值 Proji(V1, V2) eager ViV1和和V2是值是值 fix V eager V(delay fix V ) V是值是值 子项规则子项规则 和上一章一样和上一章一样疟诉乾吵黎疆紊高餐刹臃瞒
13、昼肝弛纸黎祖坦邪烹玛戚唐柯膛礼禄涕孙再稠第4類型化演算的模型第4類型化演算的模型4.2 递归函数和不动点算子递归函数和不动点算子例：仅含一个平凡不动点例：仅含一个平凡不动点 (fix ( x : nat nat. y : nat.y) ( z : nat.z +1)2)eager( x:nat nat. y:nat.y)(delay fix( x:nat nat. y : nat.y) ) ( z : nat.z +1)2)eager( y:nat.y)( z : nat.z +1)2)eager ( y:nat.y)(2+1) eager ( y:nat.y)3 eager 3例：急切归约可
14、能发散（无不动点）例：急切归约可能发散（无不动点）let f (x : nat) : nat = 5 inletrec g (x : nat) : nat = g (x +1) in f (g 3)希烃寥枕侍嫂厢娇表虫宰诱汇锄泣胡宿籽藻贮吏铁改蘑撩歇拿猿蛋体浸贯第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点4.3.1 递归定义和不动点算子递归定义和不动点算子用用fix归约的特点来启发论域的主要性质归约的特点来启发论域的主要性质以阶乘函数为例：以阶乘函数为例：fact fixnatnat F，其中，其中F是表达式是表达式F f :natnat. y:na
15、t.if Eq? y 0 then 1else y f (y-1)考虑考虑fix F的有限步展开，用另一种方式来理解的有限步展开，用另一种方式来理解fact羔凯穗澜耀饥寅仅甫拇钒晾碗黎钡缮胜陀茁杰中蛊濒奖须呕陇膜功眶据狠第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点fix F的有限步展开的有限步展开fixnF描述描述F体的计算最多使用体的计算最多使用n次的递归计算次的递归计算 fix0F = diverge （表示处处无定义的函数表示处处无定义的函数） fixn+1F = F(fixnF) (fix2F) 0 = 1，(fix2F)1 = 1，(fix
16、2F) n对对n 2没没有定义有定义 把函数把函数看成二元组的集合后看成二元组的集合后，fixn 1F = (fixnF) n, n ，真包含所有的真包含所有的fixiF (i n) 即即 0, 0! 0, 0! , 1, 1! 0, 0! , 1, 1! , 2, 2! 敏绢胳诊腕灌栅获赂辗肆舟陪击兹嚎关辕叛症意曝巷创我连踏之甄恍蘑鸦第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点 n( fixnF)和和F的不动点的不动点 让让fact = n( fixnF)是有直观计算意义的是有直观计算意义的 尚不足以相信，对任意的尚不足以相信，对任意的F， n(
17、fixnF)就是就是F的不动点的不动点 强加一些相对自然的条件到强加一些相对自然的条件到F才能保证这一点才能保证这一点 当用集合包含对部分函数排序时，当用集合包含对部分函数排序时， n( fixnF)将将是是F的最小不动点的最小不动点吞哗式几统胸葫新魄佐寞麻醋殖耽圣狄厦灾戌峨拈抿叔瘦幌触藏靶吱浆村第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点论域论域 用集合之间的包含用集合之间的包含关系来定义部分函数关系来定义部分函数之间的偏序之间的偏序 在类型化在类型化 演算的演算的论域理论模型中，论域理论模型中，类型指称值的偏类型指称值的偏序集合，叫做序集合，叫做
18、论域论域 0,1 , 1,1 , 2,1 常函数常函数1阶乘函数阶乘函数 0,1 , 1,1 , 2,2 0,1 , 1,1 0,1 0,5 . . . . . . . . . . . . . . . . .砰羚邓窿欠五舍焊辗盼桶摘鲁厩孺捆赎瑰瘤谴讣芋豢湛逛氮禽澳蚜机常狂第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点计算不终止的项计算不终止的项 和递归相联系的一个特别问题是如何给计算不终和递归相联系的一个特别问题是如何给计算不终止的项以合理解释止的项以合理解释?letrec f : nat nat = x: nat. f (x 1) in f 3 延伸
19、延伸“自然数自然数”论域，包含一个额外的值论域，包含一个额外的值 nat，表示，表示类型类型nat上的不终止的计算上的不终止的计算 部分数值函数可看成值域为部分数值函数可看成值域为 nat的全函数，的全函数，在该论域上在该论域上 nat所有的自然数所有的自然数 论域上的偏序可以用来论域上的偏序可以用来刻画称之为刻画称之为“信息量信息量”或或“定义度定义度”的特征的特征秀豺略癣士菏亥挟海遏蔷拢橡莹绍床婴仓憨裔迎凉空搓怒甩倚盒工迟淑浚第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点4.3.2 完全偏序集合、提升和笛卡儿积完全偏序集合、提升和笛卡儿积定义定义
20、偏序集合偏序集合 D, 有自反、反对称和传递关系有自反、反对称和传递关系 的集合的集合D 离散序离散序 指指x y iff x y。集合有离散的偏序。集合有离散的偏序上界上界若若 D, ，则子集，则子集S D的的上界上界是元素是元素x D，使，使得对任何得对任何y S都有都有y x埋掏堵隔挤呵耳欲战旬劳阵荐硼棵控尽暂钞樱甥果柔阻恍泌校谬诊陡衙鸣第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定义定义 最小上界最小上界S的一的一 个上界，它小于等于个上界，它小于等于()S的任何其它上界的任何其它上界 有向集合有向集合在在 D, 中，对子集中，对子集S D，
21、若每个有限集合，若每个有限集合S0 S都有上界在都有上界在S中，则称子集中，则称子集S有向有向有向集合都非空有向集合都非空若若S D是线性序，则是线性序，则S一定有向一定有向 线性序线性序对所有的对所有的x, y S，都有，都有x y或或y x 俯欧锥影段资哟傻酮判咋脚握蕉肮碑纹布榜霞挂阅撵龋框艺阁朝伟律赞鄂第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点例例 偏序集合偏序集合a0, b0, a1, b1, a2, b2, ，其中对任意，其中对任意i j都有都有ai aj, bj并且并且bi aj, bj 两个线性序两个线性序a0a1a2，和，和b0b1
22、b2 ai, bi有上界有上界ai+1和和bi+1等，等，但没有最小上界但没有最小上界a0a1a2b0b1b2 ai和和bi没有最小上界没有最小上界疫悲倍译理檬更痕凿启谊狭镍坦舟坊陆代署桅摄贰纽嘻窃姜汹敞俞瑟内须第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定义定义 完全偏序集合完全偏序集合 D, （简称（简称CPO） 若若每个有向集合每个有向集合S D都有最小上界（都有最小上界（S）例例 使用离散序，任何集合都可看成使用离散序，任何集合都可看成CPO 任何有限偏序集合都是任何有限偏序集合都是CPO 考虑普通算术序，自然数集合不是考虑普通算术序，自然数
23、集合不是CPO 有理数的非平凡闭区间不是有理数的非平凡闭区间不是CPO，所有，所有小于小于的有理数的最小上界是无理数的有理数的最小上界是无理数 若若S，T D都有向，且都有向，且S的每个元素都的每个元素都T的某个的某个元素，那么元素，那么S T2却主医支窒拱情兴惰巳哗埋梗阐愤脾优靠仇澈呛犊决矛硬甄掌难瞳祟埂一第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定义定义 有最小元有最小元的的CPO D D D, 存在元素存在元素a，使得对，使得对D的任何元素的任何元素b都有都有a b 最小元（也叫底元最小元（也叫底元）用）用 D表示表示 提升集合提升集合A A
24、 提升提升CPO D D，类似地可得到类似地可得到有底元的有底元的CPO D D 01234 CPO N N 的图形表示的图形表示斩怀课究势癣窄镁霹尝挽澄域泣逗必矿凯苫团匈秤葡勤擅唤择怒惦佳郧杜第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点引理引理4.3 若若D D是一个是一个CPO，那么，那么D D 是有底元的是有底元的CPO引理引理4.4 若若D D和和EE都是都是CPO并都有底元，则它们的积并都有底元，则它们的积D D EE也是有底元的也是有底元的CPO。而且，若。而且，若S D E是有向的，是有向的，则则S = S1, S2 ，其中，其中Si=
25、 ProjiS如果如果D D和和EE分别有最小元分别有最小元 D和和 E，那么，那么D, , E 是是D D E E 的最小元的最小元靖颧吐斯糕腑淘漳畸疥揍视焦嘴侄虑菱毒友一耍车是蕾淫跟材垒千拖撅积第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点4.3.3 连续函数连续函数 CPO上的连续函数上的连续函数 包括了在程序设计中使用的所有普通函数包括了在程序设计中使用的所有普通函数 给出的是一类有不动点的函数给出的是一类有不动点的函数 本本节节证证明明从从一一个个CPO到到另另一一个个CPO的的所所有有连连续续函函数的集合形成一个数的集合形成一个CPO 在在
26、构构造造把把每每个个类类型型看看成成一一个个CPO的的模模型型时时，这这是是最最本本质质的的一一步步，因因为为构构造造这这样样的的模模型型时时，函函数数类类型型必须解释成必须解释成CPO鸽摔口藐处雏伤喻遗祝把溅谎晚厦择同膀棠父潦摇皇碍讽牲液走螺腕俞板第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点记号记号 如如果果f : D E是是函函数数，如如果果S D，用用记记号号f(S)表表示示E的子集：的子集：f (S) = f (d ) | d S定义定义 单调函数单调函数 若若D D= D, D 和和EE= E, E 都都是是CPO，且且f : D E是是它
27、它们们基基础础集集合合上上的的函函数数，若若dd 蕴蕴涵涵 f(d) f (d ),则则f 单调单调若若f 单调且单调且S有向，则有向，则f (S)有向有向刀剐立肝峰钦世勿觅塞往疤到困衫剧连姚秆吮券檄饲鲍阴炕菠壮搁经犬绎第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定义定义 连续函数连续函数 单调，且单调，且 若对每个有向的若对每个有向的S D，都有，都有f (S) f (S)例例 在在实实轴轴闭闭区区间间x, y上上，若若把把x, y看看成成CPO时时，则则通常计算意义下的连续函数仍然连续通常计算意义下的连续函数仍然连续 任何任何CPO上的常函数是平
28、凡地连续的上的常函数是平凡地连续的 若若D D是离散序，则是离散序，则D D上每个函数都连续上每个函数都连续 从提升集合从提升集合A 到任何到任何CPO的单调函数连续的单调函数连续撅丛娩牲允咀刁五唤稿蜘似递咽嫡铺贱像晃券呵聚巳擦拜医宅庸朵鲤映崖第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定义定义 提升函数提升函数 如果如果D D和和EE都是都是CPO，且，且f :D E连续，定义连续，定义f : (D ) (E )如下：如下： f (d) = if d D then f(d) else 严格函数严格函数若若f 是有底元是有底元CPO之间的函数，且之间
29、的函数，且f ( ) 引理引理4.5 令令 D D和和 E E 都都 是是 CPO, , 若若 f:DE连连 续续 , , 则则f :D E 严格并连续严格并连续吁撼傣岭甩略苔蹄俏列撕疟惭套碴骇洽完凋供抚润世弄奏浩慰授京簇否条第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点CPO之间的函数之间的函数集合上的偏序关系集合上的偏序关系 若若D D = D, D 和和E = E, E 都都是是CPO，对对于于连连续续函函数数f, g:DE，若若对对每每个个d D，都都有有f(d)E g(d)，就说就说f D E g（逐点地排序逐点地排序）记号记号 从从D D
30、到到E E 的连续函数集写成的连续函数集写成D DEE D E, D E 若若S D E是是函函数数集集合合，且且d D，那那么么S(d) E是由是由S (d) = f (d) | f S给出的集合给出的集合吓帚践其沽价赊腻众锹篷脊经捆娃恿惧澈撅夕兑肚埃帚破蓉郝绝炽奖南自第4類型化演算的模型第4類型化演算的模型表表4.2 从从B 到到B 的单调函数的单调函数f ( ) f (true) f (false) f ( ) f (true) f (false)f0 f6 false truef1 true f7 true falsef2 false f8 false falsef3 true f9
31、true true truef4 false f10 false false falsef5 true truef0f1f2f3f4f5f6f7f8f9f10龙瑚聘经岩羹缩箍躲昧本楚井愤泌呸抛支违稻蔽午睹贡垄绊败怒一迫测傻第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点引理引理4.6 对对任任何何CPO D D和和EE，逐逐点点排排序序的的连连续续函函数数集集D DEE也是一个也是一个CPO具具体体说说，若若S DE有有向向，则则作作为为其其最最小小上上界界的的函函数数f 由由f(d) =S(d)给给出出。若若E E 有有最最小小元元，则则CPO D D
32、E E 有最小元有最小元D DE E 是一个偏序集合是一个偏序集合若若EE有最小元有最小元 E，则，则 x:D. . E是是D D E E 的最小元的最小元每个有向集合每个有向集合S 都有最小上界都有最小上界ff 是是连续的，即对每个有向的连续的，即对每个有向的S D E ，有有f (S) f (S)籽芦毡偏瓢颊评妖寓吠儒肾鳖肺缅毫言乌原菇刘桂烬窃磷膜谋裙栽搏专娠第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点常用连续函数常用连续函数 n元函数：元函数： f :D D1 D DnE E 连续，连续，当且仅当它在每个变元上连续当且仅当它在每个变元上连续 配
33、对函数：若配对函数：若S D和和T E都有向，都有向， 则则 S, T = s, t | s S, t T 射影函数：射影函数：若若S D E有向，有向， 则则Proji(S)= Proji(x) | x S 函数应用：函数应用：若若S DE和和T D都有向，都有向， 则则S(T) = f (x) | f S, x T 函数合成：函数合成：若若S DE和和T EF都有向都有向, ,则则(S) (T) =g f | f S, g T喳汀贫查萧般秒铅馆宾傅堰招棠箔悸呵漳鹤执逆黑饿潍症依卞赦揣钵拟剔第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点4.3.4 不
34、动点和完备连续层级不动点和完备连续层级完备连续完备连续 层级层级 若若有有CPO Ab0, 0 , , Abk, k ，则则取取Ab0, , Abk为基类型为基类型 A A A ，由由 逐坐标地定序逐坐标地定序 A 所所有有连连续续的的f : A , A , ，由由 逐点地定序逐点地定序 由先前引理，每个由先前引理，每个 A , 都是一个都是一个CPO这这是是在在CPO Ab0, 0 , , Abk, k 上上构构造造的的类类型型框框架架七哩页羞孙客侄模拓坤糊加细翰孽隧百蔽骡洪复实蒋汪匹进秽控决毁遮堕第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点主要结
35、论主要结论 任任何何若若干干CPO上上的的完完备备连连续续类类型型层层级级形形成成通通用用模型，并在所有有底元的类型上有最小不动点算子模型，并在所有有底元的类型上有最小不动点算子引理引理4.8 若若D D是是有有底底元元CPO，且且f :DD连连续续，则则f 有有最最小小不不动动点点fixD f = f n ( ) | n 0。此此外外，映映射射fixD是连续的是连续的 先证先证f n ( ) | n 0是不动点是不动点 再证它是最小不动点再证它是最小不动点 最后证明最后证明fixD连续连续底谅罚皮杰薛僵港哪商歧帕杆翟哭奄搀茬棠擞媒绒依汗肃痴纵概勃舵英舌第4類型化演算的模型第4類型化演算的模型
36、4.3 论域理论模型和不动点论域理论模型和不动点例例 id:D DD D是有底元是有底元CPO D D上恒等函数上恒等函数，计算，计算fix idfix id = idn ( D) | n 0= D= D f :PPNPPN，f(A) =A 不在不在A中的最小中的最小I N，若它存在的话，若它存在的话 很容易看出很容易看出f k () = 0, , k-1 于是于是fix f = N械八疤援霜赘扼抿敷忆坪擅枢速耕商束衍巾狗矽芋塌共然拧饿从擒侠谓凿第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点4.3.5 PCF的的CPO模型模型要点要点 考虑考虑PCF语
37、言的论域语言的论域理论语义理论语义A APCF提供对提供对PCF性质的某种透彻理解性质的某种透彻理解提供对提供对PCF进行语义推理的基础进行语义推理的基础 PCF等式公理系统对等式公理系统对A APCF可靠可靠 归约系统对归约系统对A APCF也可靠也可靠 PCF等式证明系统对等式证明系统对A APCF不可能完备不可能完备 4.4节节将将考考虑虑等等式式公公理理系系统统的的一一个个扩扩展展，它它基基于于该该CPO模型，能证明项之间更多的性质模型，能证明项之间更多的性质掠嵌彬排哨周跨虽列佐儡荤薪便滨滤鞍腊劲舵彤驹滞讹枝庸箭活桂厘杨炬第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不
38、动点论域理论模型和不动点 A APCF是是N 和和B 上的完全连续体系上的完全连续体系 PCF的类型常量解释为有底元的的类型常量解释为有底元的CPO PCF的所有类型都可以解释为有底元的的所有类型都可以解释为有底元的CPO常量的解释常量的解释常常量量0,1,2,和和true，false按按通通常常的的方方式式解解释释为为提提升集合升集合N 和和B 上的自然数和布尔值上的自然数和布尔值 +和和Eq?解释为它们普通解释的提升版本解释为它们普通解释的提升版本 和和Eq? nat + x = x + nat = nat条件运算的解释需仔细考虑条件运算的解释需仔细考虑当当M指指称称 而而N不不是是时时，
39、if false then M else N不不应该指称应该指称 敌鹊窖救竟泛虹下荡吸撞丹屹匝壬憎宪浪银蒙送豫息葡饱芹材往咀炬邱续第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点 不动点不动点常量常量按下面定理进行解释按下面定理进行解释若若D D是是有有底底元元的的CPO，且且f :D DD D 连连续续，则则f 有有最最小不动点小不动点fixD f = f n( ) | n 0 此外，映射此外，映射fixD是连续的是连续的结论结论 PCF的每个项在的每个项在A APCF中都有含义中都有含义胶密搅玫炭灰华桂鄙轮壹亚铀郴氰佯数萄坯点怕早吹使叫税糠偿璃汪沟声
40、第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点定理定理4.13令令M和和N是是 上的上的PCF表达式，若表达式，若 M =N : 从从PCF的公理可证，的公理可证，则则A APCF满足等式满足等式 M = N : 推论推论4.14若若 M: 是是良良类类型型的的PCF项项，且且MN，则则PCF模型模型A APCF满足等式满足等式 M = N : 檬揖挎辑昏跋咯监酗支册氯赃程豆吕厅晦玖邑刚盂肛世围城褐译兹厘署郑第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点例例阶乘函数可以写成阶乘函数可以写成fact fixnat
41、nat F，其中其中F f :natnat. y:nat. if Eq? y 0 then 1else y f (y-1) 可以可以证明，证明，A APCF F是连续的是连续的 APCF fact = =(APCF fact)n ( ) | n 0 (APCF fact)0( ) = natnat 直接用直接用 项来表示相应论域中元素的名字项来表示相应论域中元素的名字坚吻修继置倚酗肪足泰钉帛惩琐债章丘加泄墨诬迈堂桩躬亡凋液融祭智彭第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点 (APCF fact)1( ) = y:nat. if Eq? y 0 th
42、en 1else y (APCF fact)0( ) )(y-1)= y:nat. if Eq? y 0 then 1 else y ( natnat) (y-1)= y:nat. if Eq? y 0 then 1 else nat列喳倪缅关接潜洛靡暑溃稿抓沾直盗耻鲁拢勺取收睦耸吨宜豌科槐姿突桅第4類型化演算的模型第4類型化演算的模型4.3 论域理论模型和不动点论域理论模型和不动点例例考虑函数考虑函数F : (natnat) (natnat)，其定义为，其定义为 F f :natnat. x:nat. if Eq? x 1 then 1 else f (x-2) 满足下列条件的函数满足下列条
43、件的函数g:natnat都是上面都是上面F的不动点的不动点g(1) = 1g(x+2) = g(x)最小不动点是：最小不动点是：当当x是奇数时是奇数时，结果是，结果是1 当当x是偶数时是偶数时，计算不终止，计算不终止窿龙坦禾萤溉具皋疚迸坚绕恭踊悲芽观匆愉王计戚谬避挚锤古丸郡梯君厘第4類型化演算的模型第4類型化演算的模型4.4 不动点归纳不动点归纳例例 如如果果f : D D和和g : D D是是某某个个CPO D上上的连续函数，则的连续函数，则fix (f g) = f (fix (gf)fix (f g) = ( f g)i ( ) | i 0= , ( f g) ( ), ( f g f
44、g) ( ), = f ( ), (f (g f )( ), (f (g f )2)( ),. = ( f (g f )i ) ( ) | i 0= f (fix (gf)仅使用仅使用PCF的等式证明系统不可能证明的等式证明系统不可能证明fix (f g) = f (fix (gf)辊锋凄屋萎厨迭怨昂间操仇恿雕皑啪钻控暇臣扑茅检扇堤醛酸溯辛汛捧舌第4類型化演算的模型第4類型化演算的模型4.4 不动点归纳不动点归纳基于项的基于项的CPO解释来扩展证明系统解释来扩展证明系统在在CPO模模型型A中中，近近似似 M N 对对环环境境 是是满足的，如果满足的，如果A A M A A N (eq) (as
45、ym) M = N : M N: M N : , N M : M = N: 辱战强裸发蒂逮农啼驮滤杉电纤买瓦许糜铱鸯蚌愚脓彭需妙藩腐崔讹拧箍第4類型化演算的模型第4類型化演算的模型4.4 不动点归纳不动点归纳 (trans) M (bot) = x : . : (botf) (acong) (fcong) M N : , N P : M P : M1 M2 : , N1 N2 : M1 N1 M2 N2 : , x : M N : x : . M x : . N : 洒晾淡进击傀厦厌迁邓爱瘸设戈固酿液最块曹沸殃竖局再陨遗煌桓堂栽添第4類型化演算的模型第4類型化演算的模型4.4 不动点归纳不动点
46、归纳 用用 A表示从一组等式和近似表示从一组等式和近似 可以证明等式或近可以证明等式或近似似A MN = N : fix M N : /x A, , c/xA F(c)/xA fix F/xA常量常量c不在不在A中中 (fpind)烙狄窥豁把盒伙培擂役屁咨淄钳层剔悉精蓄饵缉懒甸端蹋止栓嚎漆鹏井徒第4類型化演算的模型第4類型化演算的模型4.4 不动点归纳不动点归纳例例 证明证明, ,如果如果N是是M的一个不动点的一个不动点, ,那么那么fix M N假定假定 MN N ，这就有，这就有 MN N 令令A , x : x N : ，其中，其中x在在N中不是自由的中不是自由的令不动点归纳规则中令不动
47、点归纳规则中F是是M1、首先证明首先证明 /xA N : 2、然后取然后取c/xA c N : 作为假设，证明作为假设，证明Mc/xA Mc N : 根据假设根据假设c N, ,由单调性由单调性，有，有 Mc MN : 因为因为MN N，所以，所以 Mc N : 腺坦氯易敏继售嫉江沥吞帚膝片换缺将埔馋缀赌想坞戍揪品算评伞萌益怀第4類型化演算的模型第4類型化演算的模型第一次：第一次：4.6，4.7，4.12第二次：第二次：4.18，4.25第三次：第三次： 4.30(a)，4.40(b)习习 题题划丛搽度弹用税政口吸兔幂诺应林廊池能尸抑董秤谐释蚕惫志瞒释嘴垣自第4類型化演算的模型第4類型化演算的模型
