公理语义用逻辑系统来描述程序的性质，即它是一个证明系统，可用来推导程序及其组 成部分的性质。这些性质可以是项之间的等式、给定输入下有关输出的断言、或其他性质。 现在这里给出的是一个等式公理系统，它有约束变元改名公理，还有把函数应用联系到 代换的一个公理。为了表示这些公理，需要使用记号[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指称语义 用指称方法定义语言语义的基本思想是：先确定指称物，然后给出该语言各种构造（程 44 公理语义用逻辑系统来描述程序的性质，即它是一个证明系统，可用来推导程序及其组 成部分的性质。这些性质可以是项之间的等式、给定输入下有关输出的断言、或其他性质。 现在这里给出的是一个等式公理系统，它有约束变元改名公理，还有把函数应用联系到 代换的一个公理。为了表示这些公理，需要使用记号[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 = = =