第4章类型化演算的模型课件

第4章类型化演算的模型PCF语言由三部分组成带函数类型和积类型的纯类型化演算自然数类型和布尔类型不动点算子第2章对代数数据类型进行了透彻的研究第3章研究简单类型化演算本章先研究递归函数和不动点算子然后研究类型化演算的模型，因为第3章的模型不能解释不动点算子第4章类型化演算的模型PCF语言由三部分组成4.1引言本章的主要内容递归函数和不动点算子，以及PCF语言的编程实例基于完全偏序集合的，带不动点算子的类型化演算的论域理论模型不动点归纳法，这是一种对递归定义进行推理的证明方法4.1引言本章的主要内容4.2递归函数和不动点算子4.2.1递归函数和不动点算子在类型化演算中，可以加递归定义

letrecf:=MinNf可以出现在M中M的类型必须是，否则等式f=M没有意义例：定义阶乘函数和计算5的阶乘 letrecf:nat

nat=

y:nat.(ifEq?y0then1 elsey

f(y–1))inf5把该等式看成关于f的方程：f:nat

nat= y:nat.ifEq?y0then1elsey

f(y–1)4.2递归函数和不动点算子4.2.1递归函数和不动4.2递归函数和不动点算子从数学的观点看含PCF表达式M的方程f:

=M是否都有解？若有若干个解的话，选择哪个解？在讨论PCF的指称语义时解决这些问题从计算的观点看递归函数声明有清楚的计算解释因此，暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法4.2递归函数和不动点算子从数学的观点看4.2递归函数和不动点算子函数的不动点若F:

是类型

到它自身的函数，则F的不动点是使得F(x)=x的值x:例如，自然数上

平方函数的不动点有0和1

恒等函数有无数个不动点

后继函数没有不动点4.2递归函数和不动点算子函数的不动点4.2递归函数和不动点算子重要联系递归定义f:

=M可以用函数f:.M来表示，因为函数f:.M的不动点正好是方程f=M的解

(f:.M)N=N，即[N/f]M=N，N是f=M的解方程f=M的求解转化为找函数f:.M的不动点例：阶乘函数是 F

f:nat

nat.y:nat.ifEq?y0then1 elsey

f(y–1)的不动点4.2递归函数和不动点算子重要联系4.2递归函数和不动点算子PCF的最后一个基本构造

fix:(

), 对每个类型fix为任何

到

的函数产生一个不动点letrec声明形式看成是let和不动点算子组合的一种语法美化 letrecf:

MinN

letf:=(fix

f:.M)inN

也可用语法美化

letrecf(x:):=MinN

letrecf:

x:.MinN4.2递归函数和不动点算子PCF的最后一个基本构造4.2递归函数和不动点算子fix等式公理 fix=f:.f(fixf) (fix) fixMM(fixM) （使用()可得）fix归约规则 fix

f:

.f(fixf) (fix)4.2递归函数和不动点算子fix等式公理4.2递归函数和不动点算子继续阶乘函数的例子使用fixnatnat，阶乘函数写成 factfixnatnatF，其中F是表达式

F

f:natnat.y:nat.ifEq?y0then1 elseyf(y-1)factn

fixF

n //计算factn的前几步

F(fixF)n

(f:natnat.y:nat.ifEq?y0then1 elseyf(y-1))(fixF)n

ifEq?n0then1elsen(fixF)(n-1)4.2递归函数和不动点算子继续阶乘函数的例子4.2递归函数和不动点算子乘运算的递归定义基于加运算，并假定有前驱函数pred，它把n>0映射到n

1，并把0映射到0letrecmult:nat

nat

nat=p:nat

nat.

ifEq?(Proj1

p)0then0 else(Proj2

p)+mult

pred(Proj1

p),Proj2

p

inmult

8,10使用更多语法美化：letrecmultx:nat,y:nat

:nat=ifEq?x0then0elsey+multpredx,yinmult

8,104.2递归函数和不动点算子乘运算的递归定义4.2递归函数和不动点算子4.2.2有不动点算子的急切归约考虑fix对各种归约策略的影响

最左归约、惰性归约、并行归约

只要在原来的公理中增加fix归约公理即可

急切归约

若沿用原来的fix规则，则对变元先求值的要求会导致归约不终止

引入“延迟”（delay）来暂停对递归定义函数的归约，直到有变元提供给它为止4.2递归函数和不动点算子4.2.2有不动点算子的4.2递归函数和不动点算子值（在急切归约中需要引入值的概念）若V是常量、变量、抽象或值的序对，则V是值delayMx:.Mx,x在M:

中非自由的公理(x:.M)VeagerVxM

V是值Proji(V1,V2)eager

Vi

V1和V2是值fixV

eager

V(delay

fixV) V是值……子项规则和上一章一样4.2递归函数和不动点算子值（在急切归约中需要引入值4.2递归函数和不动点算子例：仅含一个平凡不动点(fix(x:natnat.y:nat.y))((z:nat.z+1)2)eager(x:natnat.y:nat.y)(delayfix(x:natnat.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

eager3例：急切归约可能发散（无不动点）letf(x:nat):nat=5in

letrecg(x:nat):nat=g(x+1)inf(g3)4.2递归函数和不动点算子例：仅含一个平凡不动点4.3论域理论模型和不动点4.3.1递归定义和不动点算子用fix归约的特点来启发论域的主要性质以阶乘函数为例： factfixnatnatF，其中F是表达式 F

f:natnat.y:nat.ifEq?y0then1 elseyf(y-1)考虑fixF的有限步展开，用另一种方式来理解fact4.3论域理论模型和不动点4.3.1递归定义和不动点算4.3论域理论模型和不动点fixF的有限步展开fix[n]F描述F体的计算最多使用n次的递归计算fix[0]F=diverge（表示处处无定义的函数）fix[n+1]F=F(fix[n]F)(fix[2]F)0=1，(fix[2]F)1=1，(fix[2]F)n对n2没有定义把函数看成二元组的集合后，fix[n1]F=(fix[n]F){n,n}，真包含所有的fix[i]F(in)即

{0,0!}{0,0!,1,1!}{0,0!,1,1!,2,2!}…4.3论域理论模型和不动点fixF的有限步展开4.3论域理论模型和不动点n(fix[n]F)和F的不动点让fact=n(fix[n]F)是有直观计算意义的尚不足以相信，对任意的F， n(fix[n]F)就是F的不动点强加一些相对自然的条件到F才能保证这一点当用集合包含对部分函数排序时，n(fix[n]F)将是F的最小不动点4.3论域理论模型和不动点n(fix[n]F)和F的4.3论域理论模型和不动点论域用集合之间的包含关系来定义部分函数之间的偏序在类型化演算的论域理论模型中，类型指称值的偏序集合，叫做论域{0,1,1,1,2,1}常函数1阶乘函数{0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}........................4.3论域理论模型和不动点论域{0,1,1,1,4.3论域理论模型和不动点计算不终止的项和递归相联系的一个特别问题是如何给计算不终止的项以合理解释? letrecf:nat

nat=x:nat.f(x1)inf3延伸“自然数”论域，包含一个额外的值nat，表示类型nat上的不终止的计算部分数值函数可看成值域为{nat}的全函数，在该论域上nat所有的自然数论域上的偏序可以用来刻画称之为“信息量”或“定义度”的特征4.3论域理论模型和不动点计算不终止的项4.3论域理论模型和不动点4.3.2完全偏序集合、提升和笛卡儿积定义偏序集合D, 有自反、反对称和传递关系的集合D离散序 指x

yiffxy。集合有离散的偏序上界 若D,

，则子集SD的上界是元素xD，使得对任何yS都有yx4.3论域理论模型和不动点4.3.2完全偏序集合、提升4.3论域理论模型和不动点定义最小上界 S的一个上界，它小于等于()S的任何其它上界有向集合 在D,中，对子集SD，若每个有限集合S0S都有上界在S中，则称子集S有向 有向集合都非空 若SD是线性序，则S一定有向线性序 对所有的x,yS，都有xy或yx

4.3论域理论模型和不动点定义4.3论域理论模型和不动点例偏序集合{a0,b0,a1,b1,a2,b2,…}，其中对任意i

j都有ai

aj,bj并且bi

aj,bj两个线性序

a0a1a2…，和 b0b1b2…

{ai,bi} 有上界ai+1和bi+1等， 但没有最小上界a0a1a2b0b1b2

ai和bi没有最小上界4.3论域理论模型和不动点例a0a1a2b0b1b24.3论域理论模型和不动点定义完全偏序集合D,

（简称CPO）

若每个有向集合SD都有最小上界（∨S）例使用离散序，任何集合都可看成CPO任何有限偏序集合都是CPO考虑普通算术序，自然数集合不是CPO有理数的非平凡闭区间不是CPO，所有小于的有理数的最小上界是无理数若S，TD都有向，且S的每个元素都T的某个元素，那么∨S

∨T24.3论域理论模型和不动点定义24.3论域理论模型和不动点定义有最小元的CPOD

D, 存在元素a，使得对D的任何元素b都有a

b 最小元（也叫底元）用D表示提升集合A

A{}提升CPOD， 类似地可得到

有底元的CPOD…01234

CPO

N的图形表示4.3论域理论模型和不动点定义…01234CPO4.3论域理论模型和不动点引理4.3若D是一个CPO，那么D是有底元的CPO引理4.4若D和E都是CPO并都有底元，则它们的积DE也是有底元的CPO。而且，若SDE是有向的，则∨S=

∨S1,∨S2，其中Si=ProjiS 如果D和E分别有最小元D和E，那么D,E是DE的最小元4.3论域理论模型和不动点引理4.34.3论域理论模型和不动点4.3.3

连续函数

CPO上的连续函数包括了在程序设计中使用的所有普通函数给出的是一类有不动点的函数本节证明从一个CPO到另一个CPO的所有连续函数的集合形成一个CPO在构造把每个类型看成一个CPO的模型时，这是最本质的一步，因为构造这样的模型时，函数类型必须解释成CPO4.3论域理论模型和不动点4.3.3连续函数4.3论域理论模型和不动点记号如果f:DE是函数，如果SD，用记号f(S)表示E的子集：f(S)={f(d)|dS}定义单调函数 若D=D,D和E=E,E都是CPO，且f:DE是它们基础集合上的函数，若dd蕴涵f(d)

f(d),则f单调 若f

单调且S有向，则f(S)有向4.3论域理论模型和不动点记号4.3论域理论模型和不动点定义连续函数 单调，且 若对每个有向的SD，都有f(∨S)∨f(S)例在实轴闭区间[x,y]上，若把[x,y]看成CPO时，则通常计算意义下的连续函数仍然连续任何CPO上的常函数是平凡地连续的若D是离散序，则D上每个函数都连续从提升集合A到任何CPO的单调函数连续4.3论域理论模型和不动点定义4.3论域理论模型和不动点定义提升函数 如果D和E都是CPO，且f:D

E连续，定义f:(D{})

(E{})如下：

f(d)=ifd

Dthenf(d)else严格函数 若f是有底元CPO之间的函数，且f

()

引理4.5令D和E都是CPO,若f:DE连续,则f:DE严格并连续4.3论域理论模型和不动点定义4.3论域理论模型和不动点CPO之间的函数集合上的偏序关系若D=D,D和E=E,E都是CPO，对于连续函数f,g:DE，若对每个dD，都有f(d)Eg(d)，就说fD

Eg（逐点地排序）记号从D

到E的连续函数集写成

DE

D

E,D

E若S

D

E是函数集合，且dD，那么S(d)E是由

S(d)={f(d)|f

S}给出的集合4.3论域理论模型和不动点CPO之间的函数集合上的偏序关表4.2从B到B的单调函数

f()f(true)f(false) f()f(true)f(false)f0

f6

false

truef1

true

f7

true

falsef2

falsef8

false

falsef3

true

f9true

true

truef4

false

f10false

false

falsef5

truetruef0f1f2f3f4f5f6f7f8f9f10表4.2从B到B的单调函数f0f1f2f3f4f5f64.3论域理论模型和不动点引理4.6对任何CPOD和E，逐点排序的连续函数集DE也是一个CPO 具体说，若S

DE有向，则作为其最小上界的函数f由f(d)=∨S(d)给出。若E有最小元，则CPO

DE有最小元

DE是一个偏序集合 若E有最小元E，则x:D.E是D

E的最小元 每个有向集合S都有最小上界f f是连续的，即对每个有向的SDE， 有f(∨S)

∨f(S)4.3论域理论模型和不动点引理4.64.3论域理论模型和不动点常用连续函数n元函数：f:D1…DnE连续， 当且仅当它在每个变元上连续配对函数：若SD和TE都有向， 则∨S,∨T=∨{s,t|sS,tT}射影函数：若SDE有向， 则Proji(∨S)=∨{Proji(x)|xS}函数应用：若SDE和TD都有向， 则∨S(∨T)=∨{f(x)|fS,xT}函数合成：若SDE和TEF都有向, 则(∨S)

(∨T)=∨{g

f|fS,gT}4.3论域理论模型和不动点常用连续函数4.3论域理论模型和不动点4.3.4不动点和完备连续层级完备连续层级若有CPOAb0,0,…,Abk,k，则取Ab0,…,Abk为基类型AAA，由逐坐标地定序A所有连续的f:A,A,，由逐点地定序由先前引理，每个A,都是一个CPO这是在CPOAb0,0,…,Abk,k上构造的类型框架4.3论域理论模型和不动点4.3.4不动点和完备连续层4.3论域理论模型和不动点主要结论 任何若干CPO上的完备连续类型层级形成通用模型，并在所有有底元的类型上有最小不动点算子引理4.8若D是有底元CPO，且f:DD连续，则f有最小不动点fixDf=∨{fn()|n0}。此外，映射fixD是连续的先证∨{fn()|n0}是不动点再证它是最小不动点最后证明fixD连续4.3论域理论模型和不动点主要结论4.3论域理论模型和不动点例id:DD是有底元CPO

D上恒等函数，计算fixid

fixid=∨{idn(D)|n0} =∨{

D} =Df

:PNPN，f(A)= A不在A中的最小IN，若它存在的话很容易看出fk()={0,…,k-1}于是fixf=N4.3论域理论模型和不动点例4.3论域理论模型和不动点4.3.5PCF的CPO模型要点考虑PCF语言的论域理论语义APCF 提供对PCF性质的某种透彻理解 提供对PCF进行语义推理的基础PCF等式公理系统对APCF可靠归约系统对APCF也可靠PCF等式证明系统对APCF不可能完备4.4节将考虑等式公理系统的一个扩展，它基于该CPO模型，能证明项之间更多的性质4.3论域理论模型和不动点4.3.5PCF的CPO模4.3论域理论模型和不动点

APCF是N和B上的完全连续体系PCF的类型常量解释为有底元的CPOPCF的所有类型都可以解释为有底元的CPO常量的解释常量0,1,2,…和true，false按通常的方式解释为提升集合N和B上的自然数和布尔值+和Eq?解释为它们普通解释的提升版本和Eq?

nat+

x=x+

nat=nat条件运算的解释需仔细考虑

当M指称而N不是时，iffalsethenMelseN不应该指称4.3论域理论模型和不动点APCF是N和B上的完全4.3论域理论模型和不动点不动点常量按下面定理进行解释 若D是有底元的CPO，且f:DD连续，则f有最小不动点

fixDf=∨{fn()|n0} 此外，映射fixD是连续的结论PCF的每个项在APCF中都有含义4.3论域理论模型和不动点不动点常量按下面定理进行解释4.3论域理论模型和不动点定理4.13令M和N是上的PCF表达式，若 M=N:从PCF的公理可证，则APCF满足等式

M=N:推论4.14 若M:是良类型的PCF项，且MN，则PCF模型APCF满足等式

M=N:4.3论域理论模型和不动点定理4.134.3论域理论模型和不动点例阶乘函数可以写成fact

fixnatnatF，其中F

f:natnat.y:nat.ifEq?y0then1 elseyf(y-1)可以证明，APCF

F是连续的APCFfact=∨{(APCFfact)n

()|n0}(APCFfact)0()=natnat直接用项来表示相应论域中元素的名字4.3论域理论模型和不动点例4.3论域理论模型和不动点

(APCFfact)1()=y:nat.ifEq?y0then1 elsey((APCFfact)0())(y-1)=y:nat.ifEq?y0then1elsey(natnat)(y-1)=y:nat.ifEq?y0then1elsenat4.3论域理论模型和不动点 4.3论域理论模型和不动点例 考虑函数F:(natnat)(natnat)，其定义为

F

f:natnat.x:nat.ifEq?x1then1elsef(x-2)

满足下列条件的函数g:natnat都是上面F的不动点

g(1)=1

g(x+2)=g(x) 最小不动点是：

当x是奇数时，结果是1

当x是偶数时，计算不终止4.3论域理论模型和不动点例4.4不动点归纳例如果f:DD和g:DD是某个CPOD上的连续函数，则fix(fg)=f(fix(gf))fix(fg)=∨{(fg)i()|i0} =∨{,(fg)

(),(f

g

f

g)

(),…} =∨{f(),(f(g

f))(),(f(g

f)2)(),...

} =∨{(f(g

f)i)

()|i0} =f(fix(gf)) 仅使用PCF的等式证明系统不可能证明 fix(fg)=f(fix(gf))4.4不动点归纳例如果f:DD和g:DD4.4不动点归纳基于项的CPO解释来扩展证明系统在CPO模型A中，近似

M

N

对环境

是满足的，如果A

M

A

N

(eq) (asym)

M

=N:

M

N:

M

N:,

N

M

:

M=N:4.4不动点归纳基于项的CPO解释来扩展证明系统M4.4不动点归纳

(trans)M (bot)=x:.: (botf) (acong) (fcong)

M

N:,

N

P

:

M

P

:

M1M2

:,

N1N2

:

M1

N1

M2N2

:,x:

MN:

x:.

M

x:.N:4.4不动点归纳MN:,N4.4不动点归纳

用

A表示从一组等式和近似可以证明等式或近似A

MN=

N:

fixM

N

:[/x]A,,[c/x]A[F(c)/x]A[fixF/x]A常量c不在A中(fpind)4.4不动点归纳MN=N:[/4.4不动点归纳例证明,如果N是M的一个不动点,那么fixM

N假定

MNN，这就有

MN

N

令A,x:x

N:，其中x在N中不是自由的令不动点归纳规则中F是M1、首先证明

[/x]A

N:

2、然后取[c/x]A

c

N:作为假设，证明 [Mc/x]A

Mc

N:根据假设c

N,由单调性，有

Mc

MN:

因为MN

N，所以

Mc

N:4.4不动点归纳例证明,如果N是M的一个不动点,那么fi第一次：4.6，4.7，4.12第二次：4.18，4.25第三次：4.30(a)，4.40(b)习题第一次：4.6，4.7，4.12习题第4章类型化演算的模型PCF语言由三部分组成带函数类型和积类型的纯类型化演算自然数类型和布尔类型不动点算子第2章对代数数据类型进行了透彻的研究第3章研究简单类型化演算本章先研究递归函数和不动点算子然后研究类型化演算的模型，因为第3章的模型不能解释不动点算子第4章类型化演算的模型PCF语言由三部分组成4.1引言本章的主要内容递归函数和不动点算子，以及PCF语言的编程实例基于完全偏序集合的，带不动点算子的类型化演算的论域理论模型不动点归纳法，这是一种对递归定义进行推理的证明方法4.1引言本章的主要内容4.2递归函数和不动点算子4.2.1递归函数和不动点算子在类型化演算中，可以加递归定义

letrecf:=MinNf可以出现在M中M的类型必须是，否则等式f=M没有意义例：定义阶乘函数和计算5的阶乘 letrecf:nat

nat=

y:nat.(ifEq?y0then1 elsey

f(y–1))inf5把该等式看成关于f的方程：f:nat

nat= y:nat.ifEq?y0then1elsey

f(y–1)4.2递归函数和不动点算子4.2.1递归函数和不动4.2递归函数和不动点算子从数学的观点看含PCF表达式M的方程f:

=M是否都有解？若有若干个解的话，选择哪个解？在讨论PCF的指称语义时解决这些问题从计算的观点看递归函数声明有清楚的计算解释因此，暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法4.2递归函数和不动点算子从数学的观点看4.2递归函数和不动点算子函数的不动点若F:

是类型

到它自身的函数，则F的不动点是使得F(x)=x的值x:例如，自然数上

平方函数的不动点有0和1

恒等函数有无数个不动点

后继函数没有不动点4.2递归函数和不动点算子函数的不动点4.2递归函数和不动点算子重要联系递归定义f:

=M可以用函数f:.M来表示，因为函数f:.M的不动点正好是方程f=M的解

(f:.M)N=N，即[N/f]M=N，N是f=M的解方程f=M的求解转化为找函数f:.M的不动点例：阶乘函数是 F

f:nat

nat.y:nat.ifEq?y0then1 elsey

f(y–1)的不动点4.2递归函数和不动点算子重要联系4.2递归函数和不动点算子PCF的最后一个基本构造

fix:(

), 对每个类型fix为任何

到

的函数产生一个不动点letrec声明形式看成是let和不动点算子组合的一种语法美化 letrecf:

MinN

letf:=(fix

f:.M)inN

也可用语法美化

letrecf(x:):=MinN

letrecf:

x:.MinN4.2递归函数和不动点算子PCF的最后一个基本构造4.2递归函数和不动点算子fix等式公理 fix=f:.f(fixf) (fix) fixMM(fixM) （使用()可得）fix归约规则 fix

f:

.f(fixf) (fix)4.2递归函数和不动点算子fix等式公理4.2递归函数和不动点算子继续阶乘函数的例子使用fixnatnat，阶乘函数写成 factfixnatnatF，其中F是表达式

F

f:natnat.y:nat.ifEq?y0then1 elseyf(y-1)factn

fixF

n //计算factn的前几步

F(fixF)n

(f:natnat.y:nat.ifEq?y0then1 elseyf(y-1))(fixF)n

ifEq?n0then1elsen(fixF)(n-1)4.2递归函数和不动点算子继续阶乘函数的例子4.2递归函数和不动点算子乘运算的递归定义基于加运算，并假定有前驱函数pred，它把n>0映射到n

1，并把0映射到0letrecmult:nat

nat

nat=p:nat

nat.

ifEq?(Proj1

p)0then0 else(Proj2

p)+mult

pred(Proj1

p),Proj2

p

inmult

8,10使用更多语法美化：letrecmultx:nat,y:nat

:nat=ifEq?x0then0elsey+multpredx,yinmult

8,104.2递归函数和不动点算子乘运算的递归定义4.2递归函数和不动点算子4.2.2有不动点算子的急切归约考虑fix对各种归约策略的影响

最左归约、惰性归约、并行归约

只要在原来的公理中增加fix归约公理即可

急切归约

若沿用原来的fix规则，则对变元先求值的要求会导致归约不终止

引入“延迟”（delay）来暂停对递归定义函数的归约，直到有变元提供给它为止4.2递归函数和不动点算子4.2.2有不动点算子的4.2递归函数和不动点算子值（在急切归约中需要引入值的概念）若V是常量、变量、抽象或值的序对，则V是值delayMx:.Mx,x在M:

中非自由的公理(x:.M)VeagerVxM

V是值Proji(V1,V2)eager

Vi

V1和V2是值fixV

eager

V(delay

fixV) V是值……子项规则和上一章一样4.2递归函数和不动点算子值（在急切归约中需要引入值4.2递归函数和不动点算子例：仅含一个平凡不动点(fix(x:natnat.y:nat.y))((z:nat.z+1)2)eager(x:natnat.y:nat.y)(delayfix(x:natnat.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

eager3例：急切归约可能发散（无不动点）letf(x:nat):nat=5in

letrecg(x:nat):nat=g(x+1)inf(g3)4.2递归函数和不动点算子例：仅含一个平凡不动点4.3论域理论模型和不动点4.3.1递归定义和不动点算子用fix归约的特点来启发论域的主要性质以阶乘函数为例： factfixnatnatF，其中F是表达式 F

f:natnat.y:nat.ifEq?y0then1 elseyf(y-1)考虑fixF的有限步展开，用另一种方式来理解fact4.3论域理论模型和不动点4.3.1递归定义和不动点算4.3论域理论模型和不动点fixF的有限步展开fix[n]F描述F体的计算最多使用n次的递归计算fix[0]F=diverge（表示处处无定义的函数）fix[n+1]F=F(fix[n]F)(fix[2]F)0=1，(fix[2]F)1=1，(fix[2]F)n对n2没有定义把函数看成二元组的集合后，fix[n1]F=(fix[n]F){n,n}，真包含所有的fix[i]F(in)即

{0,0!}{0,0!,1,1!}{0,0!,1,1!,2,2!}…4.3论域理论模型和不动点fixF的有限步展开4.3论域理论模型和不动点n(fix[n]F)和F的不动点让fact=n(fix[n]F)是有直观计算意义的尚不足以相信，对任意的F， n(fix[n]F)就是F的不动点强加一些相对自然的条件到F才能保证这一点当用集合包含对部分函数排序时，n(fix[n]F)将是F的最小不动点4.3论域理论模型和不动点n(fix[n]F)和F的4.3论域理论模型和不动点论域用集合之间的包含关系来定义部分函数之间的偏序在类型化演算的论域理论模型中，类型指称值的偏序集合，叫做论域{0,1,1,1,2,1}常函数1阶乘函数{0,1,1,1,2,2}{0,1,1,1}{0,1}{0,5}........................4.3论域理论模型和不动点论域{0,1,1,1,4.3论域理论模型和不动点计算不终止的项和递归相联系的一个特别问题是如何给计算不终止的项以合理解释? letrecf:nat

nat=x:nat.f(x1)inf3延伸“自然数”论域，包含一个额外的值nat，表示类型nat上的不终止的计算部分数值函数可看成值域为{nat}的全函数，在该论域上nat所有的自然数论域上的偏序可以用来刻画称之为“信息量”或“定义度”的特征4.3论域理论模型和不动点计算不终止的项4.3论域理论模型和不动点4.3.2完全偏序集合、提升和笛卡儿积定义偏序集合D, 有自反、反对称和传递关系的集合D离散序 指x

yiffxy。集合有离散的偏序上界 若D,

，则子集SD的上界是元素xD，使得对任何yS都有yx4.3论域理论模型和不动点4.3.2完全偏序集合、提升4.3论域理论模型和不动点定义最小上界 S的一个上界，它小于等于()S的任何其它上界有向集合 在D,中，对子集SD，若每个有限集合S0S都有上界在S中，则称子集S有向 有向集合都非空 若SD是线性序，则S一定有向线性序 对所有的x,yS，都有xy或yx

4.3论域理论模型和不动点定义4.3论域理论模型和不动点例偏序集合{a0,b0,a1,b1,a2,b2,…}，其中对任意i

j都有ai

aj,bj并且bi

aj,bj两个线性序

a0a1a2…，和 b0b1b2…

{ai,bi} 有上界ai+1和bi+1等， 但没有最小上界a0a1a2b0b1b2

ai和bi没有最小上界4.3论域理论模型和不动点例a0a1a2b0b1b24.3论域理论模型和不动点定义完全偏序集合D,

（简称CPO）

若每个有向集合SD都有最小上界（∨S）例使用离散序，任何集合都可看成CPO任何有限偏序集合都是CPO考虑普通算术序，自然数集合不是CPO有理数的非平凡闭区间不是CPO，所有小于的有理数的最小上界是无理数若S，TD都有向，且S的每个元素都T的某个元素，那么∨S

∨T24.3论域理论模型和不动点定义24.3论域理论模型和不动点定义有最小元的CPOD

D, 存在元素a，使得对D的任何元素b都有a

b 最小元（也叫底元）用D表示提升集合A

A{}提升CPOD， 类似地可得到

有底元的CPOD…01234

CPO

N的图形表示4.3论域理论模型和不动点定义…01234CPO4.3论域理论模型和不动点引理4.3若D是一个CPO，那么D是有底元的CPO引理4.4若D和E都是CPO并都有底元，则它们的积DE也是有底元的CPO。而且，若SDE是有向的，则∨S=

∨S1,∨S2，其中Si=ProjiS 如果D和E分别有最小元D和E，那么D,E是DE的最小元4.3论域理论模型和不动点引理4.34.3论域理论模型和不动点4.3.3

连续函数

CPO上的连续函数包括了在程序设计中使用的所有普通函数给出的是一类有不动点的函数本节证明从一个CPO到另一个CPO的所有连续函数的集合形成一个CPO在构造把每个类型看成一个CPO的模型时，这是最本质的一步，因为构造这样的模型时，函数类型必须解释成CPO4.3论域理论模型和不动点4.3.3连续函数4.3论域理论模型和不动点记号如果f:DE是函数，如果SD，用记号f(S)表示E的子集：f(S)={f(d)|dS}定义单调函数 若D=D,D和E=E,E都是CPO，且f:DE是它们基础集合上的函数，若dd蕴涵f(d)

f(d),则f单调 若f

单调且S有向，则f(S)有向4.3论域理论模型和不动点记号4.3论域理论模型和不动点定义连续函数 单调，且 若对每个有向的SD，都有f(∨S)∨f(S)例在实轴闭区间[x,y]上，若把[x,y]看成CPO时，则通常计算意义下的连续函数仍然连续任何CPO上的常函数是平凡地连续的若D是离散序，则D上每个函数都连续从提升集合A到任何CPO的单调函数连续4.3论域理论模型和不动点定义4.3论域理论模型和不动点定义提升函数 如果D和E都是CPO，且f:D

E连续，定义f:(D{})

(E{})如下：

f(d)=ifd

Dthenf(d)else严格函数 若f是有底元CPO之间的函数，且f

()

引理4.5令D和E都是CPO,若f:DE连续,则f:DE严格并连续4.3论域理论模型和不动点定义4.3论域理论模型和不动点CPO之间的函数集合上的偏序关系若D=D,D和E=E,E都是CPO，对于连续函数f,g:DE，若对每个dD，都有f(d)Eg(d)，就说fD

Eg（逐点地排序）记号从D

到E的连续函数集写成

DE

D

E,D

E若S

D

E是函数集合，且dD，那么S(d)E是由

S(d)={f(d)|f

S}给出的集合4.3论域理论模型和不动点CPO之间的函数集合上的偏序关表4.2从B到B的单调函数

f()f(true)f(false) f()f(true)f(false)f0

f6

false

truef1

true

f7

true

falsef2

falsef8

false

falsef3

true

f9true

true

truef4

false

f10false

false

falsef5

truetruef0f1f2f3f4f5f6f7f8f9f10表4.2从B到B的单调函数f0f1f2f3f4f5f64.3论域理论模型和不动点引理4.6对任何CPOD和E，逐点排序的连续函数集DE也是一个CPO 具体说，若S

DE有向，则作为其最小上界的函数f由f(d)=∨S(d)给出。若E有最小元，则CPO

DE有最小元

DE是一个偏序集合 若E有最小元E，则x:D.E是D

E的最小元 每个有向集合S都有最小上界f f是连续的，即对每个有向的SDE， 有f(∨S)

∨f(S)4.3论域理论模型和不动点引理4.64.3论域理论模型和不动点常用连续函数n元函数：f:D1…DnE连续， 当且仅当它在每个变元上连续配对函数：若SD和TE都有向， 则∨S,∨T=∨{s,t|sS,tT}射影函数：若SDE有向， 则Proji(∨S)=∨{Proji(x)|xS}函数应用：若SDE和TD都有向， 则∨S(∨T)=∨{f(x)|fS,xT}函数合成：若SDE和TEF都有向, 则(∨S)

(∨T)=∨{g

f|fS,gT}4.3论域理论模型和不动点常用连续函数4.3论域理论模型和不动点4.3.4不动点和完备连续层级完备连续层级若有CPOAb0,0,…,Abk,k，则取Ab0,…,Abk为基类型AAA，由逐坐标地定序A所有连续的f:A,A,，由逐点地定序由先前引理，每个A,都是一个CPO这是在CPOAb0,0,…,Abk,k上构造的类型框架4.3论域理论模型和不动点4.3.4不动点和完备连续层4.3论域理论模型和不动点主要结论 任何若干CPO上的完备连续类型层级形成通用模型，并在所有有底元的类型上有最小不动点算子引理4.8若D是有底元CPO，且f:DD连续，则f有最小不动点fixDf=∨{fn()|n0}。此外，映射fixD是连续的先证∨{fn()|n0}是不动点再证它是最小不动点最后证明fixD连续4.3论域理论模型和不动点主要结论4.3论域理论模型和不动点例id:DD是有底元CPO

D上恒等函数，计算fixid

fixid=∨{idn(D)|n0} =∨{

D} =Df

:PNPN，f(A)= A不在A中的最小IN，若它存在的话很容易看出fk()={0,…,k-1}于是fixf=N4.3论域理论模型和不动点例4.3论域理论模型和不动点4.3.5PCF的CPO模型要点考虑PCF语言的论域理论语义APCF 提供对PCF性质的某种透彻理解 提供对PCF进行语义推理的基础PCF等式公理系统对APCF可靠归约系统对APCF也可靠PCF等式证明系统对APCF不可能完备4.4节将考虑等式公理系统的一个扩展，它基于该CPO模型，能证明项之间更多的性质4.3论域理论模型和不动点4.3.5PCF的CPO模4.3论域理论模型和不动点

APCF是N和B上的完全连续体系PCF的类型常量解释为有底元的CPOPCF的所有类型都可以解释为有底元的CPO常量的解释常量0,1,2,…和true，false按通常的方式解释为提升集合N和B上的自然数和布尔值+和Eq?解释为它们普通解释的提升版本和Eq?

nat+

x=x+

nat=nat条件运算的解释需仔细考虑

当M指称而N不是时，iffalsethenMelseN不应该指称4.3论域理论模型和不动点APCF是N和B上的完全4.3论域理论模型和不动点不动点常量按下面定理进行解释 若D是有底元的CPO，且f:DD连续，则f有最小不动点

fixDf=∨{fn()|n0} 此外，映射fixD是连续的结论PCF的每个项在APCF中都有含义4.3论域理论模型和不动点不动点常量按下面定理进行解释4.3论域理论模型和不动点定理4.13令M和N是上的PCF表达式，若 M=N:从PCF的公理可证，则APCF满足等式

M=N:推论4.14 若M:是良类型的PCF项，且MN，则PCF模型APCF满足等式

M=N: