第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语言（递归函数留待下一章）及其 公理语义和操作语义
3.2类型和项 3.2.1类型的语法 ·简单类型化)演算的类型表达式文法 o:=b null|unit|o+oo×oo-→o b:类型常量 nnll:初始类型 unit:终结类型 和、积与函数类型 类型表达式中不含类型变量 用入、入×，→和入+，×，来命名所讨论的演算
3.2 类型和项 3.2.1 类型的语法 • 简单类型化演算的类型表达式文法 ::= b | null | unit | + | | → b：类型常量 null：初始类型 unit：终结类型 和、积与函数类型 类型表达式中不含类型变量 • 用→ 、 →和 +→来命名所讨论的演算
3.2类型和项 3.2.2上下文有关语法 不存在上下文无关文法，它正好产生)→良类 型的项 ·用一种基于逻辑的形式系统来定义类型语言 一用公理和推理规则来同时定义表达式及其类型 -定型公理C:无 推理规则 M1:61...Mk:Ok T1 M:01...Tk MKOK N:t T N:t 定型断言工 M:t,其中T=1:O,,xx:O}
3.2 类型和项 3.2.2 上下文有关语法 • 不存在上下文无关文法，它正好产生→良类 型的项 • 用一种基于逻辑的形式系统来定义类型语言 – 用公理和推理规则来同时定义表达式及其类型 – 定型公理 c : – 推理规则 – 定型断言 M : , 其中 = {x1 :1 , …, xk :k } M1 :1 … Mk :k N : 1 M1 :1 … k Mk :k N :
3.2类型和项 3.2.3入→项的语法 ,一个入基调Σ=〈B,C)包含 一个集合B,其元素叫做基本类型或类型常量 形式为c:o的项常量集合C,其中σ是B上的入→类 型表达式 多类代数的基调Σ=S,F万)的基调很容易变换 成入基调Σ=〈B,C) -令B就等于S 若F有f:S1×.×Sk→S,则在C中包含项常量 f:S1→…Sk→S
3.2 类型和项 3.2.3 →项的语法 • 一个→基调 = B, C包含 – 一个集合B，其元素叫做基本类型或类型常量 – 形式为c的项常量集合C，其中是B上的→类 型表达式 • 多类代数的基调 = S, F 的基调很容易变换 成→基调 = B, C – 令B就等于S – 若F有f : s1 … sk → s，则在C中包含项常量 f : s1 → … → sk → s
3.2类型和项 项的语法及类型按如下方式描述 -首先用BNF定义类型表达式的语法(3.2.1节) 然后用定型公理和定型规则同时定义Σ上的入→项 和它们的类型（良形的项就是良类型的项） 良形(wel-formed)和良类型(well-yped) 良形的项x+3在x是整型时才是良类型的 ·定型公理 C: 一X:O x:O
3.2 类型和项 • 项的语法及类型按如下方式描述 – 首先用BNF定义类型表达式的语法（3.2.1节） – 然后用定型公理和定型规则同时定义上的→项 和它们的类型（良形的项就是良类型的项） – 良形（well-formed）和良类型（well-typed） 良形的项x + 3在x是整型时才是良类型的 • 定型公理 – c (cst) – x x (var)
3.2类型和项 ·定型规则 M:o (add var) T,x:t M:o T,x:o M:t (>Intro） (入x:o.)：σ→E TM:o→TN:o (→Elim) T MN:t ·定型断言的证明叫做定型推导
3.2 类型和项 • 定型规则 (add var) (→ Intro) (→ Elim) • 定型断言的证明叫做定型推导 M : , x : M : M : → N : MN : , x : M : ( x : . M) : →
