类型化演算的模型

1、第第4章章 类型化类型化 演算的模型演算的模型 PCF语言由三部分组成语言由三部分组成带函数类型和积类型的纯类型化带函数类型和积类型的纯类型化 演算演算自然数类型和布尔类型自然数类型和布尔类型不动点算子不动点算子 第第2章对代数数据类型进行了透彻的研究章对代数数据类型进行了透彻的研究 第第3章研究简单类型化章研究简单类型化 演算演算 本章先研究递归函数和不动点算子本章先研究递归函数和不动点算子 然后研究类型化然后研究类型化 演算演算的的模型，因为第模型，因为第3章的章的模型不能解释不动点算子模型不能解释不动点算子4.1 引引 言言本章的主要内容本章的主要内容 递归函数和不动点算子，以及递归函数

2、和不动点算子，以及PCF语言的编语言的编程实例程实例 基于完全偏序集合的，带不动点算子的类型基于完全偏序集合的，带不动点算子的类型化化 演算的论域理论模型演算的论域理论模型 不动点归纳法，这是一种对递归定义进行推不动点归纳法，这是一种对递归定义进行推理的证明方法理的证明方法4.2 递归函数和不动点算子递归函数和不动点算子4.2.1 递归函数和不动点算子递归函数和不动点算子 在类型化在类型化 演算中，可以加递归定义演算中，可以加递归定义letrec f : = M in Nf可以出现在可以出现在M中中M的类型必须是的类型必须是 ，否则等式，否则等式f = M没有意义没有意义 例：例：定义阶乘函数

3、和计算定义阶乘函数和计算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.2 递归函数和不动点算子递归函数和不动点算子 从数学的观点看从数学的观点看 含含PCF表达式表达式M的方程的方程f : = M是否都有解？是否都有解？ 若若有若干个解的话，选择哪个解？有若干个解的话，选择哪个解？ 在讨论在讨论PCF的指称语义时解决这些问题的指

4、称语义时解决这些问题 从计算的观点看从计算的观点看 递归函数声明有清楚的计算解释递归函数声明有清楚的计算解释 因此因此，暂且假定每个这样的等式都有解，并在暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法中增加上述表示它的语法4.2 递归函数和不动点算子递归函数和不动点算子 函数的不动点函数的不动点若若F : 是类型是类型 到它到它自身自身的函数，的函数，则则F的不动的不动点是使得点是使得F (x) = x的值的值x : 例如，自然数上例如，自然数上 平方函数的不动点有平方函数的不动点有0和和1 恒等函数有无数个不动点恒等函数有无数个不动点 后继函数没有不动点后继函数没有不动点4.

5、2 递归函数和不动点算子递归函数和不动点算子 重要联系重要联系 递归定义递归定义f : = M可以用函数可以用函数 f : .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.2 递归函数和不动点算子递归函数和不动点算子 P

6、CF的最后的最后一个一个基本构造基本构造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 N4.2 递归函数和不动点算子递归函数和不动点算子 fix等式公理等式公理fix = f : . .f (fix f )

7、(fix)fix M M (fix M)（使用使用( ) 可得可得） fix归约规则归约规则fix f : . f (fix f )(fix)4.2 递归函数和不动点算子递归函数和不动点算子 继续阶乘函数的例子继续阶乘函数的例子使用使用fixnatnat，阶乘函数写成阶乘函数写成fact fixnatnat F，其中其中F是表达式是表达式F f :natnat. y:nat.if Eq? y 0 then 1else y f (y-1)fact n fix F n/计算计算fact n的前几步的前几步 F(fix F) n ( f : natnat. y:nat.if Eq? y 0 then

8、 1else y f(y-1) (fix F) n if Eq? n 0 then 1 else n (fix F) (n-1)4.2 递归函数和不动点算子递归函数和不动点算子 乘运算乘运算的递归定义的递归定义 基于加运算基于加运算，并，并假定有前驱函数假定有前驱函数pred，它把，它把n 0映射到映射到n 1，并把并把0映射到映射到0 letrec 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 使用更

9、多语法美化：使用更多语法美化： letrec mult x : nat, y : nat : nat = if Eq? x 0 then 0 else y + mult pred x, y in mult 8, 10 4.2 递归函数和不动点算子递归函数和不动点算子4.2.2 有不动点算子的急切归约有不动点算子的急切归约考虑考虑fix对各种归约策略的影响对各种归约策略的影响 最左归约最左归约、惰性归约惰性归约、并行归约、并行归约只要只要在原来的在原来的公理中公理中增加增加fix归约公理归约公理即可即可 急切归约急切归约若若沿用原来的沿用原来的fix规则，规则，则对则对变元先求值的要求变元先求值

10、的要求会导致归约不终止会导致归约不终止引入引入“延迟延迟”（ delay）来）来暂停对递归定义函数暂停对递归定义函数的归约的归约，直到直到有有变元提供给它为止变元提供给它为止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

11、(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 eager 3 例：例

12、：急切归约急切归约可能发散（无不动点）可能发散（无不动点）let f (x : nat) : nat = 5 inletrec g (x : nat) : nat = g (x +1) in f (g 3)4.3 论域理论模型和不动点论域理论模型和不动点4.3.1 递归定义和不动点算子递归定义和不动点算子 用用fix归约的特点来启发论域的主要性质归约的特点来启发论域的主要性质 以阶乘函数为例：以阶乘函数为例：fact fixnatnat F，其中其中F是表达式是表达式F f :natnat. y:nat.if Eq? y 0 then 1else y f (y-1) 考虑考虑fix F的有限步

13、展开，用另一种方式来理解的有限步展开，用另一种方式来理解fact4.3 论域理论模型和不动点论域理论模型和不动点 fix F的有限步展开的有限步展开fixnF描述描述F体的计算最多使用体的计算最多使用n次的递归计算次的递归计算 fix0F = diverge （表示处处无定义的函数表示处处无定义的函数） fixn+1F = F(fixnF) (fix2F) 0 = 1，(fix2F)1 = 1，(fix2F) n对对n 2没没有定义有定义 把函数把函数看成二元组的集合后看成二元组的集合后，fixn 1F = (fixnF) n, n ，真包含所有的真包含所有的fixiF (i n) 即即 0,

14、 0! 0, 0! , 1, 1! 0, 0! , 1, 1! , 2, 2! 4.3 论域理论模型和不动点论域理论模型和不动点n( fixnF)和和F的不动点的不动点 让让fact = n( fixnF)是有直观计算意义的是有直观计算意义的 尚不足以相信，对任意的尚不足以相信，对任意的F， n( fixnF)就是就是F的不动点的不动点 强加一些相对自然的条件到强加一些相对自然的条件到F才能保证这一点才能保证这一点 当用集合包含对部分函数排序时，当用集合包含对部分函数排序时， n( fixnF)将将是是F的最小不动点的最小不动点4.3 论域理论模型和不动点论域理论模型和不动点 论域论域 用集合

15、之间的包含用集合之间的包含关系来定义部分函数关系来定义部分函数之间的偏序之间的偏序 在类型化在类型化 演算的演算的论域理论模型中，论域理论模型中，类型指称值的偏类型指称值的偏序集合，叫做序集合，叫做论域论域 0,1 , 1,1 , 2,1 常函数常函数1阶乘函数阶乘函数 0,1 , 1,1 , 2,2 0,1 , 1,1 0,1 0,5 . . . . . . . . . . . . . . . . .4.3 论域理论模型和不动点论域理论模型和不动点 计算不终止的项计算不终止的项 和递归相联系的一个特别问题是如何给计算不终和递归相联系的一个特别问题是如何给计算不终止的项以合理解释止的项以合理解

16、释?letrec f : nat nat = x: nat. f (x 1) in f 3 延伸延伸“自然数自然数”论域，包含一个额外的值论域，包含一个额外的值 nat，表示类型表示类型nat上的不终止的计算上的不终止的计算 部分数值函数可看成值域为部分数值函数可看成值域为 nat的全函数，的全函数，在该论域上在该论域上 nat所有的自然数所有的自然数 论域上的偏序可以用来论域上的偏序可以用来刻画称之为刻画称之为“信息量信息量”或或“定义度定义度”的特征的特征4.3 论域理论模型和不动点论域理论模型和不动点4.3.2 完全偏序集合、提升和笛卡儿积完全偏序集合、提升和笛卡儿积 定义定义 偏序集合

17、偏序集合 D, 有自反、反对称和传递关系有自反、反对称和传递关系 的集合的集合D 离散序离散序 指指x y iff x y。集合有离散的偏序。集合有离散的偏序上界上界若若 D, ，则子集，则子集S D的的上界上界是元素是元素x D，使得使得对任何对任何y S都有都有y x4.3 论域理论模型和不动点论域理论模型和不动点 定义定义 最小上界最小上界S的一的一 个上界，它小于等于个上界，它小于等于()S的任何其它上的任何其它上界界 有向集合有向集合在在 D, 中，对子集中，对子集S D，若每个有限集合，若每个有限集合S0 S都有上界在都有上界在S中，则称子集中，则称子集S有向有向有向集合都非空有向

18、集合都非空若若S D是线性序，则是线性序，则S一定有向一定有向 线性序线性序对所有的对所有的x, y S，都有，都有x y或或y x 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 论域理论模型和不动点论域理论模型和不动点 定义定义 完全偏序

19、集合完全偏序集合 D, （简称（简称CPO） 若若每个有向集合每个有向集合S D都有最小上界（都有最小上界（S） 例例 使用离散序，任何集合都可看成使用离散序，任何集合都可看成CPO 任何有限偏序集合都是任何有限偏序集合都是CPO 考虑普通算术序，自然数集合不是考虑普通算术序，自然数集合不是CPO 有理数的非平凡闭区间不是有理数的非平凡闭区间不是CPO，所有所有小于小于的有理数的最小上界是无理数的有理数的最小上界是无理数 若若S，T D都有向，且都有向，且S的每个元素都的每个元素都T的某个的某个元素，那么元素，那么S T24.3 论域理论模型和不动点论域理论模型和不动点 定义定义 有最小元有最

20、小元的的CPO D D, 存在元素存在元素a，使得对使得对D的任何元素的任何元素b都有都有a b 最小元（也叫底元最小元（也叫底元）用）用 D表示表示 提升集合提升集合A A 提升提升CPO D，类似地可得到类似地可得到有底元的有底元的CPO D 01234 CPO N 的图形表示的图形表示4.3 论域理论模型和不动点论域理论模型和不动点 引理引理4.3 若若D是一个是一个CPO，那么，那么D 是有底元的是有底元的CPO 引理引理4.4 若若D和和E都是都是CPO并都有底元，则它们的积并都有底元，则它们的积D E也是有底元的也是有底元的CPO。而且，若而且，若S D E是有向的，是有向的，则则

21、S = S1, S2 ，其中其中Si= ProjiS如果如果D和和E分别有最小元分别有最小元 D和和 E，那么那么D, , E 是是D E 的最小元的最小元4.3 论域理论模型和不动点论域理论模型和不动点4.3.3 连续函数连续函数 CPO上的连续函数上的连续函数 包括了在程序设计中使用的所有普通函数包括了在程序设计中使用的所有普通函数 给出的是一类有不动点的函数给出的是一类有不动点的函数 本节证明从一个本节证明从一个CPO到另一个到另一个CPO的所有连续函的所有连续函数的集合形成一个数的集合形成一个CPO 在构造把每个类型看成一个在构造把每个类型看成一个CPO的模型时，这是的模型时，这是最本

22、质的一步，因为构造这样的模型时，函数类型最本质的一步，因为构造这样的模型时，函数类型必须解释成必须解释成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是它们基础集合上的函数，是它们基础集合上的函数，若若dd 蕴涵蕴涵 f(d) f (d ),则则f 单调单调若若f 单调且单调且S有向，则有向，则f (S)有向有向4.3 论域理论模型和

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

24、PO，且且f :D E连续，定义连续，定义f : (D ) (E )如下：如下： f (d) = if d D then f(d) else 严格函数严格函数若若f 是有底元是有底元CPO之间的函数，且之间的函数，且f ( ) 引理引理4.5 令令D和和E 都是都是CPO, , 若若f:DE连续连续, , 则则f :D E 严格并连续严格并连续4.3 论域理论模型和不动点论域理论模型和不动点 CPO之间的函数之间的函数集合上的偏序关系集合上的偏序关系 若若D = D, D 和和E = E, E 都是都是CPO，对于连续对于连续函数函数f, g:DE，若对每个若对每个d D，都有都有f(d)E

25、g(d)，就说就说f D E g（逐点地排序逐点地排序） 记号记号 从从D 到到E 的连续函数集写成的连续函数集写成DE D E, D E 若若S D E是函数集合，且是函数集合，且d D，那么那么S(d) E是由是由S (d) = f (d) | f S给出的集合给出的集合范文精选网http:/ 范文大全http:/ 范文表表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 t

26、rue f9 true true truef4 false f10 false false falsef5 true truef0f1f2f3f4f5f6f7f8f9f104.3 论域理论模型和不动点论域理论模型和不动点 引理引理4.6 对任何对任何CPO D和和E，逐点排序的连续函数集逐点排序的连续函数集DE也是一个也是一个CPO具体说，若具体说，若S DE有向，则作为其最小上界的有向，则作为其最小上界的函数函数f 由由f(d) =S(d)给出。若给出。若E 有最小元，则有最小元，则CPO DE 有最小元有最小元DE 是一个偏序集合是一个偏序集合若若E有最小元有最小元 E，则则 x:D. .

27、 E是是D E 的最小元的最小元每个有向集合每个有向集合S 都有最小上界都有最小上界ff 是是连续的，即对每个有向的连续的，即对每个有向的S D E ，有有f (S) f (S)4.3 论域理论模型和不动点论域理论模型和不动点 常用连续函数常用连续函数 n元函数：元函数： f :D1 DnE 连续，连续，当且仅当它在每个变元上连续当且仅当它在每个变元上连续 配对函数：若配对函数：若S D和和T E都有向，都有向， 则则 S, T = s, t | s S, t T 射影函数：射影函数：若若S D E有向，有向， 则则Proji(S)= Proji(x) | x S 函数应用：函数应用：若若S

28、DE和和T D都有向，都有向， 则则S(T) = f (x) | f S, x T 函数合成：函数合成：若若S DE和和T EF都有向都有向, ,则则(S) (T) =g f | f S, g T4.3 论域理论模型和不动点论域理论模型和不动点4.3.4 不动点和完备连续层级不动点和完备连续层级 完备连续完备连续 层级层级 若有若有CPO Ab0, 0 , , Abk, k ，则取则取Ab0, , Abk为基类型为基类型 A A A ，由由 逐坐标地定序逐坐标地定序 A 所有连续的所有连续的f : A , A , ，由由 逐点地定序逐点地定序 由先前引理，每个由先前引理，每个 A , 都是一个

29、都是一个CPO这是在这是在CPO Ab0, 0 , , Abk, k 上上构造的类型框构造的类型框架架4.3 论域理论模型和不动点论域理论模型和不动点 主要结论主要结论 任何任何若干若干CPO上的完备连续类型层级形成通用上的完备连续类型层级形成通用模型，并在所有有底元的类型上有最小不动点算子模型，并在所有有底元的类型上有最小不动点算子 引理引理4.8 若若D是有底元是有底元CPO，且且f :DD连续，则连续，则f 有最小有最小不动点不动点fixD f = f n ( ) | n 0。此外，映射。此外，映射fixD是是连续的连续的 先证先证f n ( ) | n 0是不动点是不动点 再证它是最小

30、不动点再证它是最小不动点 最后证明最后证明fixD连续连续4.3 论域理论模型和不动点论域理论模型和不动点 例例 id:DD是有底元是有底元CPO D上恒等函数上恒等函数，计算，计算fix idfix id = idn ( D) | n 0= D= D f :PNPN，f(A) =A 不在不在A中的最小中的最小I N，若它存在的话若它存在的话 很容易看出很容易看出f k () = 0, , k-1 于是于是fix f = N4.3 论域理论模型和不动点论域理论模型和不动点4.3.5 PCF的的CPO模型模型 要点要点 考虑考虑PCF语言的论域语言的论域理论语义理论语义APCF提供对提供对PCF

31、性质的某种透彻理解性质的某种透彻理解提供对提供对PCF进行语义推理的基础进行语义推理的基础 PCF等式公理系统对等式公理系统对APCF可靠可靠 归约系统对归约系统对APCF也可靠也可靠 PCF等式证明系统对等式证明系统对APCF不可能完备不可能完备 4.4节将考虑等式公理系统的一个扩展，它基于该节将考虑等式公理系统的一个扩展，它基于该CPO模型，能证明项之间更多的性质模型，能证明项之间更多的性质4.3 论域理论模型和不动点论域理论模型和不动点 APCF是是N 和和B 上的完全连续体系上的完全连续体系 PCF的类型常量解释为有底元的的类型常量解释为有底元的CPO PCF的所有类型都可以解释为有底

32、元的的所有类型都可以解释为有底元的CPO 常量的解释常量的解释常量常量0,1,2,和和true，false按通常的方式解释为提按通常的方式解释为提升集合升集合N 和和B 上的自然数和布尔值上的自然数和布尔值 +和和Eq?解释为它们普通解释的提升版本解释为它们普通解释的提升版本 和和Eq? nat + x = x + nat = nat条件运算的解释需仔细考虑条件运算的解释需仔细考虑当当M指称指称 而而N不是时，不是时，if false then M else N不不应该指称应该指称 4.3 论域理论模型和不动点论域理论模型和不动点 不动点不动点常量常量按下面定理进行解释按下面定理进行解释若若D

33、是有底元的是有底元的CPO，且且f :DD 连续，则连续，则f 有有最小不动点最小不动点fixD f = f n( ) | n 0 此外，映射此外，映射fixD是连续的是连续的 结论结论 PCF的每个项在的每个项在APCF中都有含义中都有含义4.3 论域理论模型和不动点论域理论模型和不动点 定理定理4.13令令M和和N是是 上的上的PCF表达式，若表达式，若 M =N : 从从PCF的公理可证，的公理可证，则则APCF满足等式满足等式 M = N : 推论推论4.14若若 M: 是良类型的是良类型的PCF项，且项，且MN，则则PCF模型模型APCF满足等式满足等式 M = N : 4.3 论域

34、理论模型和不动点论域理论模型和不动点 例例阶乘函数可以写成阶乘函数可以写成fact fixnatnat F，其中其中F f :natnat. y:nat. if Eq? y 0 then 1else y f (y-1) 可以可以证明，证明，APCF F是连续的是连续的 APCF fact = =(APCF fact)n ( ) | n 0 (APCF fact)0( ) = natnat 直接用直接用 项来表示相应论域中元素的名字项来表示相应论域中元素的名字4.3 论域理论模型和不动点论域理论模型和不动点(APCF fact)1( ) = y:nat. if Eq? y 0 then 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 nat4.3 论域理论模型和不动点论域理论模型和不动点 例例考虑函数考虑函数F : (natnat) (natnat)，其定义为其定义为 F f :natnat. x:nat. if Eq? x 1 then 1 else f (x-2)