组合子逻辑
维基百科，自由的百科全书
组合子逻辑是 Moses Schönfinkel 和 Haskell Curry 介入的一种符号系统，用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。
目录 |
[编辑] 数学中的组合子逻辑
组合子逻辑意图作为简单的元逻辑，它能澄清在逻辑符号中的变量的意义，并真正的消除对它们的需要。
参见 Curry, 1958-72。
[编辑] 计算中的组合子逻辑
在计算机科学中，组合子逻辑被用做可计算性理论(什么是可计算的)中计算和证明论(什么是可以在数学上证明的)的简化模型。这个理论尽管简单，但捕获了计算本质的很多根本特征。
组合子逻辑可以被看作是 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 项展开为长度为 Θ(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。
[编辑] Curry 的 B 和 C 组合子
组合子 S 和 K 已经在 Schönfinkel 的著作中提出(尽管使用了符号 C 表示 K)，Curry 在他 1930 年的博士论文中介绍入了 B、C、W (和 K) 组合子(参见B,C,K,W系统)。在 Combinatory Logic V. I 中，我们回到了 S、K，但是(通过马尔可夫算法)他使用 B 和 C 来简化了很多归约。这被后来的 David Turner 所使用，他的名字已经同它的计算使用连结在一起了。介入这两个新组合子:
(C a b c) = (a c b)
(B a b c) = (a (b c))
使用这些组合子，我们可以扩展变换规则为如下:
- 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 只在参数内进行代换。
[编辑] 逆转换
从组合子项到 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)来识别。特别是，有类型的组合子逻辑对应于证明论中的希尔伯特系统。
[编辑] 参见
[编辑] 引用
- "über die Bausteine der mathematischen Logik", Moses Sch?nfinkel, 1924, translated as "On the Building Blocks of Mathematical Logic" in From Frege to G?del: a source book in mathematical logic, 1879-1931, ed. Jean van Heijenoort, Harvard University Press, 1977. ISBN 0674324498 The original publication of combinatory logic.
- Combinatory Logic. Curry, Haskell B. et al., North-Holland, 1972. ISBN 0720422086 A comprehensive overview of combinatory logic, including a historical sketch.
- Functional Programming. Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. ISBN 0201192497
- "Foundations of Functional Programming". Lawrence C. Paulson. University of Cambridge, 1995.
- "Lectures on the Curry-Howard Isomorphism". S?rensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1999.
- 1920-1931 Curry's block notes
- "Principal Type-Schemes and Condensed Detachment", Hindley and Meredith, Journal of Symbolic Logic (JSL), Volume 55 (1990), Number 1, pages 90-105
