文档介绍：第5章类型化演算的模型
PCF语言的三部分组成
带函数和积类型的纯类型化演算
自然数类型和布尔类型
不动点算子
第3章对代数数据类型进行了透彻的研究
第4章研究简单类型化演算
本章研究不动点算子
上一章的模型不能解释不动点算子
引言
本章的主要内容
基于完全偏序集合的,带不动点算子的类型化演算的论域理论模型。
不动点归纳法,这是一种对递归定义进行推理的证明方法
计算的适当性和完全抽象定理,它将PCF(及其衍生)的操作语义和基于论域的指称语义联系起来
论域理论模型和不动点
递归定义和不动点算子
在类型化演算中,如果想加递归定义
letrec f := M in N
只要加上不动点算子fix就够了
fix= f : .f (fix f ) (fix)
fix MM (fix M) (使用() 可得)
下面用fix归约的性质来启发fix的语义解释
论域理论模型和不动点
使用fixnatnat,阶乘函数可以写成fact =def fixnatnat F,其中F是表达式
F =def f :natnat.y: Eq? y 0 then 1 else yf (y-1)
fact n fix F n
= (f : (natnat) (natnat). f (fix f)) F n
= F(fix F) n
(f : natnat.y: Eq? y 0 then 1 else yf(y-1)) (fix F) n
= if Eq? n 0 then 1 else n(fix F) (n-1)
论域理论模型和不动点
考虑fix F的有限步展开,用另一种方式来理解
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[n1] F = (fix[n] F){n, n}是真包含所有的fix[i] F (in),
即{0, 0!} {0, 0!, 1, 1!} {0, 0!, 1, 1!, 2, 2!} …
论域理论模型和不动点
让fact = n ( fix[n] F)是有直观的计算意义的
尚不足以让人相信,对任意的F,n ( fix[n] F)就是F的不动点
需要强加一些相对自然的条件到F才能保证这一点
当用集合包含对部分函数排序时,n ( fix[n] F)将是F的最小不动点
论域理论模型和不动点
用集合之间的包含关系来定义部分函数之间的偏序
在类型化演算的
论域理论模型中,类型
指称值的偏序集合,
叫做论域
{0,1,1,1,2,1}
常函数1
阶乘函数
{0,1,1,1,2,2}
{0,1,1,1}
{0,1}
{0,5}
. . .
. . .
. . .
. . .
. . .
. . .
. . .
. . .
论域理论模型和不动点
和递归相联系的一个特别问题是如何给计算不终止的项以合理解释?
letrec f : nat nat = x: nat. f (x1) in f 3
延伸“自然数”论域,包含一个额外的值nat,用以表示类型nat上的不终止的计算
任何部分数值函数可以看成值域为自然数加nat上的一个全函数
论域上的这种序可用来刻画称之为“信息量”或“定义度”的特征
论域理论模型和不动点
完全偏序集合、提升和笛卡儿积
偏序集合D,:有自反、反对称和传递关系的集合D
任何集合可以看成有离散序的偏序集合,离散序是指xy当且仅当xy
上界:如果D,是偏序集合,那么子集SD的上界是元素xD,使得对任何yS都有yx
最小上界: S的一个上界,它小于()S的任何其它上界
论域理论模型和不动点
有向集合:在偏序集合D,中,对于子集SD, 如果每个有限集合S0S都有上界在S中, 那么子集S称作有向的
有向集合都是非空集合
如果SD是线性序,
那么S一定是有向的
偏序集合{a0, b0, a1, b1,
a2, b2,…},其中对所有
的i j都有aiaj, bj并且
biaj, bj
a0
a1
a2
b0
b1
b2
ai和bi没有最小上界