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

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

. 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 (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: :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, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...

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

, would require the combinatory analog to the law of excluded middle, 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 tha ...

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

Notes

References

Hendrik Pieter Barendregt Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory. Life and work Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...

(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