 |
|
| ||||||||||||||||||||||||||
|
|
| ||||||||||||||||||||||||||
|
|
|
|
|
| ||||||||
Combinatory logic is a simplified model of computation, used in computability theory (the study of what can be computed) and proof theory (the study of what can be mathematically proven.) The theory, despite its simplicity, captures many essential features of the nature of computation.
Combinatory logic is a variation of the lambda calculus, in which lambda expressions (used to allow for functional abstraction) are replaced by a limited set of combinators, primitive functions which contain no free variables. It is easy to transform lambda expressions into combinator expressions, and since combinator reduction is much simpler than lambda reduction, it has been used as the basis for the implementation of some non-strict functional programming languages in software and hardware.
For complete details about the lambda calculus, see the article under that head. We will summarize here. The lambda calculus is concerned with objects called lambda-terms, which are strings of symbols of one of the following forms:
where v is a variable name drawn from a predefined infinite set of variable names, and E1 and E2 are lambda-terms. Terms of the form λv.E1 are called abstractions. The variable v is called the normal form.
The expression E[a/v] represents the result of taking the term E and replacing all free occurrences of v with a. Thus we write
By convention, we take (a b c d ... z) as short for (...(((a b) c) d) ... z). (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 Turing machines); that is, any calculuation that can be accomplished in any of these other models can be expressed in the 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 the lambda calculus, but without abstraction.
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:
where V is a variable, P is one of the primitive functions, or E1 and E2 are combinatorial terms. The primitive functions themselves are combinators, or functions that contain no free variables.
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: (K x) is the function which, for any argument, returns x, so we say
for all terms x and y. Or, following the same convention for multiple application as in the lambda-calculus,
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.
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) = (I x) for any x, (S K K) itself is not equal to I. We say the terms are fixed point combinator or Y combinator, which can be used to implement recursion.
It is a perhaps astonishing fact that 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:
For example, we will convert the lambda term λx.λy.(y x)) to a combinator:
If we apply this combinator to any two terms x and y, 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 Θ(3n).
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 (K 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's 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.(E1 E2) is a function which takes an argument, say a, and substitutes it into the lambda term (E1 E2) in place of x, yielding (E1 E2)[a/x]. But substituting a into (E1 E2) in place of x is just the same as substituting it into both E1 and E2, so
By extensional equality,
Therefore, to find a combinator equivalent to λx.(E1 E2), it is sufficient to find a combinator equivalent to (S λx.E1 λx.E2), and
evidently fits the bill. E1 and E2 each contain strictly fewer applications than (E1 E2), 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.(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.
The combinators S and K already figure in the work of Schönfinkel (although symbol C was used instead of present K), Curry introduced the use of B, C, W (and K), already in his doctoral thesis of 1930 (see B,C,K,W System). In Combinatory Logic V. I, we return to S, K but, (via Markov's algorithms) he uses B and C to simplify many reductions. This seems to have been used, much later, by Functional programming languages are often based on the simple but universal semantics of the lambda calculus. (Add details.)
David Turner used his combinators to implement the SASL language.
(Discuss strict vs. lazy evaluation semantics. Note implications of graph reduction implementation for lazy evaluation. Point out efficiency problem in lazy semantics: Repeated evaluation of the same expression, in, e.g. (square COMPLICATED) => (* COMPLICATED COMPLICATED), normally avoided by eager evaluation and call-by-value. Discuss benefit of graph reduction in this case: when (square COMPLICATED) is evaluated, the representation of COMPLICATED can be shared by both branches of the resulting graph for (* COMPLICATED COMPLICATED), and evaluated only once.)
The Curry-Howard isomorphism implies a relationship between logic and programming: Every valid proof of a theorem of logic corresponds directly to a reduction of a lambda term, and vice versa. Theorems themselves are identified with function type signatures. Specifically, typed combinatory logics correspond to Hilbert systems in proof theory.
(Add: Demonstration that the axioms
are complete for the intuitionistic fragment of propositional logic.)
See also:
|
||||
| View Live Article | This article is from Wikipedia. All text is available under the terms of the GNU Free Documentation License | |
||
