B, C, K, W system

The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930).

Definition

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.

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).^[1]

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,^[2] 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 sentential 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;
Complete classical logic, would require the combinatory analog to the sentential axiom F → A.

Notes

^ Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.
^ Larry Wos, William McCune (September 1988). "Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report" (PDF). Argonne National Laboratory. Retrieved December 12, 2024., p.77

References

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 0-444-87508-5
Haskell Curry (1930) "Grundlagen der kombinatorischen Logik," Amer. J. Math. 52: 509–536; 789–834. https://doi.org/10.2307/2370619
Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press.

External links

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

[1] Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.

[2] Larry Wos, William McCune (September 1988). "Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report" (PDF). Argonne National Laboratory. Retrieved December 12, 2024., p.77

[1]

[2]