lambda演算系列搬运cgnail的blog，源blog连接为这里。

我们已经掌握了直觉逻辑（Intuitionistic Logic，IL），我们再回到lambda演算：我们已经得到了我们需要定义模型的逻辑工具。 当然，在没有更简单的事情了，对吧？

到目前为止我们讨论的都是简单的无类型lambda演算。一如丘奇首次提出LC的第一个版本。但它存在一些问题，为了解决这些问题，人们引入了「类型」（type）的概念，于是出现了简单类型lambda演算，之后出现了各种变种 —— SystemT，SystemF，Lambda立方（和时间立方没啥关系:-)）等等。最终，人们意识到无类型lambda演算实际上是类型化lambda演算的一个简单到病态的特例 —— 只有一个类型的LC。

lambda演算的语义在类型化演算中最容易理解。现在，我们来看看最简单的类型化LC，叫做「简单类型化lambda演算」（simply typed lambda calculus）；以及它如何在语义上等同于直觉逻辑。（其实上，每个种类型化LC都对应于一种IL，而且每个LC中的beta规约都对应于IL中的一步推理，这就是为什么我们需要先跑去介绍直觉逻辑，然后再回到这里。）

类型化lambda演算的主要变化是增加了一个叫做「基类型」（base types）的概念。在类型化lambda演算中，你可以使用一些由原子值构成的论域（universe）， 这些值分为不同的简单类型。基类型通常由单个的小写希腊字母命名，然而这正好是Blogger的痛处（普通html文本打不出希腊字母），我只好用大写英文字母来代替类型名称。因此，例如，我们可以有一个类型「N」，它由包含了自然数集合，也可以有一个类型「B」，对应布尔值true / false，以及一个对应于字符串类型的类「S」。

现在我们有了基本类型，接下来我们讨论函数的类型。函数将一种类型（参数的类型）的值映射到的第二种类型（返回值的类型）的值。对于一个接受类型A的输入参数，并且返回类型B的值的函数，我们将它的类型写为A -> B 。「 ->」叫做函数类型构造器（function type constructor），它是右关联的，所以 A -> B -> C 表示 A -> (B -> C)。

为了将类型应用于lambda演算，我们还要做几件事情。首先，我们需要更新语法，使我们可以包含类型信息。第二，我们需要添加一套规则，以表示哪些类型化程序是合法的。

语法部分很简单。我们添加了一个「:」符号； 冒号左侧是表达式或变量的绑定，其右侧是类型规范。 它表明，其左侧拥有其右侧指定的类型。举几个例子：

  • lambda x : N . x + 3。表示参数x 类型为N ，即自然数。这里没有指明函数的结果的类型；但我们知道，函数「+」的类型是 N -> N ，于是可以推断，函数结果的类型是N。
  • (lambda x . x + 3) : N -> N，这和上面一样，但类型声明被提了出来，所以它给出了lambda表达式作为一个整体的类型。这一次我们可以推出 x : N ，因为该函数的类型为 N -> N，这意味着该函数参数的类型为 N 。
  • lambda x : N, y : B . if y then x * x else x。这是个两个参数的函数，第一个参数类型是 N ，第二个的类型是 B 。我们可以推断返回类型为 N 。于是整个函数的类型是 N -> B -> N 。乍看之下有点奇怪；但请记住，lambda演算实际上只有单个参数；多参数函数的写法只是柯里化的简写。所以实际上这个函数是：lambda x : N . (lambda y : B . if y then x * x else x)；内层lambda的类型是 B -> N ; 外层类型是 N -> (B -> N)。

为了讨论程序是否关于类型合法（即「良类型的」(well-typed) ），我们需要引入一套类型推理规则。当使用这些规则推理一个表达式的类型时，我们称之为类型判断（type judgement）。类型推理和判断使我们能推断lambda表达式的类型；如果表达式的任一部分和类型判断结果不一致，则表达式非法。（丘奇开始研究类型化LC的动机之一是区分「原子」值和「谓词」值，他通过使用类型以确保谓词不能操作谓词，以试图避免的哥德尔式的悖论。）

我将采用一套不太正规的符号表示类型判断；标准符号太难用我目前使用的软件渲染了。常用的符号跟分数有点像；分子由我们已知为真的语句组成；分母则是我们可以从分子中推断出来的东西。 我们经常在分子中使用一个叫「上下文」（context）的概念，它包含了一组我们已知为真的语句，通常表示为一个大写的希腊字母。这里我用大写的希腊字母的名称表示。如果一个类型上下文包含声明”x : A，我会写成 CONTEXT |- x : A。对于分数形式的推理符号，我用两行表示，分子一行标有「Given: 」，分母一行标有「Infer: 」。 （正常符号用法可以访问维基百科的STLC页 。）

规则1：（类型标识） 

1
2
Given: nothing 
Infer: x : A |- x : A

最简单的规则：如果我们只知道变量的类型声明，那么我们知道这个变量是它所声明的类型。

规则2：（类型不变式） 

1
2
Given: GAMMA |- x : A, x != y 
Infer: (GAMMA + y : B) |- x : A

这是不干涉语句。 如果我们知道 x : A，那么我们可以推断出其他任何类型判断都不能改变我们对x的类型推断。

规则3：（参数到函数的推理）

1
2
Given: (GAMMA + x : A) |- y : B 
Infer: GAMMA |- (lambda x : A . y) : A -> B

这个语句使我们能够推断函数的类型：如果我们知道函数参数的类型是 A，而且该函数返回值的类型是 B ，那么我们可以推出函数的类型为 A -> B 。

最后，Rule4：（函数应用推理）

1
2
Given: GAMMA |- x : A -> B, GAMMA |- y : A 
Infer: GAMMA |- (x y) : B

如果我们知道一个函数的类型为 A -> B ，且把它应用到类型为A的值上，那么结果是类型为 B 的表达式。

规则就是这四个。如果我们有一个lambda表达式，且表达式中每一项的类型判断都保持一致，那么表达式就是良类型化的（well-typed）。如果不是，则表达式非法。

下面我们找点刺激，描述下SKI组合子的类型。这些都是不完整的类型——我用的是类型变量，而不是具体的类型。 在真正使用组合子的程序中，你可以找到实际类型来替换类型变量。 别担心，我会用一个例子来阐明这一点。

  • I组合子： (lambda x . x) : A -> A
  • K组合子： (lambda x : A . ((lambda y : B . x) : B -> A)): A -> B -> A
  • S组合子： (lambda x : A -> B-> C . (lambda y : A -> B . (lambda z : A . (x z : B -> C) (y z : B)))) : (A -> B -> C) -> (A -> B) -> C

现在，让我们来看一个简单的lambda演算表达式：lambda x y . y x。由于没有任何关于类型的声明或参数，我们无法知道确切的类型。但是，我们知道，x一定具有某种类型，我们称之为A；而且我们知道，y是一个函数，它以x作为应用的参数，所以它的参数类型为A，但它的结果类型是未知的。因此，利用类型变量，我们有 x : A, y : A -> B。我们可以通过看分析完整的具体表达式来确定A 和 B 。所以，让我们用x = 3，和y = lambda a : N. a * a 来计算类型。假设我们的类型上下文已经包含了 * 的类型为 “N -> N -> N“。

  • (lambda x y . y x) 3 (lambda a : N . a * a)
  • 3是整数，所以它的类型是： 3 : N 。
  • 根据规则4，我们可以推出出表达式 a * a 的类型是 N，其中 a : N （*的类型：N -> N -> N），因此，由规则3，lambda表达式的类型是 N - > N 。 于是，我们的表达式现在变成了：(lambda x y . y x) (3 : N) (lambda a : N . (a * a) : N) : N -> N
  • 所以 —— 现在我们知道，第一个lambda的参数 x 须是 N 类型，以及 y是 N -> N 类型 。根据规则4我们知道，应用表达式的类型 y x 一定是 N ，然后根据规则3，表达式的类型为： N -> (N -> N) -> N 。
  • 所以此处的类型 A 和 B 最后都是N。

所以，现在我们得到了一个简单的类型化lambda演算。说它是简单的类型化，是因为这里对类型的处理方式很少：建立新类型的唯一途径就是通过「 ->」 构造器。其他的类型化lambda演算包括了定义「参数化类型」（parametric types）的能力，它将类型表示为不同类型的函数。