B,C,K,Wシステム

定数記号 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).^[1]

すなわち、SKIコンビネータ計算とB,C,K,Wシステムは等価な計算体系である。

定数記号 B, C, K, W はそれぞれよく知られた4つの命題論理の公理と対応する^[2]：

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: ${\displaystyle A\to B,A\vdash B}$

公理 AB, AC, AK, AW 及び推論規則 MP は、直観主義命題論理の含意断片（英語版）に対して完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を加えたものは古典命題論理と対応する。コンビネータ W とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-λ計算と対応するものである。

• コンビネータ論理
• SKIコンビネータ計算
• ラムダ計算
• カリー＝ハワード同型対応
• To Mock a Mockingbird（英語版）