很快就会熟悉这种表示法，并且可以明白，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)的简写。这两个约定可以一起使用。例如，多元函数 应用可写成 22 很快就会熟悉这种表示法，并且可以明白，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))的简写。这两个约定可以一起使用。例如，多元函数 应用可写成