第3章 简单类型化)演算 函数式程序设计语言PCF由三部分组成 代数数据类型：自然数类型和布尔类型等 带函数和积等类型的纯类型化入演算 不动点算子 第2章对代数数据类型进行了透彻的研究 本章研究简单类型化入演算 第4章研究不动点算子
第3章 简单类型化演算 • 函数式程序设计语言PCF由三部分组成 –代数数据类型：自然数类型和布尔类型等 –带函数和积等类型的纯类型化演算 –不动点算子 • 第2章对代数数据类型进行了透彻的研究 • 本章研究简单类型化演算 • 第4章研究不动点算子
3.1引 言 本章的系统是以后各章研究的所有其它演算 的核心 抽象可用来定义新的函数，而代数数据类型 只涉及到所声明的一阶函数的应用 在类型化入演算的指称语义中需要考虑函数类 型的解释
3.1 引 言 • 本章的系统是以后各章研究的所有其它演算 的核心 • 抽象可用来定义新的函数，而代数数据类型 只涉及到所声明的一阶函数的应用 • 在类型化演算的指称语义中需要考虑函数类 型的解释
3.1引 言 ·入演算的历史 Church在20世纪30年代研究的定义可计算函数的 一种形式体系 Kleene在1936年证明，入可定义的所有自然数函 数正好是所有的递归函数 Turing在1937年证明，入可定义的数值函数正好 是Turing机可计算的函数 一演算一直影响着程序设计语言的研究
3.1 引 言 • 演算的历史 – Church在20世纪30年代研究的定义可计算函数的 一种形式体系 – Kleene在1936年证明，可定义的所有自然数函 数正好是所有的递归函数 – Turing在1937年证明，可定义的数值函数正好 是Turing机可计算的函数 – 演算一直影响着程序设计语言的研究
3.1引 言 ·演算和程序设计语言 20世纪50年代，无类型入演算明显影响了Lis语 言的研究 20世纪60年代认识到，程序设计语言的语义可以 通过使用拓展的，演算给出 现代的观点认为，类型化)演算引导对程序设计 语言进行更加涉及本质的分析 让类型化)演算的类型对应到程序设计语言中的 类型，就可以忠实地为类型化程序设计语言的能 力和局限性建模
3.1 引 言 • 演算和程序设计语言 – 20世纪50年代，无类型演算明显影响了Lisp语 言的研究 – 20世纪60年代认识到，程序设计语言的语义可以 通过使用拓展的演算给出 – 现代的观点认为，类型化演算引导对程序设计 语言进行更加涉及本质的分析 让类型化演算的类型对应到程序设计语言中的 类型，就可以忠实地为类型化程序设计语言的能 力和局限性建模
3.1引 言 本章的主要内容 提出使用定型公理和推理规则的上下文有关 语法 讨论类型化入演算的等式证明系统（公理语义） 和归约系统（操作语义） 讨论类型化)演算的通用模型（指称语义）及 可靠性和完备性定理 介绍PCF语言（递归函数留待下一章）及其 公理语义和操作语义
3.1 引 言 本章的主要内容 • 提出使用定型公理和推理规则的上下文有关 语法 • 讨论类型化演算的等式证明系统(公理语义) 和归约系统（操作语义） • 讨论类型化演算的通用模型（指称语义）及 可靠性和完备性定理 • 介绍PCF语言（递归函数留待下一章）及其 公理语义和操作语义