第1章引言 1.1基本概念 1.1.1程序设计语言的建模 对程序设计语言进行数学分析通常是从程序设计语言的建模开始，而且模型语言的设计 一般要突出感兴趣的程序构造，忽略一些无关的细节。例如，若想分析过程调用机制，可先 设计一个简单的语言，它的主要构造是过程声明和调用，然后分析该简化语言。这种方法不 仅对分析现行的语言有用，而且有助于新语言的设计。因为实际的程序设计语言是非常庞大 和复杂的，语言的设计必须包括仔细地和分离地考虑各个子语言。从简化语言可能会得出一 些错误的印象，因此在进行程序设计语言的理论分析和把理论分析用于实际情况时，不要忘 记所做的简化及这些简化对结论的影响。 20世纪60年代就已经知道，一个复杂的程序设计语言可以被形式化为两部分：一部分 是能抓住该语言本质机制的一个非常小的核心演算一入演算(ambda calculus):另一部分是 一组导出形式，它们的行为可以通过把它们翻译成演算来理解。通过这种方式来理解语言 要深刻得多。 入演算是20世纪20年代确立的一种形式系统，它源于可计算理论，是奠定程序设计语 言中函数定义和命名约定的基本机制。在这种系统中，所有的计算都归约到函数定义和函数 应用这样的基本操作。20世纪60年代以来，入演算己广泛用于规范程序设计语言的特征、 类型系统、设计和实现的研究中。它的重要性在于它同时可以看成一种简单的程序设计语言 (用于描述计算)和看成一种数学对象（有关它的一些严格陈述可以证明）。 本书将用类型化入演算(ped lambda calculus)的框架来研究程序设计语言的各种概念。 用不同方式来扩充基本的类型化入演算，可以设计出多种模型语言，它们包含历史的、现代 的、甚至将来的语言特征。盯在类型化入演算上的一个优点是，所建立的理论具有某种程度 的“模块性”。类型化入演算的许多扩充可以组合在一起，一般来说这种组合不会出现出乎意 料的叠加影响（当然也会有例外）。例如，在分别调查了多态性和记录后，很容易定义含多 态性和记录的语言，并且指出它的很多性质。 本书研究程序设计语言的概念和特征的目的是透过表面的语法，对各种程序短语（表达 式、命令和声明等)理解到一个适当详细的程度。本章介绍一个非常简单的、以自然数和 布尔值作为基本类型的、基于类型化演算的语言，介绍该语言的语法、操作语义和它在程 序设计中的能力。该语言是后面几章介绍的可计算函数编程(Programming Computable Functions,简称PCF)语言的一个简化版本。通过这个简要介绍，读者可以对本书将要采用 的技术和方法有一个浅显的了解。 本章的主要议题如下： (1)入表示法和入演算系统概述： (2)类型和类型系统的扼要讨论： (3)基于表达式的归纳，基于证明的归纳和良基归纳。 本书以后各章也按此风格，即每一章有一节导言，导言中包含该章的主要议题。 1.1.22表示法 在描述、分析和实现程序设计语言时，入演算己被证明是非常有用的。稍加练习，读者
1 第 1 章 引 言 1.1 基本概念 1.1.1 程序设计语言的建模 对程序设计语言进行数学分析通常是从程序设计语言的建模开始，而且模型语言的设计 一般要突出感兴趣的程序构造，忽略一些无关的细节。例如，若想分析过程调用机制，可先 设计一个简单的语言，它的主要构造是过程声明和调用，然后分析该简化语言。这种方法不 仅对分析现行的语言有用，而且有助于新语言的设计。因为实际的程序设计语言是非常庞大 和复杂的，语言的设计必须包括仔细地和分离地考虑各个子语言。从简化语言可能会得出一 些错误的印象，因此在进行程序设计语言的理论分析和把理论分析用于实际情况时，不要忘 记所做的简化及这些简化对结论的影响。 20 世纪 60 年代就已经知道，一个复杂的程序设计语言可以被形式化为两部分：一部分 是能抓住该语言本质机制的一个非常小的核心演算—λ演算（lambda calculus）；另一部分是 一组导出形式，它们的行为可以通过把它们翻译成λ演算来理解。通过这种方式来理解语言 要深刻得多。 λ演算是 20 世纪 20 年代确立的一种形式系统，它源于可计算理论，是奠定程序设计语 言中函数定义和命名约定的基本机制。在这种系统中，所有的计算都归约到函数定义和函数 应用这样的基本操作。20 世纪 60 年代以来，λ演算已广泛用于规范程序设计语言的特征、 类型系统、设计和实现的研究中。它的重要性在于它同时可以看成一种简单的程序设计语言 （用于描述计算）和看成一种数学对象（有关它的一些严格陈述可以证明）。 本书将用类型化λ演算（typed lambda calculus）的框架来研究程序设计语言的各种概念。 用不同方式来扩充基本的类型化λ演算，可以设计出多种模型语言，它们包含历史的、现代 的、甚至将来的语言特征。盯在类型化λ演算上的一个优点是，所建立的理论具有某种程度 的“模块性”。类型化λ演算的许多扩充可以组合在一起，一般来说这种组合不会出现出乎意 料的叠加影响（当然也会有例外）。例如，在分别调查了多态性和记录后，很容易定义含多 态性和记录的语言，并且指出它的很多性质。 本书研究程序设计语言的概念和特征的目的是透过表面的语法，对各种程序短语（表达 式、命令和声明等）理解到一个适当详细的程度。 本章介绍一个非常简单的、以自然数和 布尔值作为基本类型的、基于类型化λ演算的语言，介绍该语言的语法、操作语义和它在程 序设计中的能力。该语言是后面几章介绍的可计算函数编程（Programming Computable Functions，简称 PCF）语言的一个简化版本。通过这个简要介绍，读者可以对本书将要采用 的技术和方法有一个浅显的了解。 本章的主要议题如下： （1）λ表示法和λ演算系统概述； （2）类型和类型系统的扼要讨论； （3）基于表达式的归纳，基于证明的归纳和良基归纳。 本书以后各章也按此风格，即每一章有一节导言，导言中包含该章的主要议题。 1.1.2 λ表示法 在描述、分析和实现程序设计语言时，λ演算已被证明是非常有用的。稍加练习，读者
很快就会熟悉这种表示法，并且可以明白，C、Pascal和Ada的程序短语都是在入表达式的 基础上做了语法美化。这就使得本书描述的理论更加有用，而且使得程序设计语言的多样性 更容易理解。语言PCF将直接使用表示法，就像Lisp语言那样：所不同的是，PCF没有 表和原子，但它有相对严格的定型原则。 表示法的主要特征是入抽象和入应用，前者用于定义函数，后者用于使用所定义的函数。 用入表示法写出的表达式叫做表达式或项。表示法既可用于类型化入演算，也可用于无类 型入演算。 在类型化入演算中，函数的论域(domain)由给出形式参数的类型来指定。如果变元x 的类型是o,M是基于这个假定的良类型(well typed)表达式，那么r:o.M定义一个函数， 它把。类型的任意x映射到由M给定的值。一个简单的入抽象的例子是： 入x:nal.x 它表示自然数上的恒等函数。记号x:nal说明该函数的论域是nal,即自然数类型。在该表 达式中，点后面的部分是函数体。因为该例的函数体也是x,因此该函数的值域也是n1。 每一种形式的类型化入演算，都有精确的规则来说明：在变量类型给定的情况下，什么 样的表达式是良类型的，以及良类型表达式的类型。例如，表达式x:na1.x+e不是良类 型的，因为true和自然数相加是没有意义的。 用程序设计语言定义恒等函数，最熟悉的形式可能是 Id(x nat)=x 但是这种形式要求为每个函数起一个名字，而表示法给出了无须给函数命名的一种简洁方 式。例如， x natx+1 定义了自然数上的后继函数。 x nat.10 是自然数上的一个常函数，该函数的值恒为10。 在)抽象中，入是一个约束算子，这意味着在)项x:oM中，变元x只是一个占位符，就 像在谓词演算公式 x:A.中 中的变元x那样。因此可以重新命名入约束变元而不改变表达式的含义，只要所选择的新变 元与其他已经使用的变元没有名字冲突便可以了。仅仅约束变元名字不同的项称为等价 的。如果M和N是a等价的，可以写成M=aN。如果x出现在表达式M中，并且它出现在 形式为x:oN的子表达式中，那么称x的这个出现是约束的(bound),否则是自由的。注意， 在一个表达式中，x可能既有约束出现也有自由出现，例如表达式(y:nal→nal.x)x:na1.x) 中的x(这种两个项并置的含义在下面解释)。不含自由变元的表达式称为闭表达式。 在)表示法中，用项的并置来表示函数应用，并且用括号来说明运算对象的结合。例如， 把恒等函数应用于5可写成 (hx natx)5 这个函数应用的结果是5，即 (x nat.x)5=5 下一节将看到，有几种不同的方式可用来计算，表达式的值或证明表达式之间的等式。 入表示法有两个约定，以省略入表达式中的大量括号。第一个约定是函数应用是左结合 的，即MNP应看成(MW)P。第二个约定是每个)的约束范围尽可能地大，一直到表达式的结 束或碰到不能配对的右括号为止。例如，x:o.MN解释为x:o.(MW),而不是(x:o.MN。同 样地，x:oy:x.MN是x:o.(yx(M)的简写。这两个约定可以一起使用。例如，多元函数 应用可写成 2
2 很快就会熟悉这种表示法，并且可以明白，C、Pascal 和 Ada 的程序短语都是在λ表达式的 基础上做了语法美化。这就使得本书描述的理论更加有用，而且使得程序设计语言的多样性 更容易理解。语言 PCF 将直接使用λ表示法，就像 Lisp 语言那样；所不同的是，PCF 没有 表和原子，但它有相对严格的定型原则。 λ表示法的主要特征是λ抽象和λ应用，前者用于定义函数，后者用于使用所定义的函数。 用λ表示法写出的表达式叫做λ表达式或λ项。λ表示法既可用于类型化λ演算，也可用于无类 型λ演算。 在类型化λ演算中，函数的论域（domain）由给出形式参数的类型来指定。如果变元 x 的类型是σ，M 是基于这个假定的良类型（well typed）表达式，那么λx:σ.M 定义一个函数， 它把σ 类型的任意 x 映射到由 M 给定的值。一个简单的λ抽象的例子是： λx : nat.x 它表示自然数上的恒等函数。记号 x : nat 说明该函数的论域是 nat，即自然数类型。在该表 达式中，点后面的部分是函数体。因为该例的函数体也是 x，因此该函数的值域也是 nat。 每一种形式的类型化λ演算，都有精确的规则来说明：在变量类型给定的情况下，什么 样的表达式是良类型的，以及良类型表达式的类型。例如，表达式λx : nat.x + true 不是良类 型的，因为 true 和自然数相加是没有意义的。 用程序设计语言定义恒等函数，最熟悉的形式可能是 Id ( x : nat ) = x 但是这种形式要求为每个函数起一个名字，而λ表示法给出了无须给函数命名的一种简洁方 式。例如， λx : nat.x + 1 定义了自然数上的后继函数。 λx : nat.10 是自然数上的一个常函数，该函数的值恒为 10。 在λ抽象中，λ是一个约束算子，这意味着在λ项λx:σ.M 中，变元 x 只是一个占位符，就 像在谓词演算公式 ∀x : A.φ 中的变元 x 那样。因此可以重新命名λ约束变元而不改变表达式的含义，只要所选择的新变 元与其他已经使用的变元没有名字冲突便可以了。仅仅约束变元名字不同的项称为α等价 的。如果 M 和 N 是α等价的，可以写成 M =α N。如果 x 出现在表达式 M 中，并且它出现在 形式为λx:σ.N 的子表达式中，那么称 x 的这个出现是约束的（bound），否则是自由的。注意， 在一个表达式中，x 可能既有约束出现也有自由出现，例如表达式(λy : nat → nat.x)(λx : nat.x) 中的 x（这种两个项并置的含义在下面解释）。不含自由变元的表达式称为闭表达式。 在λ表示法中，用项的并置来表示函数应用，并且用括号来说明运算对象的结合。例如， 把恒等函数应用于 5 可写成 (λx : nat.x) 5 这个函数应用的结果是 5，即 (λx : nat.x) 5 = 5 下一节将看到，有几种不同的方式可用来计算λ表达式的值或证明λ表达式之间的等式。 λ表示法有两个约定，以省略λ表达式中的大量括号。第一个约定是函数应用是左结合 的，即 MNP 应看成(MN)P。第二个约定是每个λ的约束范围尽可能地大，一直到表达式的结 束或碰到不能配对的右括号为止。例如，λx:σ.MN 解释为λx:σ.(MN)，而不是(λx:σ.M)N。同 样地，λx:σ.λy:τ. MN 是λx:σ.(λy:τ.(MN))的简写。这两个约定可以一起使用。例如，多元函数 应用可写成
(Ax:o.Ay:t.):p.M)NPO 它是 (((x:(y:(P.M)))N)P)O 的简写。 1.13记号和约定 本书用到的数学基础主要是集合论的知识，包括关系和函数，这些大家都己熟悉，本书 不再重复。本书用到的各种归纳法另用一节专门介绍。 本书使用几种形式的相等符号，这些符号及它们的含义如下： =两个表达式有相同的值： =除了约束变元的名字可能不同以外，两个表达式语法上等同： 会用M兰N来表示符号或表达式M被定义成等于N: :=在文法中用来表示表达式的可能形式： 三表示（集合、代数等的）同构。 本书使用的逻辑符号如下： 廿全称量词，公式x.中可以读成“对所有的x,中为真” 3存在量词，公式3x.中可以读成“存在一个x使得b为真”： 入合取，公式中AΨ可以读成“中合取Ψ”： 析取，公式中Vw可以读成“中析取Ψ”： 一否定，公式中可以读成“非中”： →蕴涵，公式中→Ψ可以读成“中蕴涵Ψ”（不使用→作为蕴涵，因为→用于类型表 达式，并用于表达式的归约（求值）)： f当且仅当。 本书中使用的集合运算符号如下： ∈属于运算： U 并集运算： O交集运算： c子集运算： ×笛卡儿积运算。 1.2等式、归约和语义 历史上，入表示法是入演算的一部分，入演算是关于)表达式的一个推理系统。除了语法 外，这个形式系统有三个主要部分。按照现代程序设计语言的术语，它们分别叫做公理语义、 操作语义和指称语义。逻辑学家可能把前二者叫做证明系统，而把第三者称为一种模型。公 理语义是推导表达式之间等式的一个形式系统。操作语义是一种将等式确定为有向规则的推 理，叫做归约。按计算机科学的术语，归约可看成符号求值的一种形式。指称语义或模型， 本质上类似于其他逻辑系统（如等式逻辑或一阶逻辑）的模型。一个模型是一组集合，每种 类型一个集合，这个集合就是对应类型的解释域，并且每个良类型的表达式都可以解释为相 应集合中的一个元素。 本节对本书常用的语义方法做一个概述，让读者有一个粗浅的认识。 1.2.1公理语义 3
3 (λx:σ.λy:τ.λz:ρ.M)NPQ 它是 (((λx:σ.(λy:τ.(λz:ρ.M)))N)P)Q 的简写。 1.1.3 记号和约定 本书用到的数学基础主要是集合论的知识，包括关系和函数，这些大家都已熟悉，本书 不再重复。本书用到的各种归纳法另用一节专门介绍。 本书使用几种形式的相等符号，这些符号及它们的含义如下： = 两个表达式有相同的值； ≡ 除了约束变元的名字可能不同以外，两个表达式语法上等同； 用 M N 来表示符号或表达式 M 被定义成等于 N； ::= 在文法中用来表示表达式的可能形式； ≅ 表示（集合、代数等的）同构。 本书使用的逻辑符号如下： ∀ 全称量词，公式∀x.φ可以读成“对所有的 x，φ为真”； ∃ 存在量词，公式∃x.φ可以读成“存在一个 x 使得φ为真”； ∧ 合取，公式φ ∧ ψ 可以读成“φ 合取ψ”； ∨ 析取，公式φ ∨ ψ 可以读成“φ 析取ψ”； ¬ 否定，公式¬φ 可以读成“非φ”； ⇒ 蕴涵，公式φ ⇒ ψ 可以读成“φ 蕴涵ψ”（不使用→作为蕴涵，因为→用于类型表 达式，并用于表达式的归约（求值））； iff 当且仅当。 本书中使用的集合运算符号如下： ∈ 属于运算； ∪ 并集运算； ∩ 交集运算； ⊆ 子集运算； × 笛卡儿积运算。 1.2 等式、归约和语义 历史上，λ表示法是λ演算的一部分，λ演算是关于λ表达式的一个推理系统。除了语法 外，这个形式系统有三个主要部分。按照现代程序设计语言的术语，它们分别叫做公理语义、 操作语义和指称语义。逻辑学家可能把前二者叫做证明系统，而把第三者称为一种模型。公 理语义是推导表达式之间等式的一个形式系统。操作语义是一种将等式确定为有向规则的推 理，叫做归约。按计算机科学的术语，归约可看成符号求值的一种形式。指称语义或模型， 本质上类似于其他逻辑系统（如等式逻辑或一阶逻辑）的模型。一个模型是一组集合，每种 类型一个集合，这个集合就是对应类型的解释域，并且每个良类型的表达式都可以解释为相 应集合中的一个元素。 本节对本书常用的语义方法做一个概述，让读者有一个粗浅的认识。 1.2.1 公理语义
公理语义用逻辑系统来描述程序的性质，即它是一个证明系统，可用来推导程序及其组 成部分的性质。这些性质可以是项之间的等式、给定输入下有关输出的断言、或其他性质。 现在这里给出的是一个等式公理系统，它有约束变元改名公理，还有把函数应用联系到 代换的一个公理。为了表示这些公理，需要使用记号[Nx]M,它表示M中的自由变元x用 表达式N代换的结果。代换时需要注意的是，N中的自由变元不能代换到M中后成为约束 变元。把M中的自由变元x用N代换的最简单办法是，首先将M中所有的约束变元改名， 使得它们和N中的自由变元都有区别，然后再将x的自由出现用N代替。第3章将给出更 详细的定义。使用代换，约束变元改名公理可写成 x:o.M=y:o.Dy/x]M,M中无自由出现的y (a) 例如，入x:ox=入Gy。 因为项x:o.M定义了一个函数，因此可以通过用N代替x来计算该函数应用于N的结 果。例如，将函数2x:nalx+4应用于4的结果是 (x:nat.x+4)4=[4/x](x+4)=4+4 更一般而言，等式公理 (Ax:G.M)N [NIx]M (B)eg 被称为B等价公理。本质上，B等价是说，计算函数应用就是在函数体中用实在变元代替 形式变元。除了这些公理和个别其他公理外，等式系统还包含自反性、对称性、传递性和同 余性规则。同余性规则是说，相等的函数应用于相等的变元产生相等的结果，可以写成 M1=M2,W1=W2 MINI=M2N2 当然，为了完全精确，还应说明它们的类型，以保证每个项都有意义。和其他逻辑证明系统 一样，类型化演算的等式证明规则允许推导任何一组等式前提的逻辑推论。 1.2.2操作语义 语言的操作语义可用不同的方式给出，一种接近实际实现的方式是定义一台抽象机， 它是一种理论上的计算机，然后通过一系列的机器状态变换来计算程序。这种操作语义最 实际的表示就是语言的解释器。操作语义比较抽象的表示是演绎出最终结果的证明系统， 或者说是通过一系列步骤变换一个表达式的证明系统。本书主要使用第二种形式的操作语 义，即定义完整的、一步一步求值的证明系统。 先前所列等式公理的自左向右的单向形式给出了演算的归约规则。直观上讲，基本归 约规则描述了单步符号计算，它们可以反复用于表达式的求值，直至得到表达式的最简形式， 或因无最简形式而计算不终止。符号计算过程给出了入演算的计算特征。归约是非对称的， 箭头→通常用于表示一步归约，双箭头→用于表示任意步（包括零步）归约。 最核心的归约规则是（的单向形式，叫做B归约，写成 (x:o.MN→B[N/x]M (B)red 例如， (入x:nat.x+4)4>4+4 因为在代换时约束变元可能需要改名，因此归约是定义在α等价上的。即B归约的结果 依赖于新约束变元的选择，它不是唯一确定的。但是归约产生的任何两个项仅在约束变元的 名字上有区别，因此它们是a等价的。 除了()规则外，还有一些其他的归约规则。完整的归约系统及其性质在后面章节讨论。 1.2.3指称语义 用指称方法定义语言语义的基本思想是：先确定指称物，然后给出该语言各种构造（程 4
4 公理语义用逻辑系统来描述程序的性质，即它是一个证明系统，可用来推导程序及其组 成部分的性质。这些性质可以是项之间的等式、给定输入下有关输出的断言、或其他性质。 现在这里给出的是一个等式公理系统，它有约束变元改名公理，还有把函数应用联系到 代换的一个公理。为了表示这些公理，需要使用记号[N/x]M，它表示 M 中的自由变元 x 用 表达式 N 代换的结果。代换时需要注意的是，N 中的自由变元不能代换到 M 中后成为约束 变元。把 M 中的自由变元 x 用 N 代换的最简单办法是，首先将 M 中所有的约束变元改名， 使得它们和 N 中的自由变元都有区别，然后再将 x 的自由出现用 N 代替。第 3 章将给出更 详细的定义。使用代换，约束变元改名公理可写成 λx:σ.M = λy:σ.[y/x]M， M 中无自由出现的 y (α) 例如，λx:σ.x = λy:σ.y。 因为项λx:σ.M 定义了一个函数，因此可以通过用 N 代替 x 来计算该函数应用于 N 的结 果。例如，将函数λx:nat.x+4 应用于 4 的结果是 (λx:nat.x+4) 4 = [4/x](x+4) = 4 + 4 更一般而言，等式公理 (λx:σ.M)N = [N/x]M (β)eq 被称为β 等价公理。本质上，β 等价是说，计算函数应用就是在函数体中用实在变元代替 形式变元。除了这些公理和个别其他公理外，等式系统还包含自反性、对称性、传递性和同 余性规则。同余性规则是说，相等的函数应用于相等的变元产生相等的结果，可以写成 当然，为了完全精确，还应说明它们的类型，以保证每个项都有意义。和其他逻辑证明系统 一样，类型化λ演算的等式证明规则允许推导任何一组等式前提的逻辑推论。 1.2.2 操作语义 语言的操作语义可用不同的方式给出，一种接近实际实现的方式是定义一台抽象机， 它是一种理论上的计算机，然后通过一系列的机器状态变换来计算程序。这种操作语义最 实际的表示就是语言的解释器。操作语义比较抽象的表示是演绎出最终结果的证明系统， 或者说是通过一系列步骤变换一个表达式的证明系统。本书主要使用第二种形式的操作语 义，即定义完整的、一步一步求值的证明系统。 先前所列等式公理的自左向右的单向形式给出了λ演算的归约规则。直观上讲，基本归 约规则描述了单步符号计算，它们可以反复用于表达式的求值，直至得到表达式的最简形式， 或因无最简形式而计算不终止。符号计算过程给出了λ演算的计算特征。归约是非对称的， 箭头→通常用于表示一步归约，双箭头→→用于表示任意步（包括零步）归约。 最核心的归约规则是(β)eq 的单向形式，叫做β 归约，写成 (λx:σ.M)N →β [N/x]M (β)red 例如， (λx:nat.x+4) 4 → 4 + 4 因为在代换时约束变元可能需要改名，因此归约是定义在α等价上的。即β 归约的结果 依赖于新约束变元的选择，它不是唯一确定的。但是归约产生的任何两个项仅在约束变元的 名字上有区别，因此它们是α等价的。 除了(β)eq 规则外，还有一些其他的归约规则。完整的归约系统及其性质在后面章节讨论。 1.2.3 指称语义 用指称方法定义语言语义的基本思想是：先确定指称物，然后给出该语言各种构造（程 1 1 2 2 1 2 1 2 M N M N M M ,N N = = =
序、语句、表达式等)到相应指称物的语义映射，这个映射要满足： (1)各语言构造的每个实例都有对应的指称： (2)复合语言构造的实例的指称只依赖于它的子构造的指称。 在类型化入演算的指称语义中，每个类型表达式对应到一个集合，称为该类型的值集。 类型o的项解释为其值集上的一个元素。类型o→x的值集是函数集合，因此项x:σ.M解 释为一个数学函数。纯类型化入演算的语义是简单的，而它的各种扩充的语义可能会比较复 杂。具有挑战性的特征有函数的递归定义、类型的递归定义和多态函数等。除了不讨论递归 定义的类型的指称语义外，其他两个概念的指称语义在后面都会详细讨论。 对于熟悉无类型入演算的读者来说，值得一提的是，无类型入演算可以从类型化入演算中 派生出来。事实上，考虑无类型入演算的语义的最自然方式之一是从类型化入演算的语义开 始。基于这个原因，类型化演算被看成是更加基本的系统，更适于作为研究的起点。 1.3类型和类型系统 类型论是为避免集合论悖论而建立起来的数学理论，主要研究集合的分层、分类方法。 在程序设计语言理论中，类型论是指类型系统的设计、分析和研究。在任何类型系统中，类 型提供了全体所有可能值的一种分类：一个类型是一群有某些公共性质的值。对于不同的类 型系统，类型的多少和值所属的类型可能不同。 本节扼要介绍类型系统的有关概念和应用。 1.3.1类型和类型系统 一个程序变量在程序执行期间的值可以设想为有一个范围，这个范围的一个界叫做该变 量的类型。例如，类型b0ol的变量x在程序每次运行时的值只能是该类型的值。如果x有 类型bool,那么布尔表达式no1(x)在程序每次运行时都有意义。变量都被给定（非平凡）类 型的语言叫做类型化的语言(yped language)。 语言若不限制变量值的范围，则被称作无类型语言(ntyped language),它们没有类型， 或者说仅有一个包含所有值的泛类型。在这些语言中，一个运算可以应用到任意的运算对象， 其结果可能是一个有意义的值、一个错误、一个异常或一个语言未作规定的结果。 类型化语言的类型系统是语言的一个组成部分，它始终监视着程序中变量的类型，通常 还包括所有表达式的类型。一个类型系统主要由一组定型规则(typing rule)构成，这组规 则用来给各种语言构造指派类型。 在计算机科学中，类型系统的研究有两个分支：比较实际的一支是类型系统在程序设计 语言中的应用：比较抽象的一支关心“纯类型化入演算”和各种逻辑之间的对应关系。本书 主要研究前面一个分支。 为语言设计类型系统的目的是什么？简单讲，类型系统的根本目的是用来保证程序运行 时不会出现不良行为，例如将整数和布尔值相加。只有那些顺从类型系统的程序才被认为是 类型化语言的合法程序，其他的程序在它们运行前都应该被抛弃。 非形式地说，当用一种程序设计语言所能表示的所有合法程序在运行时都不会出现不良 行为时，就称该语言是安全语言。若语言的类型系统能保证语言的安全性，则又称该语言是 类型可靠的(type sound)或类型安全的。显然，希望通过适当的分析和证明来对语言的类 型安全性做出准确的回答。这种分析和证明将基于语言的类型系统，因此类型系统的研究也 需要形式方法，这是本书的一个重要内容。 5
5 序、语句、表达式等）到相应指称物的语义映射，这个映射要满足： （1）各语言构造的每个实例都有对应的指称； （2）复合语言构造的实例的指称只依赖于它的子构造的指称。 在类型化λ演算的指称语义中，每个类型表达式对应到一个集合，称为该类型的值集。 类型σ 的项解释为其值集上的一个元素。类型σ →τ 的值集是函数集合，因此项λx:σ.M 解 释为一个数学函数。纯类型化λ演算的语义是简单的，而它的各种扩充的语义可能会比较复 杂。具有挑战性的特征有函数的递归定义、类型的递归定义和多态函数等。除了不讨论递归 定义的类型的指称语义外，其他两个概念的指称语义在后面都会详细讨论。 对于熟悉无类型λ演算的读者来说，值得一提的是，无类型λ演算可以从类型化λ演算中 派生出来。事实上，考虑无类型λ演算的语义的最自然方式之一是从类型化λ演算的语义开 始。基于这个原因，类型化λ演算被看成是更加基本的系统，更适于作为研究的起点。 1.3 类型和类型系统 类型论是为避免集合论悖论而建立起来的数学理论，主要研究集合的分层、分类方法。 在程序设计语言理论中，类型论是指类型系统的设计、分析和研究。在任何类型系统中，类 型提供了全体所有可能值的一种分类：一个类型是一群有某些公共性质的值。对于不同的类 型系统，类型的多少和值所属的类型可能不同。 本节扼要介绍类型系统的有关概念和应用。 1.3.1 类型和类型系统 一个程序变量在程序执行期间的值可以设想为有一个范围，这个范围的一个界叫做该变 量的类型。例如，类型 bool 的变量 x 在程序每次运行时的值只能是该类型的值。如果 x 有 类型 bool，那么布尔表达式 not (x)在程序每次运行时都有意义。变量都被给定（非平凡）类 型的语言叫做类型化的语言（typed language）。 语言若不限制变量值的范围，则被称作无类型语言（untyped language），它们没有类型， 或者说仅有一个包含所有值的泛类型。在这些语言中，一个运算可以应用到任意的运算对象， 其结果可能是一个有意义的值、一个错误、一个异常或一个语言未作规定的结果。 类型化语言的类型系统是语言的一个组成部分，它始终监视着程序中变量的类型，通常 还包括所有表达式的类型。一个类型系统主要由一组定型规则（typing rule）构成，这组规 则用来给各种语言构造指派类型。 在计算机科学中，类型系统的研究有两个分支：比较实际的一支是类型系统在程序设计 语言中的应用；比较抽象的一支关心“纯类型化λ演算”和各种逻辑之间的对应关系。本书 主要研究前面一个分支。 为语言设计类型系统的目的是什么？简单讲，类型系统的根本目的是用来保证程序运行 时不会出现不良行为，例如将整数和布尔值相加。只有那些顺从类型系统的程序才被认为是 类型化语言的合法程序，其他的程序在它们运行前都应该被抛弃。 非形式地说，当用一种程序设计语言所能表示的所有合法程序在运行时都不会出现不良 行为时，就称该语言是安全语言。若语言的类型系统能保证语言的安全性，则又称该语言是 类型可靠的（type sound）或类型安全的。显然，希望通过适当的分析和证明来对语言的类 型安全性做出准确的回答。这种分析和证明将基于语言的类型系统，因此类型系统的研究也 需要形式方法，这是本书的一个重要内容