组合子逻辑

组合子逻辑是Moses Schönfinkel和哈斯凱爾·加里介入的一种符号系统，用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。

数学中的组合子逻辑

组合子逻辑意图作为简单的元逻辑，它能澄清在逻辑符号中的量化变量的意义，并真正的消除对它们的需要。消除量化变量的另一种方式是蒯因的谓词函子。尽管多数组合子逻辑系统超出了一阶逻辑的表达能力，蒯因的谓词函子的表达能力等价于一阶逻辑（Quine [1960] 1966）。

组合子逻辑的最初发明者Schönfinkel，在1929年之后基本停止了发表著作。Curry在1927年[1]晚期于哥廷根大学读博士的时候重新发现了组合子。在1930年代后期，邱奇和他的学生在普林斯顿发明了一个竞争的函数抽象的形式化，就是lambda演算，它比组合子逻辑更加流行。这些历史上的意外事件的结果是直到在1960年代和1970年代理论计算机科学开始感兴趣于组合子逻辑，关于这个主题的几乎所有工作都是Haskell Curry和他的学生们，或比利时的Robert Feys做的。Curry和Feys (1958)和Curry等人（1972） 纵览了组合子逻辑的早期历史。组合子逻辑和lambda演算的更现代的平行处置参见Barendregt（1984），他还评论了Dana Scott在1960年代和1970年代为组合子逻辑设计的模型。

计算中的组合子逻辑

在计算机科学中，组合子逻辑被用做可计算性理论中计算和证明论的简化模型。这个理论尽管简单，但捕获了计算本质的很多根本特征。

组合子逻辑可以被看作是lambda演算的变体，它把lambda表达式（用来允许函数抽象）替代为组合子的有限集合，它们是不包含自由变量的原始函数。很容易把lambda表达式变换成组合子表达式，并且因为组合子归约比lambda归约要简单，它已经被用做用软件中的某些非严格的函数式编程语言和硬件的图归约机的实现基础。

还可以用很多其他方式来看待它，很多早年的论文证明了各种组合子到各种逻辑公理的等价性[Hindley and Meredith, 1990]。

lambda演算概要
主条目：lambda演算

lambda演算关注的是叫做lambda-项的对象，它们是下列形式之一的符号串：

  • v
  • λv.E1
  • (E1 E2)

这里的v是变量名字，它取自预定义变量名字的无限集合，而E1和E2是lambda-项。形如λv.E1的项叫做抽象。变量v叫做抽象的形式参数，而E1是抽象的“主体”。

项λv.E1表示一个函数，它应用于一个参数，绑定形式参数v到这个参数，接着计算E1的结果值---就是说，它返回E1，带有v的所有出现被参数所替代。

形如 (E1 E2)的项叫做应用。应用建模函数调用或执行：调用E1所代表的函数，带有E2作为它的参数，并计算结果。如果E1（有时叫做applicand）是一个抽象，则这个项可以被归约：参数E2可以被代换如E1的主体中E1的形式参数的位置上，而结果是一个新的lambda项，它等价于旧的。如果一个lambda项不包含形如 (λv.E1 E2)的子项，则它不能被归约，而被称为是范式。

表达式E[v := a]表示接受项E并把v的所有自由出现替代为a的结果。所以我们写

(λv.E a) => E[v := a]

出于方便，我们用 (a b c d ... z)来简写 (...(((a b) c) d) ... z)。（就是说，应用是左结合的）。

归约的这个定义的动机是捕获所有数学函数的本质行为。例如，考虑计算数的平方的函数。我们写

x的平方是x*x

（使用"*"来指示乘法）。这里的x是这个函数的形式参数。要计算一个特定参数的平方，比如3，我们把它插入到这个定义中形式参数的位置上：

3的平方是3*3

要求值表达式3*3的结果，我们必须诉诸我们关于乘法和数3的知识。因为任何计算都简单的就是在适当基本参数上的适当函数的计算的复合，这个简单代换原理足够捕获计算的本质机制。此外，在lambda演算中，概念比如3和*，不需要任何额外定义基本运算符或常量就可以表示出来。有可能在lambda表达式中确定一些项，在做适合的解释的时候，它们的表现得如同数3和乘法运算符。

已知lambda演算在计算性上等价于关于计算的任何其他似乎为真的模型（包括图灵机）的能力；就是说，可以在任何这些模型中完成的计算都可以用lambda演算表达，反之亦然。根据邱奇-图灵论题，这些模型都可以表达任何可能的计算。

可能令人惊奇，只使用基于对项中变量的简单文字代换的函数抽象和应用的简单概念，lambda演算可以表达任何可想象出来的计算。但是更加不寻常的是甚至抽象都是不需要的。组合子逻辑就是等价于lambda演算的计算模型，它不需要抽象。

组合子演算

因为在lambda演算中抽象是制造函数的唯一方式，在组合子演算中必须有某种东西替代它。不再使用抽象，组合子演算提供了有限的基本函数的集合，其他函数可以用它们来构建。

组合子项

组合子项是下列形式之一：

  • v
  • P
  • (E1 E2)

这里的v是一个变量，P是基本函数之一，而E1和E2是组合子项。基本函数自身是组合子，或不包含自由变量的函数。

组合子的例子

组合子的最简单的例子是I，恒等组合子，定义为

(I x) = x

对于所有的项x。另一个简单的组合子是K，制造常量函数：(K x)是对于任何参数都返回x的函数，所以我们定义

((K x) y) = x

对于所有的项x和y。或者，服从同lambda演算中多重应用同样的约定，

(K x y) = x

第三个组合子是S，它是应用的一般化版本：

(S x y z) = (x z (y z))

S首先将z分别代换到x和y，然后再将两个结果进行应用操作。

给出S和K，I自身就不是必须的了，因为可以建造自其他两个：

((S K K) x)
=(S K K x)
= (K x (K x))
= x

对于任何的项x。注意尽管((S K K)x) = (I x)对于任何x，(S K K)自身不等于I。我们称这种项是外延相等的。外延相等捕获了函数的等式的数学概念：两个函数是相等的，如果它们对于相同的参数总是生成相同的结果。相反的，项自身捕获了函数的内涵相等的概念：两个函数是相等的，当且仅当它们有相同的实现。有很多实现恒等函数的方式；(S K K)和I是其中的方式，(S K S)也是。我们将使用词等价来指示外延相等，保留等于给同一的组合子项。

更有趣的组合子是不动点组合子或Y组合子，它可以用来实现递归。

S-K基的完备性

可能会令人惊奇，事实上S和K可以组合起来生成外延相等于任何lambda项的组合子，所以依据邱奇-图灵论题，等价于任何可计算的函数。证明是提出一个变换T[ ]，它转换一个任意的lambda项到等价的组合子。

T[ ]可定义如下：

  1. T[V] = > V
  2. T[(E1 E2)] = >(T[E1] T[E2])
  3. T[λx.E] = > (K T[E])（如果x在E中没有自由出现）
  4. T[λx.x] = > I
  5. T[λx.λy.E] = > T[λx.T[λy.E]]（如果x在E中自由出现）
  6. T[λx.(E1 E2)] =>（S T[λx.E1] T[λx.E2]）

把lambda项转换成组合子项

例如，我们可以转换λx.λy.(y x)为组合子：

T[λx.λy.(y x)]
= T[λx.T[λy.(y x)]]（通过5）
= T[λx.(S T[λy.y] T[λy.x])]（通过6）
= T[λx.(S I T[λy.x])]（通过4）
= T[λx.(S I (K x))]（通过3）
= (S T[λx.(S I)] T[λx.(K x)])（通过6）
= (S (K (S I)) T[λx.(K x)])（通过3）
= (S (K (S I)) (S T[λx.K] T[λx.x]))（通过6）
= (S (K (S I)) (S (K K) T[λx.x]))（通过3）
= (S (K (S I)) (S (K K) I))（通过4）

如果我们应用这个组合子于任何两个项x和y，它可以归约到如下：

(S (K (S I)) (S (K K) I) x y)
= (K (S I) x (S (K K) I x) y)
= (S I (S (K K) I x) y)
= (I y (S (K K) I x y))
= (y (S (K K) I x y))
= (y (K K x (I x) y))
= (y (K (I x) y))
= (y (I x))
=(y x)

组合子表示 (S (K (S I)) (S (K K) I))比相应的lambda项λx.λy.(y x)要长很多，这是典型的。一般的，T[ ]构造可以把长度为n的lambda项展开为长度为Θ（3n）的组合子项。

T[ ]变换的解释

T[ ]变换的目的是要消除抽象。两个特殊情况，规则3和4是平凡的：λx.x明显等价于I，而λx.E明显等价于（K E），如果x在E中不是自由出现的。

前两个规则也是简单的：变量转换为自身；通过简单的转换applicand和参数到组合子，把在组合子项中允许的应用转换为组合子。

有趣的是规则5和6。规则5简单的声称要转换一个复杂的抽象为组合子，我们必须首先把它的主体转换成组合子，接着消除这个抽象。规则6实际上消除这个抽象。

λx.(E1 E2)是一个函数，它接受一个参数比如a，并把它代换到lambda项 (E1 E2)中x的位置上，生成 (E1 E2)[x : = a]。但是代换a到 (E1 E2)中x的位置上同于代换它到E1和E2二者中，所以

(E1 E2)[x := a] =(E1[x := a] E2[x := a])
(λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a))
=(S λx.E1 λx.E2 a)
= ((S λx.E1 λx.E2) a)

通过外延相等，

λx.(E1 E2) =(S λx.E1 λx.E2)

所以，要找到等价λx.(E1 E2)的组合子，找到等价于 (S λx.E1 λx.E2)的组合子就足够了，而

(S T[λx.E1] T[λx.E2])

显然合适。E1和E2每个都包含严格的比 (E1 E2)更少的应用，所以递归必定终止于根本没有应用的lambda项之上---要么是一个变量，要么是形如λx.E的项。

η-归约

通过T[ ]变换生成的组合子可以做的更小，如果我们采用η-归约规则：

T[λx.(E x)] = T[E]（如果x在E中不是自由的）

λx.(E x)是一个函数，它接受一个参数x并应用函数E于它之上；这外延相等于函数E自身。因此足够转换E到组合子形式。

采用这种简化，上面的例子变成：

T[λx.λy.(y x)]
= ...
= (S (K (S I)) T[λx.(K x)])
= (S (K (S I)) K) （通过η-归约）

这个组合子等价于早先的更长的那个：

(S (K (S I)) K x y)
= (K (S I) x (K x) y)
= (S I (K x) y)
= (I y (K x y))
= (y (K x y))
=(y x)

类似的，T[ ]变换的最初版本把恒等函数λf.λx.(f x)变换成 (S (S (K S) (S (K K) I)) (K I))。通过η-归约规则，λf.λx.(f x)被变换成I。

一点基

有一点基（one point basis），所有组合子都可从它复合而外延等于任何lambda项。这种基的最简单的例子是{X}:

X ≡ λx.((xS)K)

不难验证：

X (X (X X)) =ηβ K而
X (X (X (X X)))) =ηβ S.

因为{K, S}是基，得出{X}也是基。

B和C组合子

除了组合子S和K之外，Schönfinkel的著作中包含了现在叫做B和C的两个组合子，带有如下归约：

(C a b c) =(a c b)
(B a b c) = (a (b c))

他还解释了如何只使用S和K来表达它们。

这些表达式在把谓词逻辑或lambda演算转换成组合子表达式的时候非常有用。它们也被Curry和更后来的David Turner所使用，他们的名字已经关联到了它们的应用上了。使用这些组合子，我们可以扩展变换规则为如下：

  1. T[V] = > V
  2. T[(E1 E2)] = >(T[E1] T[E2])
  3. T[λx.E] = > (K T[E]) （如果x在E中不是自由的）
  4. T[λx.x] = > I
  5. T[λx.λy.E] = > T[λx.T[λy.E]]（如果x在E中是自由的）
  6. T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])（如果x在E1和E2二者中是自由的）
  7. T[λx.(E1 E2)] => (C T[λx.E1] E2)（如果x在E1中是自由的，但在E2中不是自由的）
  8. T[λx.(E1 E2)] => (B E1 T[λx.E2])（如果x在E2中是自由的，但在E1中不是自由的）

使用B和C组合子，λx.λy.(y x)的变换如下：

T[λx.λy.(y x)]
= T[λx.T[λy.(y x)]]
= T[λx.(C T[λy.y] x)] （通过规则7）
= T[λx.(C I x)]
= (C I) （η-归约）
= C*（传统规范记号：X* = X I）
= I'（传统规范记号：X' = C X）

(C I x y)的确归约到 (y x):

(C I x y)
=(I y x)
=(y x)

B和C的目的是S的有限版本。S接受一个值，并把在应用之前，把它代换入applicand和它的参数内，C只在applicand内进行代换，而B只在参数内进行代换。

这些组合子的现代名字源于哈斯凱爾·加里在1930年的博士论文（参见B,C,K,W系统）。在Schönfinkel的最初著作中，把现在的S, K, I, B和C分别叫做S, C, I, Z和T。

CLK与CLI演算

在本文描述的CLK和CLI演算必须做出区分。这种区别对应于在λK和λI演算之间的区别。不同于λK演算，λI演算限制抽象为：

λv.E1这里的v在E1中有至少一次自由出现。

作为结论，组合子K不出现在λI演算和CLI演算中。CLI的常量有：I, B, C和S，这形成了所有CLI项可以从它复合出来的基，B和C模拟K。所有λI项可以转换成等价的CLI组合子，依据类似于前面提供的把λK项转换成CLK组合子的规则。参见Barendregt (1984)第9章。

逆转换

从组合子项到lambda项的转换L[ ]是平凡的：

L[I] = λx.x
L[K] = λx.λy.x
L[C] = λx.λy.λz.(x z y)
L[B] = λx.λy.λz.(x (y z))
L[S] = λx.λy.λz.(x z (y z))
L[(E1 E2)] =（L[E1] L[E2]）

但是，要注意这个变换不是我们见到的任何版本的T[ ]的逆变换。

组合子演算的不可判定性

一个组合子项是否有规范形式，两个组合子项是否是等价的等等都是不可判定的。者等价于 lambda项相应问题的不可判定性。但是，有一个直接证明如下：

首先，观察到项

Ω = (S I I (S I I))

没有规范形式，因为它在三个步骤之后归约到自身，如下：

(S I I (S I I))
= (I (S I I) (I (S I I)))
= (S I I (I (S I I)))
= (S I I (S I I))

而且没有其他归约次序可以使表达式更短些。

现在，假设N是检测范式的组合子，使得

(N x) => T,如果x有规范形式
F,没有规范形式。

(这里的T和F是常规的lambda演算的真假定义λx.λy.x和λx.λy.y的变换。 组合子版本是T = K和F = (K I))。

现在设

Z = (C (C (B N (S I I)) Ω) I)

现在考虑项（S I I Z）。(S I I Z)有规范形式吗?它有规范形式，当且仅当下列也有：

(S I I Z)
= (I Z (I Z))
= (Z (I Z))
=(Z Z)
= (C (C (B N (S I I)) Ω) I Z) （Z的定义）
= (C (B N (S I I)) Ω Z I)
= (B N (S I I) Z Ω I)
= (N (S I I Z) Ω I)

现在我们需要应用N于(S I I Z)。(S I I Z)要么有规范形式，要么没有。如果它确实有规范形式，则前述归约为如下：

(N (S I I Z) Ω I)
= (K Ω I) （N的定义）
= Ω

但是Ω没有规范形式，所以我们得到矛盾。但是如果 (S I I Z)没有规范形式，则前述归约为如下：

(N (S I I Z) Ω I)
= (K I Ω I) （N的定义）
=(I I)
= I

这意味着 (S I I Z)的范式简单的是I，这是另一个矛盾。所以，假设的范式组合子N不存在。

应用

函数式语言的编译

函数式编程语言经常基于lambda演算的简单而普遍的语义。

David Turner使用它的组合子实现了SASL编程语言。

Kenneth E. Iverson在他的J编程语言中使用了基于Curry的组合子的原语（primitive），J语言是APL语言的后继者。这使得Iverson达成了隐式编程，就是说，编程采用不包含变量的函数表达式，并一起使用与这种程序共同工作的强力工具。结果是在任何带有用户定义算子的类APL语言中隐式编程都是可能的[2]。

逻辑

Curry-Howard同构蕴涵了在逻辑和编程之间的联系：每个直觉逻辑的有效的定理证明都直接对应于一个有类型的lambda项的归约，反之亦然。定理自身也通过函数类型标志（signature）来识别。特别是，有类型的组合子逻辑对应于证明论中的希尔伯特系统。

K和S组合子对应于公理

AK: A → (B → A),
AS: (A → (B → C)) → ((A → B) → (A → C)),

而函数应用对应于肯定前件规则

MP:从A且A → B推出B。

由AK, AS和MP组成的演算对于直觉逻辑的蕴涵片段是完备的。考虑所有演绎闭合的公式的集合W，按包含排序。则是直觉Kripke框架，我们定义在这个框架内的模型为

这个定义服从对→的满足的条件：在一方面，如果，并且使得且，则通过肯定前件而。在另一方面，如，则通过演绎定理而，因此的演绎闭包是的一个元素使得, 和。

设A是在演算中不能证明的任何公式。则A不属于非空集合的演绎闭包X，所以，而A不是直觉有效的。

参见

注釋
  1. Seldin, Jonathan. .
  2. Cherlin, Edward. . Proceedings of the International Conference on APL '91. 1991: 88–93. ISBN 0897914414. doi:10.1145/114054.114065.

引用
  • Moses Schönfinkel, 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879-1931, Jean van Heijenoort, ed. Harvard University Press, 1967. ISBN 978-0-674-32449-7 The article that founded combinatory logic.
  • Curry, Haskell B.; Robert Feys. 1. Amsterdam: North Holland. 1958.
  • Curry, Haskell B.; J. Roger Hindley and Jonathan P. Seldin. 2. Amsterdam: North Holland. 1972. ISBN 978-0-7204-2208-5.
  • Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 978-0-201-19249-0
  • Paulson, Lawrence C., 1995. Foundations of Functional Programming. University of Cambridge.
  • Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry-Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
  • 1920-1931 Currys block notes
  • Hindley, Roger, and Meredith, 1990, "Principal Type-Schemes and Condensed Detachment," Journal of Symbolic Logic 55: 90-105
  • Hendrik Pieter Barendregt, 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland. ISBN 978-0-444-87508-2
  • Quine, W. V., [1960] 1966. "Variables explained away." Chapter 23 in W. V. Quine, Selected Logic Papers, 227–235. New York: Random House. Originally read by invitation to the American Philosophical Association in April 1960 and published in their Proceedings.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.