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。我们可以通过看分析完整的具体表达式来确定AB 。所以,让我们用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 类型,以及 yN -> N 类型 。根据规则4我们知道,应用表达式的类型 y x 一定是 N ,然后根据规则3,表达式的类型为: N -> (N -> N) -> N
  • 所以此处的类型 A 和 B 最后都是N

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