中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第4章 类型化λ演算的模型

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 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)

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