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.^{ [3] } A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
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.^{ [4] } 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,^{ [5] } which reviews the models Dana Scott devised for combinatory logic in the 1960s and 1970s.
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 (Hindley and Meredith 1990). 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 is a variable name drawn from a predefined infinite set of variable names, and and are lambda-terms.
Terms of the form are called abstractions. The variable v is called the formal parameter of the abstraction, and is the body of the abstraction. The term represents the function which, applied to an argument, binds the formal parameter v to the argument and then computes the resulting value of — that is, it returns , with every occurrence of v replaced by the argument.
Terms of the form are called applications. Applications model function invocation or execution: the function represented by is to be invoked, with as its argument, and the result is computed. If (sometimes called the applicand) is an abstraction, the term may be reduced: , the argument, may be substituted into the body of in place of the formal parameter of , 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 then it cannot be reduced, and is said to be in normal form.
The expression represents the result of taking the term E and replacing all free occurrences of v in it with a. Thus we write
By convention, we take as shorthand for (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
(Using "" 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:
To evaluate the resulting expression , 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 '' 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.
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.
A combinatory term has one of the following forms:
Syntax | Name | Description |
---|---|---|
x | Variable | A character or string representing a combinatory term. |
P | Primitive function | One of the combinator symbols I, K, S. |
(M N) | Application | Applying a function to an argument. M and N are combinatory terms. |
The primitive functions are combinators, or functions that, when seen as lambda terms, contain no free variables.
To shorten the notations, a general convention is that , or even , denotes the term . This is the same general convention (left-associativity) as for multiple application in lambda calculus.
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 {x_{1} ... x_{n}}. It is in this way that primitive combinators behave as functions.
The simplest example of a combinator is I, the identity combinator, defined by
for all terms x. Another simple combinator is K, which manufactures constant functions: (Kx) is the function which, for any argument, returns x, so we say
for all terms x and y. Or, following the convention for multiple application,
A third combinator is S, which is a generalized version of application:
S applies x to y after first substituting z into each of them. Or put another way, x is applied to y inside the environment z.
Given S and K, I itself is unnecessary, since it can be built from the other two:
for any term x. Note that although ((S K K) x) = (Ix) for any x, (S K K) itself is not equal to I. We say the terms are extensionally equal. Extensional equality captures the mathematical notion of the equality of functions: that two functions are equal if they always produce the same results for the same arguments. 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 when these ones are applied to enough arguments. There are many ways to implement an identity function; (S K K) and I are among these ways. (S K S) is yet another. We will use the word equivalent to indicate extensional equality, reserving equal for identical combinatorial terms.
A more interesting combinator is the fixed point combinator or Y combinator, which can be used to implement recursion.
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).
This process is also known as abstraction elimination. This definition is exhaustive: any lambda expression will be subject to exactly one of these rules (see Summary of lambda calculus above).
It is related to the process of bracket abstraction, which takes an expression E built from variables and application and produces a combinator expression [x]E in which the variable x is not free, such that [x]E x = E holds. A very simple algorithm for bracket abstraction is defined by induction on the structure of expressions as follows:^{ [6] }
Bracket abstraction induces a translation from lambda terms to combinator expressions, by interpreting lambda-abstractions using the bracket abstraction algorithm.
For example, we will convert the lambda term λx.λy.(yx) to a combinatorial term:
If we apply this combinatorial term to any two terms x and y (by feeding them in a queue-like fashion into the combinator 'from the right') , it reduces as follows:
The combinatory representation, (S (K (S I)) (S (K K) I)) is much longer than the representation as a lambda term, λx.λy.(y x). This is typical. In general, the T[ ] construction may expand a lambda term of length n to a combinatorial term of length Θ(n^{3}) ^{ [7] }.
The T[ ] transformation is motivated by a desire to eliminate abstraction. Two special cases, rules 3 and 4, are trivial: λx.x is clearly equivalent to I, and λx.E is clearly equivalent to (KT[E]) if x does not appear free in E.
The first two rules are also simple: Variables convert to themselves, and applications, which are allowed in combinatory terms, are converted to combinators simply by converting the applicand and the argument to combinators.
It is rules 5 and 6 that are of interest. Rule 5 simply says that to convert a complex abstraction to a combinator, we must first convert its body to a combinator, and then eliminate the abstraction. Rule 6 actually eliminates the abstraction.
λx.(E₁ E₂) is a function which takes an argument, say a, and substitutes it into the lambda term (E₁ E₂) in place of x, yielding (E₁ E₂)[x : = a]. But substituting a into (E₁ E₂) in place of x is just the same as substituting it into both E₁ and E₂, so
By extensional equality,
Therefore, to find a combinator equivalent to λx.(E₁ E₂), it is sufficient to find a combinator equivalent to (Sλx.E₁ λx.E₂), and
evidently fits the bill. E₁ and E₂ each contain strictly fewer applications than (E₁ E₂), so the recursion must terminate in a lambda term with no applications at all—either a variable, or a term of the form λx.E.
The combinators generated by the T[ ] transformation can be made smaller if we take into account the η-reduction rule:
λx.(E x) is the function which takes an argument, x, and applies the function E to it; this is extensionally equal to the function E itself. It is therefore sufficient to convert E to combinatorial form.
Taking this simplification into account, the example above becomes:
This combinator is equivalent to the earlier, longer one:
Similarly, the original version of the T[ ] transformation transformed the identity function λf.λx.(fx) into (S (S (K S) (S (K K) I)) (K I)). With the η-reduction rule, λf.λx.(fx) is transformed into I.
There are one-point bases from which every combinator can be composed extensionally equal to any lambda term. The simplest example of such a basis is {X} where:
It is not difficult to verify that:
Since {K, S} is a basis, it follows that {X} is a basis too. The Iota programming language uses X as its sole combinator.
Another simple example of a one-point basis is:
In fact, there exist infinitely many such bases.^{ [8] }
In addition to S and K, Schönfinkel's paper included two combinators which are now called B and C, with the following reductions:
He also explains how they in turn can be expressed using only S and K:
These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by Curry, and much later by David Turner, whose name has been associated with their computational use. Using them, we can extend the rules for the transformation as follows:
Using B and C combinators, the transformation of λx.λy.(yx) looks like this:
And indeed, (CIxy) does reduce to (yx):
The motivation here is that B and C are limited versions of S. Whereas S takes a value and substitutes it into both the applicand and its argument before performing the application, C performs the substitution only in the applicand, and B only in the argument.
The modern names for the combinators come from Haskell Curry's doctoral thesis of 1930 (see B, C, K, W System). In Schönfinkel's original paper, what we now call S, K, I, B and C were called S, C, I, Z, and T respectively.
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. ^{ [9] }
A distinction must be made between the CL_{K} as described in this article and the CL_{I} calculus. The distinction corresponds to that between the λ_{K} and the λ_{I} calculus. Unlike the λ_{K} calculus, the λ_{I} calculus restricts abstractions to:
As a consequence, combinator K is not present in the λ_{I} calculus nor in the CL_{I} calculus. The constants of CL_{I} are: I, B, C and S, which form a basis from which all CL_{I} terms can be composed (modulo equality). Every λ_{I} term can be converted into an equal CL_{I} combinator according to rules similar to those presented above for the conversion of λ_{K} terms into CL_{K} combinators. See chapter 9 in Barendregt (1984).
The conversion L[ ] from combinatorial terms to lambda terms is trivial:
Note, however, that this transformation is not the inverse transformation of any of the versions of T[ ] that we have seen.
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
has no normal form, because it reduces to itself after three steps, as follows:
and clearly no other reduction order can make the expression shorter.
Now, suppose N were a combinator for detecting normal forms, such that
Now let
now consider the term (SIIZ). Does (SIIZ) have a normal form? It does if and only if the following do also:
Now we need to apply N to (SIIZ). Either (SIIZ) has a normal form, or it does not. If it does have a normal form, then the foregoing reduces as follows:
but Ω does not have a normal form, so we have a contradiction. But if (SIIZ) does not have a normal form, the foregoing reduces as follows:
which means that the normal form of (SIIZ) 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 NA = T and NB = F. A combinator N is complete if and only 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.
Proof: By reductio ad absurdum. Suppose there is a complete non trivial predicate, say N. Because N is supposed to be non trivial there are combinators A and B such that
- (NA) = T and
- (NB) = F.
- Define NEGATION ≡ λx.(if (Nx) then B else A) ≡ λx.((Nx) BA)
- Define ABSURDUM ≡ (Y NEGATION)
Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for
- ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM).
Because N is supposed to be complete either:
- (N ABSURDUM) = F or
- (N ABSURDUM) = T
- Case 1: F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (NA) = T, a contradiction.
- Case 2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (NB) = F, again a contradiction.
Hence (N ABSURDUM) is neither T nor F, which contradicts the presupposition that N would be a complete non trivial predicate. Q.E.D.
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:
If EQUAL would exist, then for all A, λx.(EQUAL x A) would have to be a complete non trivial predicate.
David Turner used his combinators to implement the SASL programming language.
Kenneth E. Iverson used primitives based on Curry's combinators in his J programming language, a successor to APL. This enabled what Iverson called tacit programming, that is, programming in functional expressions containing no variables, along with powerful tools for working with such programs. It turns out that tacit programming is possible in any APL-like language with user-defined operators.^{ [10] }
The Curry–Howard isomorphism implies a connection between logic and programming: every proof of a theorem of intuitionistic logic corresponds to a reduction of a typed lambda term, and conversely. Moreover, theorems can be identified with function type signatures. 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. Consider the set W of all deductively closed sets of formulas, ordered by inclusion. Then is an intuitionistic Kripke frame, and we define a model in this frame by
This definition obeys the conditions on satisfaction of →: on one hand, if , and is such that and , then by modus ponens. On the other hand, if , then by the deduction theorem, thus the deductive closure of is an element such that , , and .
Let A be any formula which is not provable in the calculus. Then A does not belong to the deductive closure X of the empty set, thus , and A is not intuitionistically valid.
Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. Some older books use the terms real variable and apparent variable for free variable and bound variable, respectively. The idea is related to a placeholder, or a wildcard character that stands for an unspecified symbol.
In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function. In combinatory logic for computer science, a fixed-point combinator is a higher-order function that returns some fixed point of its argument function, if one exists.
Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F", requiring only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules proves everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic.
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.
The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930).
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants.
System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).
In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
The SKI combinator calculus is a combinatory logic, a computational system that may be perceived as a reduced version of the untyped lambda calculus. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It was introduced by Moses Schönfinkel and Haskell Curry.
The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor: that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of;
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.
In mathematical logic, the de Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bind variables. Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality. Each De Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:
Combinatory categorial grammar (CCG) is an efficiently parsable, yet linguistically expressive grammar formalism. It has a transparent interface between surface syntax and underlying semantic representation, including predicate-argument structure, quantification and information structure. The formalism generates constituency-based structures and is therefore a type of phrase structure grammar.
In computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not expressed within the calculus. The concept of explicit substitutions has become notorious because the notion often turns up in formal descriptions and implementation of all the mathematical forms of substitution involving variables such as in abstract machines, predicate logic, and symbolic computation.
Computable topology is a discipline in mathematics that studies the topological and algebraic structure of computation. Computable topology is not to be confused with algorithmic or computational topology, which studies the application of computation to topology.
In computer science, a "let" expression associates a function definition with a restricted scope.
Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.
|journal=
(help)