第4章 类型化演算的模型 PCF语言由三部分组成 第2章对代数数据类型进行了透彻的研究 第3章研究简单类型化演算

Presentation on theme: "第4章 类型化演算的模型 PCF语言由三部分组成 第2章对代数数据类型进行了透彻的研究 第3章研究简单类型化演算"— Presentation transcript:

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

2 4.1 引 言 本章的主要内容 递归函数和不动点算子，以及PCF语言的编程实例 基于完全偏序集合的，带不动点算子的类型化演算的论域理论模型
4.1 引 言 本章的主要内容 递归函数和不动点算子，以及PCF语言的编程实例 基于完全偏序集合的，带不动点算子的类型化演算的论域理论模型 不动点归纳法，这是一种对递归定义进行推理的证明方法

3 4.2 递归函数和不动点算子 4.2.1 递归函数和不动点算子 在类型化演算中，可以加递归定义 例：定义阶乘函数和计算5的阶乘
递归函数和不动点算子 4.2.1 递归函数和不动点算子 在类型化演算中，可以加递归定义 letrec f : = M in N f可以出现在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.2 递归函数和不动点算子 从数学的观点看 从计算的观点看 含PCF表达式M的方程f : = M是否都有解？
递归函数和不动点算子 从数学的观点看 含PCF表达式M的方程f : = M是否都有解？ 若有若干个解的话，选择哪个解？ 在讨论PCF的指称语义时解决这些问题 从计算的观点看 递归函数声明有清楚的计算解释 因此，暂且假定每个这样的等式都有解，并在PCF中增加上述表示它的语法

5 4.2 递归函数和不动点算子 函数的不动点 若F : 是类型 到它自身的函数，则F的不动点是使得F (x) = x的值x :
递归函数和不动点算子 函数的不动点 若F : 是类型 到它自身的函数，则F的不动点是使得F (x) = x的值x : 例如，自然数上 平方函数的不动点有0和1 恒等函数有无数个不动点 后继函数没有不动点

6 递归函数和不动点算子 重要联系 递归定义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.if Eq? y 0 then 1 else y  f (y – 1) 的不动点

7 4.2 递归函数和不动点算子 PCF的最后一个基本构造 fix : (  )  , 对每个类型
递归函数和不动点算子 PCF的最后一个基本构造 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

8 4.2 递归函数和不动点算子 fix等式公理 fix归约规则 fix = f :  .f (fix f ) (fix)
递归函数和不动点算子 fix等式公理 fix = f :  .f (fix f ) (fix) fix MM (fix M) （使用( ) 可得） fix归约规则 fix  f : . f (fix f ) (fix)

9 4.2 递归函数和不动点算子 继续阶乘函数的例子 使用fixnatnat，阶乘函数写成
递归函数和不动点算子 继续阶乘函数的例子 使用fixnatnat，阶乘函数写成 fact  fixnatnat F，其中F是表达式 F  f :natnat.y:nat.if Eq? y 0 then 1 else yf (y-1) fact n  fix F n //计算fact n的前几步  F(fix F) n  (f : natnat.y:nat.if Eq? y 0 then 1 else yf(y-1)) (fix F) n  if Eq? n 0 then 1 else n(fix F) (n-1)

10 4.2 递归函数和不动点算子 乘运算的递归定义 基于加运算，并假定有前驱函数pred，它把n > 0映射到n 1，并把0映射到0
递归函数和不动点算子 乘运算的递归定义 基于加运算，并假定有前驱函数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 使用更多语法美化： letrec mult x : nat, y : nat : nat = if Eq? x 0 then 0 else y + mult pred x, y in mult 8, 10

11 4.2 递归函数和不动点算子 4.2.2 有不动点算子的急切归约 考虑fix对各种归约策略的影响 最左归约、惰性归约、并行归约
递归函数和不动点算子 4.2.2 有不动点算子的急切归约 考虑fix对各种归约策略的影响 最左归约、惰性归约、并行归约 只要在原来的公理中增加fix归约公理即可 急切归约 若沿用原来的fix规则，则对变元先求值的要求会导致归约不终止 引入“延迟”（ delay）来暂停对递归定义函数的归约，直到有变元提供给它为止

12 4.2 递归函数和不动点算子 值（在急切归约中需要引入值的概念） 若V是常量、变量、抽象或值的序对，则V是值
递归函数和不动点算子 值（在急切归约中需要引入值的概念） 若V是常量、变量、抽象或值的序对，则V是值 delayMx:.Mx, x在M :  中非自由的 公理 (x :.M)V eager VxM V是值 Proji(V1, V2) eager Vi V1和V2是值 fixV eager V(delay  fixV) V是值 … … 子项规则 和上一章一样

13 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 例：急切归约可能发散（无不动点） let f (x : nat) : nat = 5 in letrec g (x : nat) : nat = g (x +1) in f (g 3)

14 4.3 论域理论模型和不动点 4.3.1 递归定义和不动点算子 用fix归约的特点来启发论域的主要性质 以阶乘函数为例：
4.3 论域理论模型和不动点 4.3.1 递归定义和不动点算子 用fix归约的特点来启发论域的主要性质 以阶乘函数为例： fact  fixnatnat F，其中F是表达式 F  f :natnat.y:nat.if Eq? y 0 then 1 else yf (y-1) 考虑fix F的有限步展开，用另一种方式来理解fact

15 4.3 论域理论模型和不动点 fix F的有限步展开 fix[n]F描述F体的计算最多使用n次的递归计算
4.3 论域理论模型和不动点 fix F的有限步展开 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!}  …

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

17 4.3 论域理论模型和不动点 论域 用集合之间的包含 关系来定义部分函数 之间的偏序 在类型化演算的 论域理论模型中， 类型指称值的偏
4.3 论域理论模型和不动点 论域 用集合之间的包含 关系来定义部分函数 之间的偏序 在类型化演算的 论域理论模型中， 类型指称值的偏 序集合，叫做论域 {0,1,1,1,2,1} 常函数1 阶乘函数 {0,1,1,1,2,2} {0,1,1,1} {0,1}  {0,5} . . . 17

18 4.3 论域理论模型和不动点 计算不终止的项 和递归相联系的一个特别问题是如何给计算不终止的项以合理解释?
4.3 论域理论模型和不动点 计算不终止的项 和递归相联系的一个特别问题是如何给计算不终止的项以合理解释? letrec f : nat  nat = x: nat. f (x1) in f 3 延伸“自然数”论域，包含一个额外的值nat，表示类型nat上的不终止的计算 部分数值函数可看成值域为 {nat}的全函数，在该论域上nat所有的自然数 论域上的偏序可以用来刻画称之为“信息量”或“定义度”的特征 18

19 4.3 论域理论模型和不动点 4.3.2 完全偏序集合、提升和笛卡儿积 定义 偏序集合D,  有自反、反对称和传递关系 的集合D
4.3 论域理论模型和不动点 4.3.2 完全偏序集合、提升和笛卡儿积 定义 偏序集合D,  有自反、反对称和传递关系 的集合D 离散序 指x  y iff x  y。集合有离散的偏序 上界 若D, ，则子集SD的上界是元素xD，使得对任何yS都有y  x 19

20 4.3 论域理论模型和不动点 定义 最小上界 S的一 个上界，它小于等于()S的任何其它上界 有向集合
4.3 论域理论模型和不动点 定义 最小上界 S的一 个上界，它小于等于()S的任何其它上界 有向集合 在D, 中，对子集SD，若每个有限集合S0S都有上界在S中，则称子集S有向 有向集合都非空 若SD是线性序，则S一定有向 线性序 对所有的x, yS，都有x  y或y  x 20

21 4.3 论域理论模型和不动点 例 偏序集合{a0, b0, a1, b1, a2, b2, …}，其中对任意i j
4.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等， 但没有最小上界 a0 a1 a2 b0 b1 b2 ai和bi没有最小上界 21

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

23 4.3 论域理论模型和不动点 定义 有最小元的CPO D  D,  存在元素a，使得对D的任何元素b都有a  b
4.3 论域理论模型和不动点 定义 有最小元的CPO D  D,  存在元素a，使得对D的任何元素b都有a  b 最小元（也叫底元）用D表示 提升集合A A  {} 提升CPO D， 类似地可得到 有底元的CPO D … 1 2 3 4  CPO N的图形表示 23

24 4.3 论域理论模型和不动点 引理4.3 引理4.4 若D是一个CPO，那么D是有底元的CPO
4.3 论域理论模型和不动点 引理4.3 若D是一个CPO，那么D是有底元的CPO 引理4.4 若D和E都是CPO并都有底元，则它们的积DE也是有底元的CPO。而且，若SDE是有向的，则∨S = ∨S1, ∨S2，其中Si= ProjiS 如果D和E分别有最小元D和E，那么D,E是DE 的最小元 24

25 4.3 论域理论模型和不动点 4.3.3 连续函数 CPO上的连续函数 包括了在程序设计中使用的所有普通函数 给出的是一类有不动点的函数
4.3 论域理论模型和不动点 4.3.3 连续函数 CPO上的连续函数 包括了在程序设计中使用的所有普通函数 给出的是一类有不动点的函数 本节证明从一个CPO到另一个CPO的所有连续函数的集合形成一个CPO 在构造把每个类型看成一个CPO的模型时，这是最本质的一步，因为构造这样的模型时，函数类型必须解释成CPO 25

26 4.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)有向 26

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

28 4.3 论域理论模型和不动点 定义 引理4.5 提升函数 如果D和E都是CPO，且f :D  E连续，定义
4.3 论域理论模型和不动点 定义 提升函数 如果D和E都是CPO，且f :D  E连续，定义 f : (D  {})  (E  {})如下： f(d) = if d  D then f(d) else  严格函数 若f 是有底元CPO之间的函数，且f ()   引理4.5 令D和E 都是CPO, 若f:DE连续, 则f:DE严格并连续 28

29 4.3 论域理论模型和不动点 CPO之间的函数集合上的偏序关系 记号
4.3 论域理论模型和不动点 CPO之间的函数集合上的偏序关系 若D = D, D和E = E, E都是CPO，对于连续函数f, g:DE，若对每个dD，都有f(d)E g(d)，就说f D E g（逐点地排序） 记号 从D 到E 的连续函数集写成 DE  D  E, D E 若S  D  E是函数集合，且d D，那么S(d) E是由 S (d) = {f (d) | f S} 给出的集合 29

30 表4.2 从B到B的单调函数 f () f (true) f (false) f () f (true) f (false)
f    f  false true f  true  f  true false f  false  f  false false f   true f true true true f   false f false false false f  true true f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 30

31 4.3 论域理论模型和不动点 引理4.6 对任何CPO D和E，逐点排序的连续函数集DE也是一个CPO
4.3 论域理论模型和不动点 引理4.6 对任何CPO D和E，逐点排序的连续函数集DE也是一个CPO 具体说，若S DE有向，则作为其最小上界的函数f 由f(d) =∨S(d)给出。若E 有最小元，则CPO DE 有最小元 DE 是一个偏序集合 若E有最小元E，则x:D.E是D E 的最小元 每个有向集合S 都有最小上界f f 是连续的，即对每个有向的S  D E ， 有f (∨S)  ∨f (S) 31

32 4.3 论域理论模型和不动点 常用连续函数 n元函数： f :D1 … DnE 连续， 当且仅当它在每个变元上连续
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} 32

33 4.3 论域理论模型和不动点 4.3.4 不动点和完备连续层级 完备连续层级
4.3 论域理论模型和不动点 4.3.4 不动点和完备连续层级 完备连续层级 若有CPOAb0, 0, …, Abk, k，则取Ab0, …, Abk为基类型 A   A A，由 逐坐标地定序 A  所有连续的f : A,   A, ，由逐点地定序 由先前引理，每个A, 都是一个CPO 这是在CPOAb0, 0, …, Abk, k上构造的类型框架 33

34 4.3 论域理论模型和不动点 主要结论 引理4.8 任何若干CPO上的完备连续类型层级形成通用模型，并在所有有底元的类型上有最小不动点算子
4.3 论域理论模型和不动点 主要结论 任何若干CPO上的完备连续类型层级形成通用模型，并在所有有底元的类型上有最小不动点算子 引理4.8 若D是有底元CPO，且f :DD连续，则f 有最小不动点fixD f = ∨{f n () | n  0}。此外，映射fixD是连续的 先证∨{f n () | n  0}是不动点 再证它是最小不动点 最后证明fixD连续 34

35 4.3 论域理论模型和不动点 例 id:DD是有底元CPO D上恒等函数，计算fix id
4.3 论域理论模型和不动点 例 id:DD是有底元CPO D上恒等函数，计算fix id fix id = ∨{ idn (D) | n  0} = ∨{ D} = D f :PNPN，f(A) = A 不在A中的最小IN，若它存在的话 很容易看出f k () = {0, …, k-1} 于是fix f = N 35

36 4.3 论域理论模型和不动点 4.3.5 PCF的CPO模型 要点 考虑PCF语言的论域理论语义APCF 提供对PCF性质的某种透彻理解
4.3 论域理论模型和不动点 PCF的CPO模型 要点 考虑PCF语言的论域理论语义APCF 提供对PCF性质的某种透彻理解 提供对PCF进行语义推理的基础 PCF等式公理系统对APCF可靠 归约系统对APCF也可靠 PCF等式证明系统对APCF不可能完备 4.4节将考虑等式公理系统的一个扩展，它基于该CPO模型，能证明项之间更多的性质 36

37 4.3 论域理论模型和不动点 APCF是N和B上的完全连续体系 常量的解释 PCF的类型常量解释为有底元的CPO
4.3 论域理论模型和不动点 APCF是N和B上的完全连续体系 PCF的类型常量解释为有底元的CPO PCF的所有类型都可以解释为有底元的CPO 常量的解释 常量0,1,2,…和true，false按通常的方式解释为提升集合N和B上的自然数和布尔值 +和Eq?解释为它们普通解释的提升版本和Eq?  nat + x = x +  nat = nat 条件运算的解释需仔细考虑 当M指称而N不是时，if false then M else N不应该指称 37

38 4.3 论域理论模型和不动点 结论 不动点常量按下面定理进行解释 若D是有底元的CPO，且f :DD 连续，则f 有最小不动点
4.3 论域理论模型和不动点 不动点常量按下面定理进行解释 若D是有底元的CPO，且f :DD 连续，则f 有最小不动点 fixD f = ∨{f n() | n  0} 此外，映射fixD是连续的 结论 PCF的每个项在APCF中都有含义 38

39 4.3 论域理论模型和不动点 定理4.13   M =N :从PCF的公理可证， 推论4.14 令M和N是上的PCF表达式，若
4.3 论域理论模型和不动点 定理4.13 令M和N是上的PCF表达式，若   M =N :从PCF的公理可证， 则APCF满足等式  M = N :  推论4.14 若M:是良类型的PCF项，且MN，则PCF模型APCF满足等式   M = N :  39

40 4.3 论域理论模型和不动点 例 (APCF fact)0() = natnat
4.3 论域理论模型和不动点 例 阶乘函数可以写成fact  fixnatnat F，其中 F  f :natnat. y:nat. if Eq? y 0 then 1 else yf (y-1) 可以证明，APCF F是连续的 APCF fact =∨{(APCF fact)n () | n0} (APCF fact)0() = natnat 直接用项来表示相应论域中元素的名字 40

41 4.3 论域理论模型和不动点 (APCF fact)1() = y:nat. if Eq? y 0 then 1
4.3 论域理论模型和不动点 (APCF fact)1() = y:nat. if Eq? y 0 then 1 else y ((APCF fact)0() )(y-1) = y:nat. if Eq? y 0 then 1 else y  (natnat) (y-1) = y:nat. if Eq? y 0 then 1 else nat 41

42 4.3 论域理论模型和不动点 例 考虑函数F : (natnat)  (natnat)，其定义为
4.3 论域理论模型和不动点 例 考虑函数F : (natnat)  (natnat)，其定义为 F f :natnat. x:nat. if Eq? x 1 then 1 else f (x-2) 满足下列条件的函数g:natnat都是上面F的不动点 g(1) = 1 g(x+2) = g(x) 最小不动点是： 当x是奇数时，结果是1 当x是偶数时，计算不终止 42

43 4.4 不动点归纳 例 如果f : D D和g : D D是某个CPO D上的连续函数，则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)) 43

44 4.4 不动点归纳 基于项的CPO解释来扩展证明系统   M = N :    M  N: 
在CPO模型A中，近似  M  N  对环境  是满足的，如果A M  A N (eq) (asym)   M = N :    M  N:    M N : ,   N  M :    M = N:  44

45 4.4 不动点归纳   M N : ,   N  P :    M  P : 
(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 :  

46 4.4 不动点归纳   MN = N :    fix M  N :  用  A表示从一组等式和近似可以证明等式或近
 [/x] A, , [c/x]A [F(c)/x]A  [fix F/x]A 常量c不在A中 (fpind)

47 4.4 不动点归纳 例 证明,如果N是M的一个不动点,那么fix M  N
假定  MN N  ，这就有  MN  N   令A  , x :  x  N :，其中x在N中不是自由的 令不动点归纳规则中F是M 1、首先证明 [/x]A      N : 2、然后取[c/x]A    c  N :作为假设，证明 [Mc/x]A    Mc  N : 根据假设c  N,由单调性，有  Mc  MN : 因为MN  N，所以  Mc  N :

48 习 题 第一次：4.6，4.7，4.12 第二次：4.18，4.25 第三次： 4.30(a)，4.40(b)