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演算的类型对应于直觉逻辑的原子类型。函数是推理规则。每个函数可以规约为一个组合子表达式；每个组合子表达式是直觉逻辑的某个基本推理规则的实例。于是，函数就成了相应逻辑里的定理的一个构造性证明。

酷吧？

（任何正常人看完会说“什么？”，但，我显然不是正常人，我是一个数学怪咖。）