The B, C, K, W system is a variant of

combinatory logic Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of com ...

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). It has expressive power equivalent to that of S, K, I system. Both systems are fully interchangeable. When compiling to combinators, an implementation may equally choose one system or the other, or both, as it helps shorten the encodings of functions. For example, the encodings of C exclusively in terms of S,K,I, as well as of S in B,C,W,K are long and complicated, as can be seen below, while their corresponding computational machine implementations are equally trivial. It can be worth it to add additional interpretation rules, allowing for much shorter code which can lead to more efficient execution.

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

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

arguments An argument is a series of sentences, statements, or propositions some of which are called premises and one is the conclusion. The purpose of an argument is to give reasons for one's conclusion via justification, explanation, and/or persua ...

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

. 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., p.77

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 In propositional logic, (; MP), also known as (), implication elimination, or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "''P'' implies ''Q.'' ''P'' is true. Therefore, ''Q'' must ...

: :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 Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this c ...

, 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 three laws of thought, along with the law of noncontradiction and t ...

, 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#Mathematics, axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written ...

; * 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. * Haskell Curry (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 * Raymond Smullyan (1994) ''Diagonalization and Self-Reference''. Oxford Univ. Press.

External links