B,C,K,W系统

1930年哈斯凱爾·加里在他的博士论文《Grundlagen der kombinatorischen Logik》中提议了一个組合子邏輯系統。它带有基本组合子B、C、K和W（采用了现在的命名）。

 定義 
 B x y z = x(y z)
 C x y z = x z y
 K x y = x
 W x y = x y y

直觉上，
 B x y是函数复合x o y
 C x y z交换参数y和z
 K x y忽略第二个参数y
 W x y复制参数y

在當代，只有兩個基本組合子K和S的SKI組合子演算成為了組合子邏輯的規范方式。B, C和W可以使用S和K表達為如下：
 B = S (K S) K
 C = S (S (K (S (K S) K)) S)(K K)
 K = K
 W = S S（K (S K K))

在另一個方向上，SKI可以依據B,C,K,W定義為：
 I = W K
 K = K
 S = B (B (B W) C) (B B)Raymond Smullyan（1994）Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d). = B (B B B W B) C

 與直覺主義邏輯的連結 
組合子 , ,  和  對應於眾所周知的命題邏輯四公理：

AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).

而函數應用對應於肯定前件
MP: 如果 A 且 A → B，則 B。

公理 AB, AC, AK 和 AW 以及函數應用規則 MP 對於直覺邏輯的蘊涵片段是完整的。為了使組合邏輯能模型化為直覺邏輯：
古典邏輯的蕴涵命题演算，需要與排中律相結合，例如，皮尔士定律;
完整的古典邏輯，需以組合子模擬到命題公式 F → A。

 参见 

组合子逻辑
SKI組合子演算

 引用 
Hendrik Pieter Barendregt（1984）The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies in Logic and the Foundations of Mathematics. North-Holland. ISBN 978-0-444-87508-2
 Haskell Curry（1930）"Grundlagen der kombinatorischen Logik," Amer. J. Math. 52: 509-536; 789-834.

Raymond Smullyan（1994）Diagonalization and Self-Reference. Oxford Univ. Press.
 注釋 

 外部連結 
 Keenan, David C. (2001) "To Dissect a Mockingbird."
 Rathman, Chris, "Combinator Birds."
 ""Drag 'n' Drop Combinators (Java Applet)."

Category:组合子逻辑