组合子逻辑

维库，知识与思想的自由文库

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

[编辑] 数学中的组合子逻辑

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

组合子逻辑的最初发明者 Schönfinkel，在1929年之后基本停止了发表著作。Curry 在 1920 年代晚期于哥廷根大学读博士的时候重新发现了组合子，但是这个划时代的系在 1933年被拆解了。在 1930 年代后期，邱奇和他的学生在普林斯顿发明了一个竞争的函数抽象的形式化，就是 lambda 演算，它比组合子逻辑更加流行。这些历史上的意外事件的结果是直到在 1960 年代和 1970 年代理论计算机科学开始感兴趣于组合子逻辑，关于这个主题的几乎所有工作都是 Haskell Curry 和他的学生们，或比利时的 Robert Feys 做的。Curry 和 Feys (1958) 和 Curry et al (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 叫做抽象的形式参数(formal parameter)，而 E1 是抽象的“主体”。

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

形如 (E1 E2) 的项叫做应用。应用建模函数调用或执行: 调用 E1 所代表的函数，带有 E2 作为它的参数(argument)，并计算结果。如果 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，恒等(identity)组合子，定义为

(I x) = x

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

((K x) y) = x

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

(K x y) = x

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

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

S 应用 x 于 y，在首先代换 z 到它们中的每个之后。

给出 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) 也是。我们将使用词等价(equivalent)来指示外延相等，保留等于给同一的组合子项。

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

[编辑] S-K 基的完备性

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

T[ ] 可定义如下:

T[V] => V
T[(E1 E2)] => (T[E1] T[E2])
T[λx.E] => (K T[E]) (如果 x 在 E 中不是自由的)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (如果 x 在 E 中是自由的)
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 项展开为长度为 Θ(3ⁿ) 的组合子项。

[编辑] 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。

[编辑] 一点基

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

       X ≡ λx.((xS)K)

不难验证:

       X (X (X X)) =^ηß K and
       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 所使用，他们的名字已经关联到了它们的应用上了。使用这些组合子，我们可以扩展变换规则为如下:

T[V] => V
T[(E1 E2)] => (T[E1] T[E2])
T[λx.E] => (K T[E]) (如果 x 在 E 中不是自由的)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (如果 x 在 E 中是自由的)
T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) (如果 x 在 E1 和 E2 二者中是自由的)
T[λx.(E1 E2)] => (C T[λx.E1] E2) (如果 x 在 E1 中是自由的，但在 E2 中不是自由的)
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 只在参数内进行代换。

这些组合子的现代名字源于 Haskell Curry 在 1930 年的博士论文(参见 B,C,K,W系统)。在 Schönfinkel 的最初著作中，把现在的 S, K, I, B 和 C 分别叫做 S, C, I, Z 和 T。

[编辑] CL_K 与 CL_I 演算

在本文描述的 CL_K 和 CL_I 演算必须做出区分。这种区别对应于在 λ_K 和 λ_I 演算之间的区别。不同于 λ_K 演算，λ_I 演算限制抽象为:

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

作为结论，组合子 K 不出现在 λ_I 演算和 CL_I 演算中。CL_I 的常量有: I, B, C 和 S，这形成了所有 CL_I 项可以从它复合出来的基，B 和 C 模拟 K。所有 λ_I 项可以转换成等价的 CL_I 组合子，依据类似于前面提供的把 λ_K 项转换成CL_K 组合子的规则。参见 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 编程语言。

[编辑] 逻辑

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，按包含排序。则 $\langle W,\subseteq\rangle$ 是直觉Kripke 框架，我们定义在这个框架内的模型 $\langle W,\subseteq,\Vdash\rangle$ 为

$X\Vdash A\iff A\in X.$

这个定义服从对 → 的满足的条件: 在一方面，如果 $X\Vdash A\to B$ ，并且 $Y\in W$ 使得 $Y\supseteq X$ 且 $Y\Vdash A$ ，则通过肯定前件而 $Y\Vdash B$ 。在另一方面，如 $X\not\Vdash A\to B$ ，则通过演绎定理而 $X,A\not\vdash B$ ，因此 $X\cup\{A\}$ 的演绎闭包是 $Y\in W$ 的一个元素使得 $Y\supseteq X$ , $Y\Vdash A$ 和 $Y\not\Vdash B$ 。

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

[编辑] 参见

[编辑] 引用

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 0-674-32449-8 The article that founded combinatory logic.
Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Amsterdam: North Holland.

Curry, Haskell B.; J. Roger Hindley and Jonathan P. Seldin (1972). Combinatory Logic Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.

Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 0-201-19249-7
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 Curry's 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 0-444-87508-5
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.

来自“http://www.wikilib.com/wiki/%E7%BB%84%E5%90%88%E5%AD%90%E9%80%BB%E8%BE%91”

个人工具

组合子逻辑

维库，知识与思想的自由文库

目录

[编辑] 数学中的组合子逻辑

[编辑] 计算中的组合子逻辑

[编辑] lambda 演算摘要

[编辑] 组合子演算

[编辑] 组合子项

[编辑] 组合子的例子

[编辑] S-K 基的完备性

[编辑] 把 lambda 项转换成组合子项

[编辑] T[ ] 变换的解释

[编辑] 变换的简化

[编辑] η-归约

[编辑] 一点基

[编辑] B 和 C 组合子

[编辑] CL_K 与 CL_I 演算

[编辑] 逆转换

[编辑] 组合子演算的不可判定性

[编辑] 应用

[编辑] 函数式语言的编译

[编辑] 逻辑

[编辑] 参见

[编辑] 引用

查看

导航

搜索

工具

其它语言

AD Links

个人工具

组合子逻辑

维库，知识与思想的自由文库

目录

[编辑] 数学中的组合子逻辑

[编辑] 计算中的组合子逻辑

[编辑] lambda 演算摘要

[编辑] 组合子演算

[编辑] 组合子项

[编辑] 组合子的例子

[编辑] S-K 基的完备性

[编辑] 把 lambda 项转换成组合子项

[编辑] T[ ] 变换的解释

[编辑] 变换的简化

[编辑] η-归约

[编辑] 一点基

[编辑] B 和 C 组合子

[编辑] CLK 与 CLI 演算

[编辑] 逆转换

[编辑] 组合子演算的不可判定性

[编辑] 应用

[编辑] 函数式语言的编译

[编辑] 逻辑

[编辑] 参见

[编辑] 引用

查看

导航

搜索

工具

其它语言

AD Links

[编辑] CL_K 与 CL_I 演算