combinatory logic a branch of formal logic that deals with formal systems designed for the study of certain basic operations for constructing and manipulating functions as rules, i.e. as rules of calculation expressed by definitions. The notion of a function was fundamental in the development of modern formal (or mathematical) logic that was initiated by Frege, Peano, Russell, Hilbert, and others. Frege was the first to introduce a generalization of the mathematical notion of a function to include propositional functions, and he used the general notion for formally representing logical notions such as those of a concept, object, relation, generality, and judgment. Frege’s proposal to replace the traditional logical notions of subject and predicate by argument and function, and thus to conceive predication as functional application, marks a turning point in the history of formal logic. In most modern logical systems, the notation used to express functions, including propositional functions, is essentially that used in ordinary mathematics. As in ordinary mathematics, certain basic notions are taken for granted, such as the use of variables to indicate processes of substitution. Like the original systems for modern formal logic, the systems of combinatory logic were designed to give a foundation for mathematics. But combinatory logic arose as an effort to carry the foundational aims further and deeper. It undertook an analysis of notions taken for granted in the original systems, in particular of the notions of substitution and of the use of variables. In this respect combinatory logic was conceived by one of its founders, H. B. Curry, to be concerned with the ultimate foundations and with notions that constitute a ‘prelogic.’ It was hoped that an analysis of this prelogic would disclose the true source of the difficulties connected with the logical paradoxes. The operation of applying a function to one of its arguments, called application, is a primitive operation in all systems of combinatory logic. If f is a function and x a possible argument, then the result of the application operation is denoted (fx). In mathematics this is usually written f(x), but the notation (fx) is more convenient in combinatory logic. The German logician M. Schönfinkel, who started combinatory logic in 1924, observed that it is not necessary to introduce functions of more than one variable, provided that the idea of a function is enlarged so that functions can be arguments as well as values of other functions. A function F(x,y) is represented with the function f, which when applied to the argument x has, as a value, the function (fx), which, when applied to y, yields F(x,y), i.e. ((fx)y) % F(x,y). It is therefore convenient to omit parentheses with association to the left so that fx1 . . . xn is used for (( . . . (fx1 . . .) xn). Schönfinkel’s main result was to show how to make the class of functions studied closed under explicit definition by introducing two specific primitive functions, the combinators S and K, with the rules Kxy % x, and Sxyz % xz(yz). (To illustrate the effect of S in ordinary mathematical notation, let f and g be functions of two and one arguments, respectively; then Sfg is the function such that Sfgx % f(x,g(x)).) Generally, if a(x1, . . . ,xn) is an expression built up from constants and the variables shown by means of the application operation, then there is a function F constructed out of constants (including the combinators S and K), such that Fx1 . . . xn % a(x1, . . . , xn). This is essentially the meaning of the combinatory completeness of the theory of combinators in the terminology of H. B. Curry and R. Feys, Combinatory Logic (1958); and H. B. Curry, J. R. Hindley, and J. P. Seldin, Combinatory Logic, vol. II (1972). The system of combinatory logic with S and K as the only primitive functions is the simplest equation calculus that is essentially undecidable. It is a type-free theory that allows the formation of the term ff, i.e. self-application, which has given rise to problems of interpretation. There are also type theories based on combinatory logic. The systems obtained by extending the theory of combinators with functions representing more familiar logical notions such as negation, implication, and generality, or by adding a device for expressing inclusion in logical categories, are studied in illative combinatory logic. The theory of combinators exists in another, equivalent form, namely as the type-free l-calculus created by Church in 1932. Like the theory of combinators, it was designed as a formalism for representing functions as rules of calculation, and it was originally part of a more general system of functions intended as a foundation for mathematics. The l-calculus has application as a primitive operation, but instead of building up new functions from some primitive ones by application, new functions are here obtained by functional abstraction. If a(x) is an expression built up by means of application from constants and the variable x, then a(x) is considered to define a function denoted lx.a (x ), whose value for the argument b is a(b), i.e. (lx.a (x))b % a(b). The function lx.a(x) is obtained from a(x) by functional abstraction. The property of combinatory completeness or closure under explicit definition is postulated in the form of functional abstraction. The combinators can be defined using functional abstraction (i.e., K % lx.ly.x and S % lx.ly.lz.xz(yz)), and conversely, in the theory of combinators, functional abstraction can be defined. A detailed presentation of the l-calculus is found in H. Barendregt, The Lambda Calculus, Its Syntax and Semantics (1981). It is possible to represent the series of natural numbers by a sequence of closed terms in the lcalculus. Certain expressions in the l-calculus will then represent functions on the natural numbers, and these l-definable functions are exactly the general recursive functions or the Turing computable functions. The equivalence of l-definability and general recursiveness was one of the arguments used by Church for what is known as Church’s thesis, i.e., the identification of the effectively computable functions and the recursive functions. The first problem about recursive undecidability was expressed by Church as a problem about expressions in the l calculus. The l-calculus thus played a historically important role in the original development of recursion theory. Due to the emphasis in combinatory logic on the computational aspect of functions, it is natural that its method has been found useful in proof theory and in the development of systems of constructive mathematics. For the same reason it has found several applications in computer science in the construction and analysis of programming languages. The techniques of combinatory logic have also been applied in theoretical linguistics, e.g. in so-called Montague grammar. In recent decades combinatory logic, like other domains of mathematical logic, has developed into a specialized branch of mathematics, in which the original philosophical and foundational aims and motives are of little and often no importance. One reason for this is the discovery of the new technical applications, which were not intended originally, and which have turned the interest toward several new mathematical problems. Thus, the original motives are often felt to be less urgent and only of historical significance. Another reason for the decline of the original philosophical and foundational aims may be a growing awareness in the philosophy of mathematics of the limitations of formal and mathematical methods as tools for conceptual clarification, as tools for reaching ‘ultimate foundations.’
See also CHURCH’S THESIS, COMPUTABILITY, PROOF THEORY, RECURSIVE FUNCTION THE – ORY. S.St.