It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic.
Another way of eliminating quantified variables is Quine's predicate functor logic.
Haskell Curry rediscovered the combinators while working as an instructor at Princeton University in late 1927.
[3] In the late 1930s, Alonzo Church and his students at Princeton invented a rival formalism for functional abstraction, the lambda calculus, which proved more popular than combinatory logic.
The upshot of these historical contingencies was that until theoretical computer science began taking an interest in combinatory logic in the 1960s and 1970s, nearly all work on the subject was by Haskell Curry and his students, or by Robert Feys in Belgium.
Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions without free variables.
Hence combinatory logic has been used to model some non-strict functional programming languages and hardware.
The purest form of this view is the programming language Unlambda, whose sole primitives are the S and K combinators augmented with character input/output.
[5] Dana Scott in the 1960s and 1970s showed how to marry model theory and combinatory logic.
Lambda calculus is concerned with objects called lambda-terms, which can be represented by the following three forms of strings: where
The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions.
It is possible to identify terms in lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator, q.v.
Lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including Turing machines); that is, any calculation that can be accomplished in any of these other models can be expressed in lambda calculus, and vice versa.
Combinatory logic is a model of computation equivalent to lambda calculus, but without abstraction.
The advantage of this is that evaluating expressions in lambda calculus is quite complicated because the semantics of substitution must be specified with great care to avoid variable capture problems.
In contrast, evaluating expressions in combinatory logic is much simpler, because there is no notion of substitution.
In combinatory logic, each primitive combinator comes with a reduction rule of the form where E is a term mentioning only variables from the set {x1 ... xn}.
In contrast, the terms themselves, together with the reduction of primitive combinators, capture the notion of intensional equality of functions: that two functions are equal only if they have identical implementations up to the expansion of primitive combinators.
S and K can be composed to produce combinators that are extensionally equal to any lambda term, and therefore, by Church's thesis, to any computable function whatsoever.
The proof is to present a transformation, T[ ], which converts an arbitrary lambda term into an equivalent combinator.
T[ ] may be defined as follows: Note that T[ ] as given is not a well-typed mathematical function, but rather a term rewriter: Although it eventually yields a combinator, the transformation may generate intermediary expressions that are neither lambda terms nor combinators, via rule (5).
(E1 E2) is a function which takes an argument, say a, and substitutes it into the lambda term (E1 E2) in place of x, yielding (E1 E2)[x : = a].
The combinators generated by the T[ ] transformation can be made smaller if we take into account the η-reduction rule: λx.
There are one-point bases from which every combinator can be composed extensionally equal to any lambda term.
The modern names for the combinators come from Haskell Curry's doctoral thesis of 1930 (see B, C, K, W System).
The reduction in combinator size that results from the new transformation rules can also be achieved without introducing B and C, as demonstrated in Section 3.2 of Tromp (2008).
A normal form is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified.
Kenneth E. Iverson used primitives based on Curry's combinators in his J programming language, a successor to APL.
Specifically, a typed combinatory logic corresponds to a Hilbert system in proof theory.
The K and S combinators correspond to the axioms and function application corresponds to the detachment (modus ponens) rule The calculus consisting of AK, AS, and MP is complete for the implicational fragment of the intuitionistic logic, which can be seen as follows.