B, C, K, W system

The combinators are defined as follows: • B x y z = x (y z) • C x y z = x z y • K x y = x • W x y = x y y Intuitively, • B x y is the composition of x and y; • C x is x with the flipped arguments order; • K x is the "constant x" function, which discards the next argument; • W duplicates its second argument for the doubled application to the first. Thus, it "joins" its first argument's two expectations for input into one. ==Connection to other combinators==

In recent decades, the SKI combinator calculus, with only two primitive combinators, K and S, has become the canonical approach to combinatory logic. B, C, and W can be expressed in terms of S and K as follows: • B = S (K S) K • C = S (S (K (S (K S) K)) S) (K K) • K = K • W = S S (S K) Another way is, having defined B as above, to further define C = S(BBS)(KK) and W = CSI. In fact, S(Kx)yz = Bxyz and Sx(Ky)z = Cxyz, as is easily verified. Going the other direction, SKI can be defined in terms of B, C, K, W as: • I = W K • K = K • S = B (B (B W) C) (B B) = B (B W) (B B C). Also of note, Y combinator has a short expression in this system, as Y = BU(CBU) = BU(BWB) = B(W(WK))(BWB), where U = WI = SII is the self-application combinator. Using just two combinators, B and W, an infinite number of fixpoint combinators can be constructed, one example being B(WW)(BW(BBB)), discovered by R. Statman in 1986. ==Connection to intuitionistic logic==

The combinators B, C, K and W correspond to four well-known axioms of propositional logic: :AB: (B → C) → ((A → B) → (A → C)), :AC: (A → (B → C)) → (B → (A → C)), :AK: A → (B → A), :AW: (A → (A → B)) → (A → B). Function application corresponds to the rule modus ponens: :MP: from A → B and A infer B. The axioms AB, AC, AK and AW, and the rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model: • the implicational fragment of classical logic, would require the combinatory analog to the law of excluded middle, e.g., Peirce's law; • full classical logic, would require the combinatory analog to the propositional axiom F → A. ==See also==