| Combinatory Logic |
Website Links For Combinatory Logic |
Information About ™Combinatory Logic |
|
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for Variable s in Mathematical Logic . It 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 are Higher-order Function s that solely use function application and possibly other, earlier defined combinators for defining a result from their arguments. COMBINATORY LOGIC IN MATHEMATICS Combinatory logic was intended as a simple 'pre-logic' which would clarify the meaning of variables in logical notation, and indeed eliminate the need for them. See Curry, 1958-72. COMBINATORY LOGIC IN COMPUTING In computer science, combinatory logic is used as 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 can be looked at as 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 Variable s. 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 . It can also be looked at in a number of other manners, with many early papers showing the equivalence of various combinators to various logic axioms and Meredith, 1990 . SUMMARY OF THE LAMBDA CALCULUS See Also: lambda calculus 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 Formal Parameter of the abstraction, and ''E1'' is the ''body'' of the abstraction. The term ''λv.E1'' represents the function which, applied to an argument, binds the formal parameter ''v'' to the argument and then computes the resulting value of ''E1''---that is, it returns ''E1'', with every occurrence of ''v'' replaced by the argument. Terms of the form ''(E1 E2)'' are called ''applications''. Applications model function invocation or execution: the function represented by ''E1'' is to be invoked, with ''E2'' as its argument, and the result is computed. If ''E1'' (sometimes called the ''applicand'') is an abstraction, the term may be ''reduced'': ''E2'', the argument, may be substituted into the body of ''E1'' in place of the formal parameter of ''E1'', 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 ''(λv.E1 E2)'' then it cannot be reduced, and is said to be in Normal Form . The expression ''E'' := ''a'' represents the result of taking the term ''E'' and replacing all free occurrences of ''v'' with ''a''. Thus we write :(''λv.E'' ''a'') => ''E'' := ''a'' 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
argument, say 3, we insert it into the definition in place of the formal parameter:
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.
represented without any need for externally defined primitive operators or constants. It is possible to identify terms in the lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator. The lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including Turing Machine s); that is, any calculation 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. 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:
where ''v'' is a variable, ''P'' is one of the primitive functions, and ''E1'' and ''E2'' are combinatory terms. The primitive functions themselves are ''combinators'', or functions that contain no Free Variable s. 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 same convention for multiple application as in the lambda-calculus, :(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. 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 capture the notion of ''intensional equality'' of functions: that two functions are 'equal' only if they have identical implementations. 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 . Completeness of the S-'''K''' basis 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'' {Link without Title} , which converts an arbitrary lambda term into an equivalent combinator. ''T'' {Link without Title} may be defined as follows: # ''T'' {Link without Title} => ''V'' # ''T'' ''E2'') => (''T'' ''T''[''E2'' ) # ''T''[''λx''.''E''] => (K ''T''[''E'']) (if ''x'' is not free in ''E'') # ''T'' {Link without Title} => I # ''T''[''λx''.''λy''.''E''] => ''T'' # ''T'' ''E2'') => (S ''T'' ''T''[''λx''.''E2'' ) Conversion of a lambda term to an equivalent combinatorial term For example, we will convert the lambda term ''λx''.''λy''.(''y'' ''x'') to a combinator: T :: = ''T'' :: = ''T'' S" class="copylinks" target="_blank">''T''[''λy''.''y'' ''T''[''λy''.''x''])] (by 6) :: = ''T'' S" class="copylinks" target="_blank">'''I''' ''T''[''λy''.''x'' )] (by 4) :: = ''T'' S" class="copylinks" target="_blank">'''I''' ('''K''' ''x'')) (by 3) :: = (S ''T'' S" class="copylinks" target="_blank">'''I''') ''T'' ''x'') ) (by 6) :: = (S ('''K''' (S '''I''')) ''T'' ''x'') ) (by 3) :: = (S ('''K''' (S '''I''')) (S ''T'' ''T''[''λx''.''x'' )) (by 6) :: = (S ('''K''' (S '''I''')) (S ('''K''' '''K''') ''T'' {Link without Title} )) (by 3) :: = (S ('''K''' (S '''I''')) (S ('''K''' '''K''') '''I''')) (by 4) If we apply this combinator to any two terms ''x'' and ''y'', 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'' {Link without Title} construction may expand a lambda term of length ''n'' to a combinatorial term of length Θ (3''n''). Explanation of the ''T'' {Link without Title} transformation The ''T'' {Link without Title} 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'' . But substituting ''a'' into (''E1'' ''E2'') in place of ''x'' is just the same as substituting it into both ''E1'' and ''E2'', so (''E1'' ''E2'') := ''a'' = (''E1'' := ''a'' ''E2'' := ''a'' ) (''λx''.(''E1'' ''E2'') ''a'') = ((''λx''.''E1'' ''a'') (''λx''.''E2'' ''a'')) = (S ''λx''.''E1'' ''λx''.''E2'' ''a'') = ((S ''λx''.''E1'' ''λx''.''E2'') ''a'') By extensional equality, ''λx''.(''E1'' ''E2'') = (S ''λx''.''E1'' ''λx''.''E2'') 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 (S ''T'' ''T''[''λx''.''E2'' ) 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''. Simplifications of the transformation η-reduction The combinators generated by the T {Link without Title} transformation can be made smaller if we take into account the ''η-reduction'' rule: ''T'' ''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'') = ... = (S ('''K''' (S '''I''')) ''T'' ''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 {Link without Title} 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. Combinators B, C of Curry 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 David Turner , whose name has been bound to its computational use. Two new combinators are introduced: (C ''a'' ''b'' ''c'') = (''a'' ''c'' ''b'') (B ''a'' ''b'' ''c'') = (''a'' (''b'' ''c'')) Using these combinators, we can extend the rules for the transformation as follows: # ''T'' {Link without Title} => ''V'' # ''T'' ''E2'') => (''T'' ''T''[''E2'' ) # ''T''[''λx''.''E''] => (K ''T''[''E'']) (if ''x'' is not free in ''E'') # ''T'' {Link without Title} => I # ''T''[''λx''.''λy''.''E''] => ''T'' # ''T'' ''E2'') => (S ''T'' ''T''[''λx''.''E2'' ) (if ''x'' is free in both ''E1'' and ''E2'') # ''T'' ''E2'') => (C ''T''[''λx''.''E1''] ''E2'') (if ''x'' is free in ''E1'' but not ''E2'') # ''T'' ''E2'') => (B ''E1'' ''T''[''λx''.''E2'']) (if ''x'' is free in ''E2'' but not ''E1'') Using B and '''C''' combinators, the transformation of ''λx''.''λy''.(''y'' ''x'') looks like this: ''T'' ''x'') = ''T'' = ''T'' C" class="copylinks" target="_blank">''T''[''λy''.''y'' ''x'')] (by rule 7) = ''T'' C" class="copylinks" target="_blank">'''I''' ''x'') = (C '''I''') (η-reduction)
= I'(traditional canonical notation: '''X'''' = '''C''' '''X''') 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. Reverse conversion The conversion ''L'' {Link without Title} from combinatorial terms to lambda terms is trivial: ''L'' I" class="copylinks" target="_blank">{Link without Title} = ''λx''.''x'' ''L'' K" class="copylinks" target="_blank">{Link without Title} = ''λx''.''λy''.''x'' ''L'' C" class="copylinks" target="_blank">{Link without Title} = ''λx''.''λy''.''λz''.(''x'' ''z'' ''y'') ''L'' B" class="copylinks" target="_blank">{Link without Title} = ''λx''.''λy''.''λz''.(''x'' (''y'' ''z'')) ''L'' S" class="copylinks" target="_blank">{Link without Title} = ''λx''.''λy''.''λz''.(''x'' ''z'' (''y'' ''z'')) ''L'' ''E2'') = (''L'' ''L''[''E2'' ) Note, however, that this transformation is not the inverse transformation of any of the versions of T {Link without Title} that we have seen. UNDECIDABILITY OF COMBINATORIAL CALCULUS 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, observe that 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 (N ''x'') => '''T''', if ''x'' has a normal form F, otherwise. (Where T and '''F''' the transformations of the conventional lambda-calculus definitions of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y''. 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. COMBINATORY TERMS AS GRAPHS (TO DO: Add details with illustrations; don't forget to discuss the effect of fixed-point combinators.) APPLICATIONS Compilation of functional languages Functional Programming Language s are often based on the simple but universal semantics of the lambda calculus. (Add details.) David Turner used his combinators to implement the SASL Programming 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
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
COMPLICATED), and evaluated only once.) Logic 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 System s in Proof Theory . (Add: Demonstration that the proof system (a -> (b -> a)) (a -> (b -> c)) -> ((a -> b) -> (a -> c)) a, a -> b / b is complete for the intuitionistic fragment of propositional logic.) SEE ALSO
REFERENCES
|