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)