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

我们已经讲过直觉逻辑(intuitionistic logic)和它的模型;从无类型的Lambda演算讲到了简单类型化Lambda演算;终于,我们可以看看Lambda演算模型了。而这正是真正有趣的地方。

先来考虑简单类型化Lambda演算中的类型。任何可以从下面语法生成的形式都是Lambda演算类型:

1
2
3
type ::= primitive | function | ( type ) 
primitive ::= A | B | C | D | ...
function ::= type -> type

这个语法中的一个陷阱是,你可以创建一个类型的表达式,而且它们是合法的类型定义,但是你无法你写出一个拥有该类型的单独的,完整的,封闭表达式。(封闭表达式是指没有自由变量的表达式。)如果一个表达式类型有类型,我们说表达式「居留」(inhabit)该类型,而该类型是一个居留类型。如果没有表达式可以居留类型,我们说这是「不可居留的」(uninhabitable) 。

那么什么是居留类型和不可居留类型之间的区别?

答案来自一种叫做「柯里-霍华德同构」(Curry-Howard isomorphism)的理论。这种理论提出,每个类型化的lambda演算,都有相应的直觉逻辑;类型表达式是可居留的当且仅当该类型是在对应逻辑上的定理。

先看类型 A -> A。现在,我们不把 -> 看作函数类型构造器,而把它视作逻辑蕴涵。A 蕴含 A 显然是直觉主义逻辑的定理。因此,类型 A -> A 是可居留的。

再来看看 A -> B 。这不是一个定理,除非在某个上下文中能证明它。作为一个函数类型,这表示一类函数,在不包括任何上下文的情况下,以A类型作为参数,并返回一个不同类型B。你没法做到这一点——必须有某个上下文提供B类型的值——为了访问这个上下文,必须存在某种允许函数访问它的上下文的方式:一个自由变量。这一点在逻辑上和lambda演算上是一样的:你需要某种上下文建立 A->B 作为一个定理(在逻辑上)或可居留的类型(在lambda演算上)。

下面就容易理解些了。如果有一个封闭LC表达式,其类型是在相应的直觉逻辑中的定理,那么,该类型的表达式就是定理的一个证明。每个Beta规约则等同于逻辑中的一个推理步骤。对应于这个lambda演算的逻辑就是它的模型。从某种意义上说,lambda演算和直觉逻辑,只是同一件事的不同反映。

有两种方式可以证明这个同构:一种是柯里当初采用的,组合子演算的方式;另一种则用到了所谓的「相继式演算」(Sequent calculus)。我会组合子证明的版本,所以下面我会快速的过一遍。以后,很可能下个礼拜,我会讲相继式演算的版本。

让我们回忆一下什么是模型。模型是一种表示演算中的每条声明(statement)在某些具体值域上都合法的方式——所以存在具体实体和演算中的实体的对应关系,凡演算中的声明都对应真正的实体的某些声明。所以我们实际上并不需要做充分的同构;我们只需要一个从演算到逻辑的同态(homomorphism)。(同构是双向的,从演算到逻辑和逻辑到演算;而同态只从演算到逻辑。)

所以我们需要做的是取任意完整的lambda演算表达式,然后将其转化为一系列合法的的直觉逻辑语句。由于直觉逻辑本身已被证明是合法的,如果我们可以把lambda演算翻译成IL,这样我们就证明了lambda演算的合法性——这意味着我们将表明,在lambda演算中的计算是合法的计算,以及lambda演算是一个完全的,合法的,有效的计算系统。

我们如何从组合子(它们只是省去了变量的lambda演算的简写)得到直觉逻辑?它实际上简单得令人难以相信。

直觉逻辑中的所有证明可以归结为一系列的步骤,其中的每一步都是使用了以下两个基本公理之一的推理:

  • A implies B implies A
  • (A implies B implies C) implies ((A implies B) implies (A implies C))

让我们用箭头重写它们,让它们看起来像一个类型:A -> B -> A ;及(A -> B -> C) -> ((A -> B) -> (A -> C))

眼熟吗?不熟的话再回头看看简单类型化lambda演算。这就是S和K组合子的类型。

接下来的建模步骤就很明显了。lambda演算的类型对应于直觉逻辑的原子类型。函数是推理规则。每个函数可以规约为一个组合子表达式;每个组合子表达式是直觉逻辑的某个基本推理规则的实例。于是,函数就成了相应逻辑里的定理的一个构造性证明。

酷吧?

(任何正常人看完会说“什么?”,但,我显然不是正常人,我是一个数学怪咖。)