第4章 类型化入演算的模型 PCF语言由三部分组成 带函数类型和积类型的纯类型化入演算 自然数类型和布尔类型 不动点算子 第2章对代数数据类型进行了透彻的研究 第3章研究简单类型化入演算 本章先研究递归函数和不动点算子 然后研究类型化入演算的模型，因为第3章的 模型不能解释不动点算子
第4章 类型化演算的模型 • PCF语言由三部分组成 –带函数类型和积类型的纯类型化演算 –自然数类型和布尔类型 –不动点算子 • 第2章对代数数据类型进行了透彻的研究 • 第3章研究简单类型化演算 • 本章先研究递归函数和不动点算子 • 然后研究类型化演算的模型，因为第3章的 模型不能解释不动点算子
4.1引 言 本章的主要内容 递归函数和不动点算子，以及PCF语言的编 程实例 基于完全偏序集合的，带不动点算子的类型 化λ演算的论域理论模型 不动点归纳法，这是一种对递归定义进行推 理的证明方法
4.1 引 言 本章的主要内容 • 递归函数和不动点算子，以及PCF语言的编 程实例 • 基于完全偏序集合的，带不动点算子的类型 化演算的论域理论模型 • 不动点归纳法，这是一种对递归定义进行推 理的证明方法
4.2 递归函数和不动点算子 4.2.1递归函数和不动点算子 在类型化入演算中，可以加递归定义 letrec f:o=Min N -可以出现在M中 -M的类型必须是o,否则等式f=M没有意义 例：定义阶乘函数和计算5的阶乘 letrec f:nat-→nat=入y:nat.(ifEg？y0 then 1 elsey *f(y-1))in f5 把该等式看成关于f的方程：f:nat→nt= Ay nat.if Eg?y 0 then 1 elsey f(y-1)
4.2 递归函数和不动点算子 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.2 递归函数和不动点算子 从数学的观点看 -含PCF表达式M的方程f:o=M是否都有解？ 一若有若干个解的话，选择哪个解？ -在讨论PCF的指称语义时解决这些问题 从计算的观点看 -递归函数声明有清楚的计算解释 因此，暂且假定每个这样的等式都有解，并在 PC℉中增加上述表示它的语法
4.2 递归函数和不动点算子 • 从数学的观点看 – 含PCF表达式M的方程f : = M是否都有解？ – 若有若干个解的话，选择哪个解？ – 在讨论PCF的指称语义时解决这些问题 • 从计算的观点看 – 递归函数声明有清楚的计算解释 – 因此，暂且假定每个这样的等式都有解，并在 PCF中增加上述表示它的语法
4.2 递归函数和不动点算子 函数的不动点 若F:σ→σ是类型σ到它自身的函数，则F的不动 点是使得F(c)=x的值x:σ 例如，自然数上 -平方函数的不动点有0和1 一恒等函数有无数个不动点 一后继函数没有不动点
4.2 递归函数和不动点算子 • 函数的不动点 若F : →是类型 到它自身的函数，则F的不动 点是使得F (x) = x的值x : 例如，自然数上 – 平方函数的不动点有0和1 – 恒等函数有无数个不动点 – 后继函数没有不动点
4.2 递归函数和不动点算子 重要联系 递归定义f:o=M可以用函数入f:c.M来表示，因 为函数入f:c.M的不动点正好是方程f=M的解 (入f:c.M)N=N,即NWIM=N,N是f=M的解 -方程f=M的求解转化为找函数入f:σ.M的不动点 例： 阶乘函数是 入f：nat->nat.y:nat.ifEq？y0then1 elsey *f(y-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.if Eq? y 0 then 1 else y f (y – 1) 的不动点
4.2 递归函数和不动点算子 PCF的最后一个基本构造 fi。:(o→O→o, 对每个类型σ -c。为任何σ到σ的函数产生一个不动点 -letrec声明形式看成是let和不动点算子组合的一 种语法美化 letrec f:o=M in N let f:o=(fix f:o.M)in N 也可用语法美化 letrec f(x:):o=Min N letrec f:T→o=入x:z.MinW
4.2 递归函数和不动点算子 • 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
4.2 递归函数和不动点算子 ”x等式公理 ic。=入f:o-→o.f(fix.f) (fc)】 fi。M=M(fix.M) (使用(B)可得〉 ·x归约规则 fic。→入f:o→of(fixaf) (fix)
4.2 递归函数和不动点算子 • fix等式公理 fix = f : →.f (fix f ) (fix) fix M=M (fix M) （使用( ) 可得） • fix归约规则 fix → f : →. f (fix f ) (fix)
4.2 递归函数和不动点算子 继续阶乘函数的例子 使用fixnat→na, 阶乘函数写成 fact inat >nat F,其中F是表达式 入f:nat-→nat.入y:nat.ifEq？y0then1 else y*f(y-1) fact n≡fix Fn 计算fact n的前几步 F(fix F)n ≡（入f:nat->nat.入y:nat.ifEg？y0then1 else y*f(yv-1))(fix F)n if Eg?n 0 then 1 else n*(fix F)(n-1)
4.2 递归函数和不动点算子 • 继续阶乘函数的例子 使用fixnat→nat，阶乘函数写成 fact fixnat→nat F，其中F是表达式 F f :nat→nat.y:nat.if Eq? y 0 then 1 else yf (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 yf(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 x nat-→nat=入p:nat×nat. if Eg?(Proj p)0 then 0 else (Projz p)+mult (pred (Proj p),Projz p) in mult(8,10》 使用更多语法美化： letrec mult (x:nat,y nat)nat=if Eg?x 0 then 0 else y mult (predx,y)in mult (8,10)
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 – 使用更多语法美化： letrec mult x : nat, y : nat : nat = if Eq? x 0 then 0 else y + mult pred x, y in mult 8, 10
