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 Haskell Brooks Curry (; September 12, 1900 – September 1, 1982) was an American mathematician and logician. Curry is best known for his work in combinatory logic. While the initial concept of combinatory logic was based on a single paper by ...

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 Composition or Compositions may refer to: Arts and literature *Composition (dance), practice and teaching of choreography *Composition (language), in literature and rhetoric, producing a work in spoken tradition and written discourse, to include v ...

of ''x'' and ''y''; * C ''x'' is ''x'' with the flipped

arguments An argument is a statement or group of statements called premises intended to determine the degree of truth or acceptability of another statement called conclusion. Arguments can be studied from three main perspectives: the logical, the dialectic ...

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 The SKI combinator calculus is a combinatory logic system and a computational system. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory o ...

, 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).

Raymond Smullyan Raymond Merrill Smullyan (; May 25, 1919 – February 6, 2017) was an American mathematician, magician, concert pianist, logician, Taoist, and philosopher. Born in Far Rockaway, New York, his first career was stage magic. He earned a BSc from ...

(1994) ''Diagonalization and Self-Reference''. Oxford Univ. Press: 344, 3.6(d) and 3.7. Also of note, Y combinator has a short expression in this system, as Y = BU(CBU), where U = WI = SII is the self-application combinator. Then we have Yg = U(BgU) = BgU(BgU) = g(U(BgU)) = g(Yg).

Connection to intuitionistic logic

The combinators B, C, K and W correspond to four well-known axioms of

sentential logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...

: :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 Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...

. 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 In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...

, e.g.,

Peirce's law In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that i ...

; * Complete classical logic, would require the combinatory analog to the sentential axiom F → ''A''.

Notes

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. *

(1930) "Grundlagen der kombinatorischen Logik," ''Amer. J. Math. 52'': 509–536; 789–834. https://doi.org/10.2307/2370619 *{{cite book , last1 = Curry , first1 = Haskell B. , first2 = J. Roger , last2 = Hindley , first3 = Jonathan P. , last3 = Seldin , authorlink1 = Haskell Curry , authorlink2 = J. Roger Hindley , authorlink3 = Jonathan P. Seldin , title = Combinatory Logic , volume = II , year = 1972 , publisher = North Holland , location = Amsterdam , isbn = 0-7204-2208-6 *

(1994) ''Diagonalization and Self-Reference''. Oxford Univ. Press.

External links