Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel^[1] and Haskell Curry,^[2] and 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 languages. 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. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.

In mathematics

Combinatory logic was originally intended as a 'pre-logic' that would clarify the role of quantified variables in logic, essentially by eliminating them. Another way of eliminating quantified variables is Quine's predicate functor logic. While the expressive power of combinatory logic typically exceeds that of first-order logic, the expressive power of predicate functor logic is identical to that of first order logic (Quine 1960, 1966, 1976).

The original inventor of combinatory logic, Moses Schönfinkel, published nothing on combinatory logic after his original 1924 paper. 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. Curry and Feys (1958), and Curry et al. (1972) survey the early history of combinatory logic. For a more modern treatment of combinatory logic and the lambda calculus together, see the book by Barendregt,^[4] which reviews the models Dana Scott devised for combinatory logic in the 1960s and 1970s.

In computing

In computer science, combinatory logic is used as a simplified model of computation, used in computability theory and proof theory. Despite its simplicity, combinatory logic captures many essential features of computation.

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. It is easy to transform lambda expressions into combinator expressions, and combinator reduction is much simpler than lambda reduction. 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. Although not a practical programming language, Unlambda is of some theoretical interest.

Combinatory logic can be given a variety of interpretations. Many early papers by Curry showed how to translate axiom sets for conventional logic into combinatory logic equations.^[5] Dana Scott in the 1960s and 1970s showed how to marry model theory and combinatory logic.

Summary of lambda calculus

Lambda calculus is concerned with objects called lambda-terms, which can be represented by the following three forms of strings:

• ${\displaystyle v}$
• ${\displaystyle \lambda v.E_{1}}$
• ${\displaystyle (E_{1}E_{2})}$

where ${\displaystyle v}$ is a variable name drawn from a predefined infinite set of variable names, and ${\displaystyle E_{1}}$ and ${\displaystyle E_{2}}$ are lambda-terms.

Terms of the form ${\displaystyle \lambda v.E_{1}}$ are called abstractions. The variable v is called the formal parameter of the abstraction, and ${\displaystyle E_{1}}$ is the body of the abstraction. The term ${\displaystyle \lambda v.E_{1}}$ represents the function which, applied to an argument, binds the formal parameter v to the argument and then computes the resulting value of ${\displaystyle E_{1}}$— that is, it returns ${\displaystyle E_{1}}$, with every occurrence of v replaced by the argument.

Terms of the form ${\displaystyle (E_{1}E_{2})}$ are called applications. Applications model function invocation or execution: the function represented by ${\displaystyle E_{1}}$ is to be invoked, with ${\displaystyle E_{2}}$ as its argument, and the result is computed. If ${\displaystyle E_{1}}$ (sometimes called the applicand) is an abstraction, the term may be reduced: ${\displaystyle E_{2}}$, the argument, may be substituted into the body of ${\displaystyle E_{1}}$ in place of the formal parameter of ${\displaystyle E_{1}}$, and the result is a new lambda term which is equivalent to the old one. If a lambda term contains no subterms of the form ${\displaystyle ((\lambda v.E_{1})E_{2})}$ then it cannot be reduced, and is said to be in normal form.

The expression ${\displaystyle E[v:=a]}$ represents the result of taking the term E and replacing all free occurrences of v in it with a. Thus we write

${\displaystyle ((\lambda v.E)a)\Rightarrow E[v:=a]}$

By convention, we take ${\displaystyle (abc)}$ as shorthand for ${\displaystyle ((ab)c)}$ (i.e., application is left associative).

The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions. For example, consider the function that computes the square of a number. We might write

The square of x is ${\displaystyle x*x}$

(Using "${\displaystyle *}$" to indicate multiplication.) x here is the formal parameter of the function. To evaluate the square for a particular argument, say 3, we insert it into the definition in place of the formal parameter:

The square of 3 is ${\displaystyle 3*3}$

To evaluate the resulting expression ${\displaystyle 3*3}$, we would have to resort to our knowledge of multiplication and the number 3. Since any computation is simply a composition of the evaluation of suitable functions on suitable primitive arguments, this simple substitution principle suffices to capture the essential mechanism of computation. Moreover, in lambda calculus, notions such as '3' and '${\displaystyle *}$' can be represented without any need for externally defined primitive operators or constants. 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. Church encoding.

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. According to the Church-Turing thesis, both models can express any possible computation.

It is perhaps surprising that lambda-calculus can represent any conceivable computation using only the simple notions of function abstraction and application based on simple textual substitution of terms for variables. But even more remarkable is that abstraction is not even required. 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.

Combinatory calculi

Since abstraction is the only way to manufacture functions in the lambda calculus, something must replace it in the combinatory calculus. Instead of abstraction, combinatory calculus provides a limited set of primitive functions out of which other functions may be built.

Undecidability of combinatorial calculus

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. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This is equivalent to the undecidability of the corresponding problems for lambda terms. However, a direct proof is as follows:

First, the term

Ω = (S I I (S I I))

has no normal form, because it reduces to itself after three steps, as follows:

(S I I (S I I))

= (I (S I I) (I (S I I)))

= (S I I (I (S I I)))

= (S I I (S I I))

and clearly no other reduction order can make the expression shorter.

Now, suppose N were a combinator for detecting normal forms, such that

${\displaystyle (\mathbf {N} \ x)={\begin{cases}\mathbf {T} ,{\text{ if }}x{\text{ has a normal form}}\\\mathbf {F} ,{\text{ otherwise.}}\end{cases}}}$

(Where T and F represent the conventional Church encodings of true and false, λx.λy.x and λx.λy.y, transformed into combinatory logic. The combinatory versions have T = K and F = (K I).)

Now let

Z = (C (C (B N (S I I)) Ω) I)

now consider the term (S I I Z). Does (S I I Z) have a normal form? It does if and only if the following do also:

  (S I I Z)

= (I Z (I Z))

= (Z (I Z))

= (Z Z)

= (C (C (B N (S I I)) Ω) I Z) (definition of Z)

= (C (B N (S I I)) Ω Z I)

= (B N (S I I) Z Ω I)

= (N (S I I Z) Ω I)

Now we need to apply N to (S I I Z). Either (S I I Z) has a normal form, or it does not. If it does have a normal form, then the foregoing reduces as follows:

  (N (S I I Z) Ω I)

= (K Ω I) (definition of N)

= Ω

but Ω does not have a normal form, so we have a contradiction. But if (S I I Z) does not have a normal form, the foregoing reduces as follows:

  (N (S I I Z) Ω I)

= (K I Ω I) (definition of N)

= (I I)

= I

which means that the normal form of (S I I Z) is simply I, another contradiction. Therefore, the hypothetical normal-form combinator N cannot exist.

The combinatory logic analogue of Rice's theorem says that there is no complete nontrivial predicate. A predicate is a combinator that, when applied, returns either T or F. A predicate N is nontrivial if there are two arguments A and B such that N A = T and N B = F. A combinator N is complete if NM has a normal form for every argument M. The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.

From this undecidability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is no complete predicate, say EQUAL, such that:

(EQUAL A B) = T if A = B and

(EQUAL A B) = F if A ≠ B.

If EQUAL would exist, then for all A, λx.(EQUAL x A) would have to be a complete non trivial predicate.

Applications

See also

• Applicative computing systems
• B, C, K, W system
• Categorical abstract machine
• Combinatory categorial grammar
• Explicit substitution
• Fixed point combinator
• Graph reduction machine
• Lambda calculus and Cylindric algebra, other approaches to modelling quantification and eliminating variables
• SKI combinator calculus
• Supercombinator
• To Mock a Mockingbird

References

Literature

• Barendregt, Hendrik Pieter (1984). The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103. North Holland. ISBN 0-444-87508-5.
• Cherlin, Edward (1991). "Pure functions in APL and J". Proceedings of the international conference on APL '91 - APL '91. pp. 88–93. doi:10.1145/114054.114065. ISBN 0897914414. S2CID 25802202.
• Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [Foundations of combinatorial logic]. American Journal of Mathematics (in German). The Johns Hopkins University Press. 52 (3): 509–536. doi:10.2307/2370619. JSTOR 2370619.
• Curry, Haskell Brooks; Feys, Robert (1958). Combinatory Logic. Vol. I. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Curry, Haskell Brooks; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Field, Anthony J.; Harrison, Peter G. (1998). Functional Programming. Addison-Wesley. ISBN 0-201-19249-7.
• Goldberg, Mayer (2004). "A construction of one-point bases in extended lambda calculi". Information Processing Letters. 89 (6): 281–286. doi:10.1016/j.ipl.2003.12.005.
• Hindley, J. Roger; Meredith, David (1990). "Principal type-schemes and condensed detachment". Journal of Symbolic Logic. 55 (1): 90–105. doi:10.2307/2274956. JSTOR 2274956. MR 1043546. S2CID 6930576.
• Hindley, J. Roger; Seldin, Jonathan P. (2008) [1986]. Lambda-Calculus and Combinators: An Introduction (2nd ed.). Cambridge University Press. ISBN 9780521898850.
• Lachowski, Łukasz (2018). "On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic". Reports on Mathematical Logic. 2018 (53): 19–42. doi:10.4467/20842589RM.18.002.8835. Retrieved 9 September 2018.
• Paulson, Lawrence C. (1995). Foundations of Functional Programming. University of Cambridge.
• Quine, Willard Van Orman (1960). "Variables explained away". Proceedings of the American Philosophical Society. 104 (3): 343–347. JSTOR 985250. Reprinted as Chapter 23 of Quine (1996)
• Quine, Willard Van Orman (1996) [1960]. "Variables explained away". Selected Logic Papers (Enl. ed., 2. print ed.). Cambridge, Mass.: Harvard University Press. pp. 227–235. ISBN 9780674798373.
• Schönfinkel, Moses (1924). "Über die Bausteine der mathematischen Logik" (PDF). Mathematische Annalen (in German). 92 (3–4): 305–316. doi:10.1007/bf01448013. S2CID 118507515. The article that founded combinatory logic. English translation: Schönfinkel (1967)
• Schönfinkel, Moses (1967) [1924]. Van Heijenoort, Jean (ed.). Über die Bausteine der mathematischen Logik [On the building blocks of mathematical logic]. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Translated by Bauer-Mengelberg, Stefan. Cambridge, MA, USA: Harvard University Press. pp. 355–366. ISBN 978-0674324497. OCLC 503886453.
• Seldin, Jonathan P. (3 March 2008). "The Logic of Curry and Church" (PDF). Retrieved 17 September 2023.
• Smullyan, Raymond (1985). To Mock a Mockingbird And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Knopf. ISBN 0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
• Smullyan, Raymond (1994). Diagonalization and Self-Reference. Oxford logic guides. Vol. 27. Oxford and New York: Oxford University Press. ISBN 978-0198534501. Chapters 17–20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
• Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. Lectures on the Curry–Howard Isomorphism (PDF). Studies in Logic and the Foundations of Mathematics. Vol. 149 (1st ed.). Elsevier. p. 442. ISBN 978-0444520777. Archived from the original (PDF) on 2005-10-16. Retrieved 2017-04-22.
• Tromp, John (2008). "Binary Lambda Calculus and Combinatory Logic" (PDF). In Calude, Cristian S. (ed.). Randomness And Complexity, from Leibniz To Chaitin. World Scientific Publishing Company. Archived from the original (PDF) on 2016-03-04.
• Turner, David A. (1979). "Another Algorithm for Bracket Abstraction". The Journal of Symbolic Logic. 44 (2): 267–270. doi:10.2307/2273733. JSTOR 2273733. S2CID 35835482.
• Wolfengagen, V. E. (2003). Combinatory logic in programming: Computations with objects through examples and exercises (2nd ed.). Moscow: "Center JurInfoR" Ltd. ISBN 5-89158-101-9.
• Wolfram, Stephen (2021). Combinators: A Centennial View. Wolfram Media. ISBN 978-1-57955-043-1. A celebration of the development of combinators, a hundred years after they were introduced by Schönfinkel (1924) (eBook: ISBN 978-1-57955-044-8)

External links

• Stanford Encyclopedia of Philosophy: "Combinatory Logic" by Katalin Bimbó.
• 1920–1931 Curry's block notes.
• Keenan, David C. (2001) "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction."
• Rathman, Chris, "Combinator Birds." A table distilling much of the essence of Smullyan (1985).
• Drag 'n' Drop Combinators. (Java Applet)
• Binary Lambda Calculus and Combinatory Logic.
• Combinatory logic reduction web server
• Wolfram, Stephen (29 April 2020). Combinators: 100-Year Celebration. Wolfram Physics Project on YouTube. Retrieved 26 September 2023.