B, C, K, Wシステムは、基本的な4つの定数記号 B, C, K, W からなるコンビネータ論理の変種である。この体系はハスケル・カリーの博士論文Grundlagen der kombinatorischen Logikによるもので、その結論部分はCurry 1930において示された。
概要 定数記号 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 は関数合成。 C x y z は引数交換。 K x y は破棄； W x y は複製。
2つの基本的な定数記号 S, K（及び SKK と外延的に同値な閉項 I）からなる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 (S K)
一方で、S, K, I は B, C, K, W からなる項によって次のように表現できる： I = W K K = K S = B (B (B W) C) (B B) = B (B W) (B B C).Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.
すなわち、SKIコンビネータ計算とB,C,K,Wシステムは等価な計算体系である。
直観主義論理との関係 定数記号 B, C, K, W はそれぞれよく知られた4つの命題論理の公理と対応するより正確には、定数記号の型と公理図式とが対応する。：
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:
公理 AB, AC, AK, AW 及び推論規則 MP は、直観主義命題論理のに対して完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を加えたものは古典命題論理と対応する。コンビネータ W とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-λ計算と対応するものである。
関連項目 コンビネータ論理 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. 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)."