Combinatory logic
Combinatory logic is a model by which logical statements can be described as a combination of a small number of primitive elements called combinators. Each combinator is like a function or lambda abstraction, but without any free variables. A "sentence" in combinatory logic is called a combinatory term, and is composed of combinators, free variables, and applications of one combinatory term to another.
Combinatory logic can capture the meaning of any arithmetic or logical statement (and by extension, any noninteractive computer program), making it a Turingcomplete computational model. It is often described and/or implemented in terms of rewriting (of graphs, trees, or terms).
Combinatory logic forces you to use pointfree programming style to write useful programs.
Contents
Syntax
The syntax commonly used for combinators is like that of the lambda calculus: each combinator only takes one argument (but may yield another combinator which will consume further arguments), application associates to the left, and parentheses are only used for disambiguation, not to delimit an argument list.
If you wish to see the grammar of pure combinatory logic, it is as such:
combinator ::= Combinator_Symbol ; app ::= exp exp ; parenexp ::= "(" exp ")" ; expression ::= app  parenexp  combinator ;
This is a fairly simple grammar, so it will not be explained here.
The syntax of the commonlyused combinatory logic (with assignments and such) is:
combinator ::= Combinator_Symbol ; var ::= Var_Symbol ; app ::= exp exp ; parenexp ::= "(" exp ")" ; expression ::= app  parenexp  combinator ; assignment ::= combinator {var} "=" expression {var} ; line ::= expression  assignment ;
Combinators
SKI calculus
In 1924, Moses Schönfinkel devised the three traditional primitive combinators. All other expressions can be formed by application of these combinators to each other:

I
, the identity combinator. Applied to some combinator x, it simply evaluates to x:
I x = x;

K
, the constantmaking combinator. Applied to some combinator x, it yields a combinator that always evaluates to x, no matter what it is applied to:
K x y = x;

S
, the application combinator. Applied to three combinators, it applies each of the first two combinators to the last, then applies the first result of that to the second:
S f g x = f x (g x);
In fact, only two different combinators are strictly necessary; the I
combinator can be formed from the S
and K
combinators:
S K K x = I x = x
BCKW calculus
The original system of four primitive combinators, used by Haskell Curry and equivalent to SKI, were B, C, K, and W. These are defined by:
B x y z = x (y z); C x y z = x z y; K x y = x; W x y = x y y;
To define the B, C, K, W primitives from the SKI system, you can use the expressions:
B = S (K S) K; C = S (B B S) (K K); K = K; W = S S (S K);
Derivations to prove these (follow them by eta conversions):
S (K S) K x y z = K S x (K x) y z = S (K x) y z = K x z (y z) = x (y z) = B x y z; S (B B S) (K K) x y z = B B S x (K K x) y z = B B S x K y z = B (S x) K y z = S x (K y) z = x z (K y z) = x z y; S S (S K) x y = S x (S K x) y = x y (S K x y) = x y (K y (X y)) = x y y = W x y;
To define the S, K, I primitives from the BCKW system (two alternative definitions are given for S), use:
S = B (B (B W) C) (B B) = B (B W) (B B C); K = K; I = S K K;
Derivations to prove these (follow them by eta conversions):
B (B W) (B B C) x y z = B W (B B C x) y z = W (B B C x y) z = B B C x y z z = B (C x) y z z = C x (y z) z = x z (y z) = S x y z; B (B (B W) C) (B B) x y z = B (B W) C (B B x) y z = B W (C (B B x)) y z = W (C (B B x) y) z = C (B B x) y z z = B B x z y z = B (x z) y z = x z (y z) = S x y z; I x = S K K x = K x (K x) = x;
Alternative Primitives
Though SK(I)
is the traditional set of primitives, some alternative primitives have been created with different goals. For example, Iota, where ιx = (xs)k
.
Nonprimitives
Various other nonprimitive combinators have been defined. For another, longer example, the named birds from "To Mock a Mockingbird" are:
B = S(KS)K #Bluebird B[1] = BBB #Blackbird B[2] = B(BBB)B #Bunting B[3] = B(BB)B #Becard C = S(BBS)(KK) #Cardinal D = BB #Dove D[1] = B(BB) #Dickcissel D[2] = BB(BB) #Dovekies E = B(BBB) #Eagle Ê = B(BBB)(B(BBB)) #Bald Eagle F = ETTET #Finch G = BBC #Goldfinch H = BW(BC) #Hummingbird I = SKK #Identity Bird/Idiot J = B(BC)(W(BC(B(BBB)))) #Jay L = CBM #Lark M = SII #Mockingbird M[2] = BM #Double Mockingbird O = SI #Owl Q = CB #Queer Bird Q[1] = BCB #Quixotic Bird Q[2] = C(BCB) #Quizzical Bird Q[3] = BT #Quirky Bird Q[4] = F*B #Quacky Bird R = BTT #Robin T = CI #Thrush U = LO #Turing (!!!) V = BCT #Vireo/Pairing W[1] = CW #Converse Warbler Y = SLL #Why Bird/Sage Bird I* = S(SK) #Identity Bird Once Removed W* = BW #Warbler Once Removed C* = BC #Cardinal Once Removed R* = C*C* #Robin Once Removed F* = BC*R* #Finch Once Removed V* = C*F* #Vireo Once Remvoed W** = B(BW) #Warbler Twice Removed C** = BC* #Cardinal Twice Removed R** = BR* #Robin Twice Removed F** = BF* #Finch Twice Removed V** = BV* #Vireo Twice Removed ω = MM #OMEGA BIRD xD θ = YO #Theta (Bird?)
Example
Let's trace through S K K x
, both to show that it is equivalent to I x
, and just as an example of how combinatory logic works.
First, S
applies each of its first two arguments to its last argument, so the expression S K K x
can be thought of as reducing to:
K x (K x)
Further, for simplicity's sake, K x
can be thought of as yielding a combinator that, when applied to anything, yields x. We'll call this combinator yieldsx
to demonstrate, even though it wouldn't really be used:
yieldsx yieldsx
Finally, yieldsx
is applied to itself. But, no matter what it is applied to, even itself, the result will always be x:
x
So from this we can see that S K K x
is equivalent to I x
.
See also
 S and K Turingcompleteness proof
 Unlambda
 Iota
 Probabilistic combinatory logic
 User:Hppavilion1/Combinatory temporal logic
External resources
 Online course in combinatory logic using Scheme (from the Wayback Machine; retrieved on 13 October 2004)
 Wikipedia:Combinatory_logic
 Wikipedia:SKI combinator calculus
 Wikipedia:B, C, K, W system
 Raymond Smullyan, To mock a mocking bird and other logic puzzles