HOME

TheInfoList



OR:

Combinatory logic is a notation to eliminate the need for quantified variables in
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal s ...
. It was introduced by
Moses Schönfinkel Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic. Life Mose ...
and Haskell Curry, and has more recently been used in
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
as a theoretical
model of computation In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how an output of a mathematical function is computed given an input. A model describes ...
and also as a basis for the design of
functional programming languages In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
. 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 First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quant ...
. A combinator is a
higher-order function In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following: * takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itsel ...
that uses only
function application In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range. In this sense, function application can be thought of as the opposite of function abstr ...
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 In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic (also known as predicate logic) by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices ...
. While the expressive power of combinatory logic typically exceeds that of
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quant ...
, the expressive power of
predicate functor logic In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic (also known as predicate logic) by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices ...
is identical to that of first order logic ( Quine 1960, 1966, 1976). The original inventor of combinatory logic,
Moses Schönfinkel Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic. Life Mose ...
, published nothing on combinatory logic after his original 1924 paper. Haskell Curry rediscovered the combinators while working as an instructor at
Princeton University Princeton University is a private research university in Princeton, New Jersey. Founded in 1746 in Elizabeth as the College of New Jersey, Princeton is the fourth-oldest institution of higher education in the United States and one of the ...
in late 1927. In the late 1930s,
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer sc ...
and his students at Princeton invented a rival formalism for functional abstraction, the
lambda calculus Lambda calculus (also written as ''λ''-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 t ...
, 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 Robert Feys (19 December 1889 – 13 April 1961) was a Belgian logician and philosopher, who worked at the University of Leuven (Belgium).De Raeymaeker, Louis.In memoriam le chanoine Robert Feys" ''Revue Philosophique de Louvain'' 59.62 (1961): 37 ...
in
Belgium Belgium, ; french: Belgique ; german: Belgien officially the Kingdom of Belgium, is a country in Northwestern Europe. The country is bordered by the Netherlands to the north, Germany to the east, Luxembourg to the southeast, France to the ...
. 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, which reviews the models
Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
devised for combinatory logic in the 1960s and 1970s.


In computing

In
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, combinatory logic is used as a simplified model of
computation Computation is any type of arithmetic or non-arithmetic calculation that follows a well-defined model (e.g., an algorithm). Mechanical or electronic devices (or, historically, people) that perform computations are known as '' computers''. An es ...
, used in
computability theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ...
and
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...
. Despite its simplicity, combinatory logic captures many essential features of computation. Combinatory logic can be viewed as a variant of the
lambda calculus Lambda calculus (also written as ''λ''-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 t ...
, in which lambda expressions (representing functional abstraction) are replaced by a limited set of ''combinators'', primitive functions without
free variable 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 ...
s. 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 In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
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 Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
in the 1960s and 1970s showed how to marry
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the ...
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: * * * 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 and replacing all free occurrences of in it with . 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 :The square of ''x'' is (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: :The square of 3 is 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 In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded ...
. Lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algo ...
s); 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.


Combinatory terms

A combinatory term has one of the following forms: The primitive functions are ''combinators'', or functions that, when seen as lambda terms, contain no
free variable 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 ...
s. 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.


Reduction in combinatory logic

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 . It is in this way that primitive combinators behave as functions.


Examples of combinators

The simplest example of a combinator is I, the identity combinator, defined by :(I ''x'') = ''x'' for all terms ''x''. Another simple combinator is K, which manufactures constant functions: (K ''x'') is the function which, for any argument, returns ''x'', so we say :((K ''x'') ''y'') = ''x'' for all terms ''x'' and ''y''. Or, following the convention for multiple application, :(K ''x'' ''y'') = ''x'' A third combinator is S, which is a generalized version of application: :(S ''x y z'') = (''x z'' (''y z'')) 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: :((S K K) ''x'') :: = (S K K ''x'') :: = (K ''x'' (K ''x'')) :: = ''x'' for any term ''x''. Note that although ((S K K) ''x'') = (I ''x'') 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 Two mathematical objects ''a'' and ''b'' are called equal up to an equivalence relation ''R'' * if ''a'' and ''b'' are related by ''R'', that is, * if ''aRb'' holds, that is, * if the equivalence classes of ''a'' and ''b'' with respect to ''R'' a ...
the expansion of primitive combinators. 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 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 (or fixpoint combinator) is a higher-order fu ...
or Y combinator, which can be used to implement
recursion Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...
.


Completeness of the S-K basis

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''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
which converts an arbitrary lambda term into an equivalent combinator. ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
may be defined as follows: # ''T'' 'x'' => ''x'' # ''T'' ''E''₁ ''E''₂) => (''T'' 'E''₁''T'' 'E''₂ # ''T'' 'λx''.''E'' => (K ''T'' 'E'' (if ''x'' does not occur free in ''E'') # ''T'' 'λx''.''x'' => I # ''T'' 'λx''.''λy''.''E'' => ''T'λx''.''T'λy''.''E'' (if ''x'' occurs free in ''E'') # ''T'' 'λx''.(''E''₁ ''E''₂)=> (S ''T'' 'λx''.''E''₁''T'' 'λx''.''E₂'' (if ''x'' occurs free in ''E''₁ or ''E''₂) Note that ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
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 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: # 'x'''y'' := K ''y'' # 'x'''x'' := I # 'x''''E₁'' ''E₂'') := S( 'x'''E₁'')( 'x'''E₂'') Bracket abstraction induces a translation from lambda terms to combinator expressions, by interpreting lambda-abstractions using the bracket abstraction algorithm.


Conversion of a lambda term to an equivalent combinatorial term

For example, we will convert the lambda term ''λx''.''λy''.(''y'' ''x'') to a combinatorial term: :''T'' 'λx''.''λy''.(''y'' ''x''):: = ''T'λx''.''T'λy''.(''y'' ''x'') (by 5) :: = ''T'' 'λx''.(S_''T''[''λy''.''y''''T''[''λy''.''x''.html" ;"title="'λy''.''y''.html" ;"title="'λx''.(S ''T''[''λy''.''y''">'λx''.(S ''T''[''λy''.''y''''T''[''λy''.''x''">'λy''.''y''.html" ;"title="'λx''.(S ''T''[''λy''.''y''">'λx''.(S ''T''[''λy''.''y''''T''[''λy''.''x''] (by 6) :: = ''T''[''λx''.(S I ''T''[''λy''.''x''])] (by 4) :: = ''T''[''λx''.(S I (K ''T''[''x'']))] (by 3) :: = ''T''[''λx''.(S I (K ''x''))] (by 1) :: = (S ''T'' 'λx''.(S I)''T'' 'λx''.(K ''x'') (by 6) :: = (S (K (S I)) ''T'' 'λx''.(K ''x'') (by 3) :: = (S (K (S I)) (S ''T'' 'λx''.K''T'' 'λx''.''x'') (by 6) :: = (S (K (S I)) (S (K K) ''T'' 'λx''.''x'') (by 3) :: = (S (K (S I)) (S (K K) I)) (by 4) 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: : (S (K (S I)) (S (K K) I) x y) :: = (K (S I) x (S (K K) I x) y) :: = (S I (S (K K) I x) y) :: = (I y (S (K K) I x y)) :: = (y (S (K K) I x y)) :: = (y (K K x (I x) y)) :: = (y (K (I x) y)) :: = (y (I x)) :: = (y x) 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''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
construction may expand a lambda term of length ''n'' to a combinatorial term of length Θ(''n''3).


Explanation of the ''T''

nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
transformation

The ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
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 (K ''T'' '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 : (''E''₁ ''E''₂) 'x'' := ''a''= (''E''₁ 'x'' := ''a''''E''₂ 'x'' := ''a'' : (''λx''.(''E''₁ ''E''₂) ''a'') = ((''λx''.''E''₁ ''a'') (''λx''.''E''₂ ''a'')) ::::: = (S ''λx''.''E''₁ ''λx''.''E''₂ ''a'') ::::: = ((S ''λx''.''E₁'' ''λx''.''E''₂) ''a'') By extensional equality, : ''λx''.(''E''₁ ''E''₂) = (S ''λx''.''E''₁ ''λx''.''E''₂) 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 : (S ''T'' 'λx''.''E''₁''T'' 'λx''.''E''₂ 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''.


Simplifications of the transformation


η-reduction

The combinators generated by the ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
transformation can be made smaller if we take into account the ''η-reduction'' rule: : ''T'' 'λx''.(''E'' ''x'')= ''T'' 'E'' (if ''x'' is not free in ''E'') ''λ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: :  ''T'' 'λx''.''λy''.(''y'' ''x''): = ... : = (S (K (S I)) ''T'' 'λx''.(K ''x'') : = (S (K (S I)) K) (by η-reduction) This combinator is equivalent to the earlier, longer one: :  (S (K (S I)) K ''x y'') : = (K (S I) ''x'' (K ''x'') ''y'') : = (S I (K ''x'') ''y'') : = (I ''y'' (K ''x y'')) : = (''y'' (K ''x y'')) : = (''y x'') Similarly, the original version of the ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
transformation transformed the identity function ''λf''.''λx''.(''f'' ''x'') into (S (S (K S) (S (K K) I)) (K I)). With the η-reduction rule, ''λf''.''λx''.(''f'' ''x'') is transformed into I.


One-point basis

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 where: : X ≡ ''λx''.((xS)K) It is not difficult to verify that: : X (X (X X)) =β K and : X (X (X (X X))) =β S. Since is a basis, it follows that is a basis too. The
Iota Iota (; uppercase: Ι, lowercase: ι; ) is the ninth letter of the Greek alphabet. It was derived from the Phoenician letter Yodh. Letters that arose from this letter include the Latin I and J, the Cyrillic І (І, і), Yi (Ї, ї), an ...
programming language uses X as its sole combinator. Another simple example of a one-point basis is: : X' ≡ ''λx''.(x K S K) with : (X' X') X' =β K and : X' (X' X') =β S In fact, there exist infinitely many such bases.


Combinators B, C

In addition to S and K, Schönfinkel's paper included two combinators which are now called B and C, with the following reductions: : (C ''f'' ''g'' ''x'') = ((''f'' ''x'') ''g'') : (B ''f'' ''g'' ''x'') = (''f'' (''g'' ''x'')) He also explains how they in turn can be expressed using only S and K: : B = (S (K S) K) : C = (S (S (K (S (K S) K)) S) (K K)) These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by
Curry A curry is a dish with a sauce seasoned with spices, mainly associated with South Asian cuisine. In southern India, leaves from the curry tree may be included. There are many varieties of curry. The choice of spices for each dish in trad ...
, 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: # ''T'' 'x'' ⇒ ''x'' # ''T'' ''E₁'' ''E₂'') ⇒ (''T'' 'E₁''''T'' 'E₂'' # ''T'' 'λx''.''E'' ⇒ (K ''T'' 'E'' (if ''x'' is not free in ''E'') # ''T'' 'λx''.''x'' ⇒ I # ''T'' 'λx''.''λy''.''E'' ⇒ ''T'λx''.''T'λy''.''E'' (if ''x'' is free in ''E'') # ''T'' 'λx''.(''E₁'' ''E₂'')⇒ (S ''T'' 'λx''.''E₁''''T'' 'λx''.''E₂'' (if ''x'' is free in both ''E₁'' and ''E₂'') # ''T'' 'λx''.(''E₁'' ''E₂'')⇒ (C ''T'' 'λx''.''E₁''''T'' 'E₂'' (if ''x'' is free in ''E₁'' but not ''E₂'') # ''T'' 'λx''.(''E₁'' ''E₂'')⇒ (B ''T'' 'E₁''''T'' 'λx''.''E₂'' (if ''x'' is free in ''E₂'' but not ''E₁'') Using B and C combinators, the transformation of ''λx''.''λy''.(''y'' ''x'') looks like this: :   ''T'' 'λx''.''λy''.(''y'' ''x''): = ''T'λx''.''T'λy''.(''y'' ''x'') : = ''T'' 'λx''.(C_''T''[''λy''.''y''''x'').html" ;"title="'λy''.''y''.html" ;"title="'λx''.(C ''T''[''λy''.''y''">'λx''.(C ''T''[''λy''.''y''''x'')">'λy''.''y''.html" ;"title="'λx''.(C ''T''[''λy''.''y''">'λx''.(C ''T''[''λy''.''y''''x'') (by rule 7) : = ''T''[''λx''.(C I ''x'')] : = (C I) (η-reduction) : = \mathbf_ (traditional canonical notation : \mathbf_ = \mathbf) : = \mathbf' (traditional canonical notation: \mathbf' = \mathbf) And indeed, (C I ''x'' ''y'') does reduce to (''y'' ''x''): :   (C I ''x'' ''y'') : = (I ''y'' ''x'') : = (''y'' ''x'') 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.


= CLK versus CLI calculus

= A distinction must be made between the CLK as described in this article and the CLI calculus. The distinction corresponds to that between the λK and the λI calculus. Unlike the λK calculus, the λI calculus restricts abstractions to: ::''λx''.''E'' where ''x'' has at least one free occurrence in ''E''. As a consequence, combinator K is not present in the λI calculus nor in the CLI calculus. The constants of CLI are: I, B, C and S, which form a basis from which all CLI terms can be composed (modulo equality). Every λI term can be converted into an equal CLI combinator according to rules similar to those presented above for the conversion of λK terms into CLK combinators. See chapter 9 in Barendregt (1984).


Reverse conversion

The conversion ''L''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
from combinatorial terms to lambda terms is trivial: : ''L'' ''I = ''λx''.''x'' : ''L'' ''K = ''λx''.''λy''.''x'' : ''L'' ''C = ''λx''.''λy''.''λz''.(''x'' ''z'' ''y'') : ''L'' ''B = ''λx''.''λy''.''λz''.(''x'' (''y'' ''z'')) : ''L'' ''S = ''λx''.''λy''.''λz''.(''x'' ''z'' (''y'' ''z'')) : ''L'' ''E₁'' ''E₂'')= (''L'' 'E₁''''L'' 'E₂'' Note, however, that this transformation is not the inverse transformation of any of the versions of ''T''
nbsp; In word processing and digital typesetting, a non-breaking space, , also called NBSP, required space, hard space, or fixed space (though it is not of fixed width), is a space character that prevents an automatic line break at its position. In ...
that we have seen.


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 :(\mathbf \ x) = \begin \mathbf, \text x \text \\ \mathbf, \text \end :(Where and represent the conventional
Church encoding In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded ...
s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic. The combinatory versions have and .) 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 In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, does the program terminate for all inputs), unlike a synt ...
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 N''M'' 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


Compilation of functional languages

David Turner used his combinators to implement the
SASL programming language SASL (from St Andrews Static Language, alternatively St Andrews Standard Language) is a purely functional programming language developed by David Turner at the University of St Andrews (Aien aristeuein) , motto_lang = grc , m ...
. Kenneth E. Iverson used primitives based on Curry's combinators in his
J programming language The J programming language, developed in the early 1990s by Kenneth E. Iverson and Roger Hui, is an array programming language based primarily on APL (also by Iverson). To avoid repeating the APL special-character problem, J uses only the basi ...
, 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.


Logic

The Curry–Howard isomorphism implies a connection between logic and programming: every proof of a theorem of
intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
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 mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C*-algebra.'' In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductiv ...
in
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...
. The K and S combinators correspond to the axioms :AK: ''A'' → (''B'' → ''A''), :AS: (''A'' → (''B'' → ''C'')) → ((''A'' → ''B'') → (''A'' → ''C'')), and function application corresponds to the detachment (modus ponens) rule :MP: from ''A'' and ''A'' → ''B'' infer ''B''. 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 \langle W,\subseteq\rangle is an intuitionistic Kripke frame, and we define a model \Vdash in this frame by :X\Vdash A\iff A\in X. This definition obeys the conditions on satisfaction of →: on one hand, if X\Vdash A\to B, and Y\in W is such that Y\supseteq X and Y\Vdash A, then Y\Vdash B by modus ponens. On the other hand, if X\not\Vdash A\to B, then X,A\not\vdash B by the
deduction theorem In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
, thus the deductive closure of X\cup\ is an element Y\in W such that Y\supseteq X, Y\Vdash A, and Y\not\Vdash B. 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 X\not\Vdash A, and ''A'' is not intuitionistically valid.


See also

*
Applicative computing systems Applicative computing systems, or ACS are the systems of object calculi founded on combinatory logic and lambda calculus. The only essential notion which is under consideration in these systems is the representation of object. In combinatory logic ...
* B, C, K, W system *
Categorical abstract machine The categorical abstract machine (CAM) is a model of computation for programs''Cousineau G., Curien P.-L., Mauny M.'' The categorical abstract machine. — LNCS, 201, Functional programming languages computer architecture.-- 1985, pp.~50-64. that ...
* Combinatory categorial grammar *
Explicit substitution 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 ...
*
Fixed point combinator 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 (or fixpoint combinator) is a higher-order fu ...
* Graph reduction machine *
Lambda calculus Lambda calculus (also written as ''λ''-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 t ...
and
Cylindric algebra In mathematics, the notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of first-order logic with equality. This is comparable to the role Boolean algebras play for propositional logic. Cylindric algebra ...
, other approaches to modelling quantification and eliminating variables * SKI combinator calculus * Supercombinator * '' To Mock a Mockingbird''


References


Further reading

* * * * * * * * Reprinted as Chapter 23 of Quine's ''Selected Logic Papers'' (1966), pp. 227–235 * Schönfinkel, Moses, 1924,
Über die Bausteine der mathematischen Logik
" translated as "On the Building Blocks of Mathematical Logic" in ''From Frege to Gödel: a source book in mathematical logic, 1879–1931'',
Jean van Heijenoort Jean Louis Maxime van Heijenoort (; July 23, 1912 – March 29, 1986) was a historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and an American Trotskyist until 1947. Life Van Heijenoort was born ...
, ed.
Harvard University Press Harvard University Press (HUP) is a publishing house established on January 13, 1913, as a division of Harvard University, and focused on academic publishing. It is a member of the Association of American University Presses. After the retir ...
, 1967. . The article that founded combinatory logic. * Smullyan, Raymond, 1985. '' To Mock a Mockingbird''. Knopf. . A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors. * ______, 1994. ''Diagonalization and Self-Reference''.
Oxford University Press Oxford University Press (OUP) is the university press of the University of Oxford. It is the largest university press in the world, and its printing history dates back to the 1480s. Having been officially granted the legal right to print books ...
. Chapters 17–20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results. * Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999.
Lectures on the Curry–Howard Isomorphism
'.
University of Copenhagen The University of Copenhagen ( da, Københavns Universitet, KU) is a prestigious public research university in Copenhagen, Denmark. Founded in 1479, the University of Copenhagen is the second-oldest university in Scandinavia after Uppsala Un ...
and
University of Warsaw The University of Warsaw ( pl, Uniwersytet Warszawski, la, Universitas Varsoviensis) is a public university in Warsaw, Poland. Established in 1816, it is the largest institution of higher learning in the country offering 37 different fields of ...
, 1999. * * e. A celebration of the development of combinators, a hundred years after they were introduced by
Moses Schönfinkel Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic. Life Mose ...
in 1920.


External links

*
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. ...
:
Combinatory Logic
by Katalin Bimbó.
1920–1931 Curry's block notes.
*Keenan, David C. (2001)

*Rathman, Chris, " ttp://www.angelfire.com/tx4/cus/combinator/birds.html 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
{{authority control
Combinatory logic Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comp ...
Lambda calculus Logic in computer science