4.3
论域理论模型和不动点常用连续函数n元函数：f:D1?…?Dn?E连续， 当且仅当它在每个变元上连续配对
函数：若S?D和T?E都有向， 则?∨S,∨T?=∨{?s,t?|s?S,t?T}射影函数
：若S?D?E有向， 则Proji(∨S)=∨{Proji(x)|x?S}函数应用：若S?D?E和
T?D都有向， 则∨S(∨T)=∨{f(x)|f?S,x?T}函数合成：若S?D?E和T?
E?F都有向, 则(∨S)?(∨T)=∨{g?f|f?S,g?T}4.3论域理论模型和不动点4.3.
4不动点和完备连续层级完备连续????层级若有CPO?Ab0,?0?,…,?Abk,?k?，则取Ab0,…,A
bk为基类型A????A??A?，由????逐坐标地定序A????所有连续的f:?A?,?????
A?,???，由????逐点地定序由先前引理，每个?A?,???都是一个CPO这是在CPO?Ab0,?0?,…,?
Abk,?k?上构造的类型框架4.3论域理论模型和不动点主要结论 任何若干CPO上的完备连续类型层级形成通用模型，并
在所有有底元的类型上有最小不动点算子引理4.8若D是有底元CPO，且f:D?D连续，则f有最小不动点fixDf
=∨{fn(?)|n?0}。此外，映射fixD是连续的先证∨{fn(?)|n?0}是不动点再证
它是最小不动点最后证明fixD连续4.3论域理论模型和不动点例id:D?D是有底元CPOD上恒等函数，计算fix
id fixid=∨{idn(?D)|n?0} =∨{?D} =?Df:PN?PN，f(
A)= A??不在A中的最小I?N，若它存在的话?很容易看出fk(?)={0,…,k-1}于是fix
f=N4.3论域理论模型和不动点4.3.5PCF的CPO模型要点考虑PCF语言的论域理论语义APCF 提供
对PCF性质的某种透彻理解 提供对PCF进行语义推理的基础PCF等式公理系统对APCF可靠归约系统对APCF也可靠P
CF等式证明系统对APCF不可能完备4.4节将考虑等式公理系统的一个扩展，它基于该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论域理论模型和不动点
不动点常量按下面定理进行解释 若D是有底元的CPO，且f:D?D连续，则f有最小不动点 fixDf=∨{fn
(?)|n?0} 此外，映射fixD是连续的结论PCF的每个项在APCF中都有含义4.3论域理论模型和不动
点定理4.13令M和N是?上的PCF表达式，若 ??M=N:?从PCF的公理可证，则APCF满足等式??M
=N:?推论4.14www.guiwenji.com盗墓笔记 若??M:?是良类型的PCF项，且M?N，则PCF模型
APCF满足等式 ??M=N:?4.3论域理论模型和不动点例阶乘函数可以写成fact?fixnat?n
atF，其中F??f:nat?nat.?y:nat.ifEq?y0then1 elsey?
f(y-1)可以证明，APCF?F?是连续的APCF?fact?=∨{(APCF?fact?)n(?)|n
?0}(APCF?fact?)0(?)=?nat?nat直接用?项来表示相应论域中元素的名字4.3论域理论模型
和不动点 (APCF?fact?)1(?)=?y:nat.ifEq?y0then1 elsey?
((APCF?fact?)0(?))(y-1)=?y:nat.ifEq?y0then1elsey?(
?nat?nat)(y-1)=?y:nat.ifEq?y0then1else?nat4.3论域理论模型
和不动点例 考虑函数F:(nat?nat)?(nat?nat)，其定义为F??f:nat?nat.?
x:nat.ifEq?x1then1elsef(x-2) 满足下列条件的函数g:nat?nat都是上面F的
不动点 g(1)=1 g(x+2)=g(x) 最小不动点是： 当x是奇数时，结果是1 当x是偶数
时，计算不终止4.4不动点归纳例如果f:D?D和g:D?D是某个CPOD上的连续函数，则fix(f?g)
=f(fix(g?f))fix(f?g)=∨{(f?g)i(?)|i?0} =∨{?,(
f?g)(?),(f?g?f?g)(?),…} =∨{f(?),(f?(g?f))(?
),(f?(g?f)2)(?),...} =∨{(f?(g?f)i)(?)|i?0}
=f(fix(g?f)) 仅使用PCF的等式证明系统不可能证明 fix(f?g)=f(fix(g?f))
4.4不动点归纳基于项的CPO解释来扩展证明系统在CPO模型A中，近似??M?N??对环境???是满足的，
如果A?M???A?N?? (eq) (asym)??M
=N:???M?N:???M?N:?,??N?M:???M=N:?
4.4不动点归纳 (trans)?????M?? (bot)
??????=?x:?.??:??? (botf) (acong)
(fcong)??M?N:?,??N?P:???M?P:?
??M1?M2:???,??N1?N2:???M1N1?M2N2:??,x:
??M?N:????x:?.M??x:?.N:???4.4不动点归纳
用??A表示从一组等式和近似?可以证明等式或近似A ??MN=N:
???fixM?N:???[?/x]A,?,[c/x]A?[F(c)/x]A??[fix
F/x]A常量c不在A中(fpind)4.4不动点归纳例证明,如果N是M的一个不动点,那么fixM?N假定
??MN?N??，这就有??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,由单调性，有??M
c?MN:?因为MN?N，所以??Mc?N:?第一次：4.6，4.7，4.12第二次：4.18
，4.25第三次：4.30(a)，4.40(b)习题
中国科大第4章类型化?演算的模型PCF语言由三部分组成带函
数类型和积类型的纯类型化?演算自然数类型和布尔类型不动点算子第2章对代数数据类型进行了透彻的研究第3章研究简单类型化?演算
本章先研究递归函数和不动点算子然后研究类型化?演算的模型，因为第3章的模型不能解释不动点算子4.1引言本章的主要
内容递归函数和不动点算子，以及PCF语言的编程实例基于完全偏序集合的，带不动点算子的类型化?演算的论域理论模型不动点归纳法，
这是一种对递归定义进行推理的证明方法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递归函数和不动点
算子从数学的观点看含PCF表达式M的方程f:?=M是否都有解？若有若干个解的话，选择哪个解？在讨论PCF的指称语义时
解决这些问题从计算的观点看递归函数声明有清楚的计算解释因此，暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法
4.2递归函数和不动点算子函数的不动点若F:???是类型?到它自身的函数，则F的不动点是使得F(x)=x
的值x:?例如，自然数上平方函数的不动点有0和1恒等函数有无数个不动点后继函数没有不动点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递归函数和不动点算子PCF的最后一个基本构造 f
ix?:(???)??, 对每个类型?fix?为任何?到?的函数产生一个不动点letrec声明形式看成是
let和不动点算子组合的一种语法美化 letrecf:??MinN? letf:?=(fix?
?f:?.M)inN也可用语法美化 letrecf(x:?):?=MinN? letre
cf:?????x:?.MinN4.2递归函数和不动点算子fix等式公理 fix?=?f:?
??.f(fix?f) (fix) fix?M?M(fix?M) （使用(?)可得）fix归约规则
fix???f:???.f(fix?f) (fix)4.2递归函数和不动点算子继续阶乘函数的例子
使用fixnat?nat，阶乘函数写成 fact?fixnat?natF，其中F是表达式 F??f:nat?nat
.?y:nat.ifEq?y0then1 elsey?f(y-1)factn?fixFn
//计算factn的前几步 ?F(fixF)n ?(?f:nat?nat.?y:nat.ifEq?y0
then1 elsey?f(y-1))(fixF)n ?ifEq?n0then1else
n?(fixF)(n-1)4.2递归函数和不动点算子乘运算的递归定义基于加运算，并假定有前驱函数pred，它把n
>0映射到n?1，并把0映射到0letrecmult:nat?nat?nat=?p:nat?nat
. ifEq?(Proj1p)0then0 else(Proj2p)+mult?pred(Pr
oj1p),Proj2p?inmult?8,10?使用更多语法美化：letrecmult?x:
nat,y:nat?:nat=ifEq?x0then0elsey+mult?predx
,y?inmult?8,10?4.2递归函数和不动点算子4.2.2有不动点算子的急切归约考虑fix对各种
归约策略的影响最左归约、惰性归约、并行归约 只要在原来的公理中增加fix归约公理即可急切归约 若沿用原来的fix规则，
则对变元先求值的要求会导致归约不终止 引入“延迟”（delay）来暂停对递归定义函数的归约，直到有变元提供给它为止4.2
递归函数和不动点算子值（在急切归约中需要引入值的概念）若V是常量、变量、?抽象或值的序对，则V是值delay????
M???x:?.Mx,x在M:???中非自由的公理(?x:?.M)V?eager?V?x?M V是值P
roji(V1,V2)?eagerVi V1和V2是值fix???V?eagerV(delay????fix?
??V?) V是值……子项规则和上一章一样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?eager3例：急切归约可能发散（无不动点）letf(x:nat):
nat=5in letrecg(x:nat):nat=g(x+1)inf(g3)4.3
论域理论模型和不动点4.3.1递归定义和不动点算子用fix归约的特点来启发论域的主要性质以阶乘函数为例： fact?
fixnat?natF，其中F是表达式 F??f:nat?nat.?y:nat.ifEq?y0then1
elsey?f(y-1)考虑fixF的有限步展开，用另一种方式来理解fact4.3论域理论模型和不动点
fixF的有限步展开www.libaiwu.com官场小说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对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!?}?…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论域理论模型和不动点论域用集合之间的包含关系来定义部分函数之间的偏序
在类型化?演算的论域理论模型中，类型指称值的偏序集合，叫做论域{?0,1?,?1,1?,?2,1?}常函数1阶乘函数
{?0,1?,?1,1?,?2,2?}{?0,1?,?1,1?}{?0,1?}?{?0,5?}......
..................4.3论域理论模型和不动点计算不终止的项和递归相
联系的一个特别问题是如何给计算不终止的项以合理解释? letrecf:nat?nat=?x:nat.f(x?
1)inf3延伸“自然数”论域，包含一个额外的值?nat，表示类型nat上的不终止的计算部分数值函数可看成值域为?
?{?nat}的全函数，在该论域上?nat?所有的自然数论域上的偏序可以用来刻画称之为“信息量”或“定义度”的特征4.3
论域理论模型和不动点4.3.2完全偏序集合、提升和笛卡儿积定义偏序集合?D,?? 有自反、反对称和传递关系?的集合
D离散序 指x?yiffx?y。集合有离散的偏序上界 若?D,??，则子集S?D的上界是元素x?D，使得
对任何y?S都有y?x4.3论域理论模型和不动点定义最小上界 S的一个上界，它小于等于(?)S的任何其它上界
有向集合 在?D,??中，对子集S?D，若每个有限集合S0?S都有上界在S中，则称子集S有向 有向集合都非空 若S?D是
线性序，则S一定有向线性序 对所有的x,y?S，都有x?y或y?x4.3论域理论模型和不动点例
偏序集合{a0,b0,a1,b1,a2,b2,…}，其中对任意i?j都有ai?aj,bj并且bi?aj,
bj两个线性序 a0?a1?a2?…，和 b0?b1?b2?…{ai,bi} 有上界ai+1和bi+1等， 但
没有最小上界a0a1a2b0b1b2ai和bi没有最小上界4.3论域理论模型和不动点定义完全偏序集
合?D,??（简称CPO） 若每个有向集合S?D都有最小上界（∨S）例使用离散序，任何集合都可看成CPO任何有限
偏序集合都是CPO考虑普通算术序，自然数集合不是CPO有理数的非平凡闭区间不是CPO，所有小于的有理数的最小上界是无理数
若S，T?D都有向，且S的每个元素都?T的某个元素，那么∨S?∨T24.3论域理论模型和不动点定义有最小元的
CPOD??D,?? 存在元素a，使得对D的任何元素b都有a?b 最小元（也叫底元）用?D表示提升集合A?
A?{?}提升CPOD， 类似地可得到 有底元的CPOD?…01234?CPON?的图
形表示4.3论域理论模型和不动点引理4.3若D是一个CPO，那么D?是有底元的CPO引理4.4若D和E都是CPO
并都有底元，则它们的积D?E也是有底元的CPO。而且，若S?D?E是有向的，则∨S=?∨S1,∨S2?，其中Si=Proj
iS 如果D和E分别有最小元?D和?E，那么??D,?E?是D?E的最小元4.3论域理论模型和不动点4.3.3连续函
数CPO上的连续函数包括了在程序设计中使用的所有普通函数给出的是一类有不动点的函数本节证明从一个CPO到另一个CP
O的所有连续函数的集合形成一个CPO在构造把每个类型看成一个CPO的模型时，这是最本质的一步，因为构造这样的模型时，函数类型必
须解释成CPO4.3论域理论模型和不动点记号如果f:D?E是函数，如果S?D，用记号f(S)表示E的子集：
f(S)={f(d)|d?S}定义单调函数 若D=?D,?D?和E=?E,?E?都是CPO，且f:
D?E是它们基础集合上的函数，若d?d?蕴涵f(d)?f(d?),则f单调 若f单调且S有向，则f(S)有向
4.3论域理论模型和不动点定义连续函数www.zw360.com360小说 单调，且 若对每个有向的S?D
，都有f(∨S)?∨f(S)例在实轴闭区间[x,y]上，若把[x,y]看成CPO时，则通常计算意义下的连续函数仍
然连续任何CPO上的常函数是平凡地连续的若D是离散序，则D上每个函数都连续从提升集合A?到任何CPO的单调函数连续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:D?E连续,则f?:D??E?严格并连续
4.3论域理论模型和不动点CPO之间的函数集合上的偏序关系若D=?D,?D?和E=?E,?E?都是CPO，
对于连续函数f,g:D?E，若对每个d?D，都有f(d)?Eg(d)，就说f?D?Eg（逐点地排序）记号从D到E
的连续函数集写成 D?E??D?E,?D?E?若S?D?E是函数集合，且d?D，那么S(d)?E
是由 S(d)={f(d)|f?S}给出的集合表4.2从B?到B?的单调函数 f(?)f
(true)f(false) f(?)f(true)f(false)
f0??? f6?
falsetruef1?true?
f7?truefalsef2?
false?f8?
falsefalsef3??truef9truetruetruef4??falsef10falsefalsefalsef5?truetruef0f1f2f3f4f5f6f7f8f9f104.3论域理论模型和不动点引理4.6对任何CPOD和E，逐点排序的连续函数集D?E也是一个CPO 具体说，若S?D?E有向，则作为其最小上界的函数f由f(d)=∨S(d)给出。若E有最小元，则CPOD?E有最小元 D?E是一个偏序集合 若E有最小元?E，则?x:D.?E是D?E的最小元 每个有向集合S都有最小上界f f是连续的，即对每个有向的S?D?E， 有f(∨S)?∨f(S)中国科大 |
|
