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

Combinatory logic

Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...

 that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry

Haskell Curry

Haskell Brooks Curry 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 Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...

 in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930).

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
  Function composition
  In mathematics, function composition is the application of one function to the results of another. For instance, the functions and can be composed by computing the output of g when it has an argument of f instead of x...
  
   of the arguments x and y;
• C x y z swaps the arguments y and z;
• K x y discards the argument y;
• W x y duplicates the argument y.

In recent decades, the SKI combinator calculus

SKI combinator calculus

SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus. It can be thought of as a computer programming language, though it is not useful for writing software...

, with only two primitive combinators, K and S, has become the canonical approach to combinatory logic

Combinatory logic

Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...

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

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

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

Modus ponens

In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...

:

MP: from A and A → B infer B.

The axioms AB, AC, AK and AW, and the rule MP are complete for the implicational fragment of intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

. In order for combinatory logic to have as a model:

• The implicational fragment
  Implicational propositional calculus
  In mathematical logic, the implicational propositional calculus is a version of classical propositional calculus which uses only one connective, called implication or conditional...
  
   of classical logic
  Classical logic
  Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
  
  , would require the combinatory analog to the law of excluded middle
  Law of excluded middle
  In logic, the law of excluded middle is the third of the so-called three classic laws of thought. It states that for any proposition, either that proposition is true, or its negation is....
  
  , e.g., Peirce's law
  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 involves only one sort of connective, namely...
  
  ;
• Complete classical logic, would require the combinatory analog to the sentential axiom F → A.

See also

• Combinatory logic
  Combinatory logic
  Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
  
  
• SKI combinator calculus
  SKI combinator calculus
  SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus. It can be thought of as a computer programming language, though it is not useful for writing software...
  
  
• Lambda calculus
  Lambda calculus
  In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
  
  
• To Mock a Mockingbird
  To Mock a Mockingbird
  To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic is a book by the mathematician and logician Raymond Smullyan. It contains many nontrivial recreational puzzles of the sort for which Smullyan is well-known...
  
  

External links

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