第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 – 恒等函数有无数个不动点 – 后继函数没有不动点