Combinatory logic
Combinatorial logic ( abbreviated CL for engl. Combinatory Logic ) is a notation that was introduced by Moses Haskell Brooks Curry Schönfinkel and to avoid the use of variables in mathematical logic. It is especially used in computer science as a theoretical model for calculation, as well as the basis for the design of functional programming languages .
- 4.5.1 η - reduction
- 4.5.2 The combinators B, C Curry
- 6.1 Compilation of Functional Programming Languages
Combinatorial logic in mathematics
Combinatorial logic was intended as a simple logic, which should clarify the meaning of quantified variables in the notation of logic and make them actually unnecessary.
See Curry, 1958-72.
Combinatorial Logic in computer science
In computer science, the combinatorial logic is used as a simple model of a calculation. This is required in computability theory and proof theory. In fact, the combinatorial logic captures many aspects of natural computation.
One can conceive of combinational logic as a variation of the lambda - calculus, where the terms of the lambda calculus are replaced by a few combinators. Combiners are primitive functions, which contain no free variables. Since it is very easy to convert lambda expressions in terms of the CL, and the reduction of combinators much simpler than the lambda reduction, CL is often used as an implementation basis for non- strict languages.
You can see the CL in many other ways to consider so many earlier treatises show the equivalence of various combinators axioms of logic. [ Hindley and Meredith, 1990].
A brief summary of the lambda calculus
A detailed description of the lambda - calculus can be found under the article. Lambda terms consist of
- Variables v,
- Abstractions λv.T,
- Applications ( T1 T2)
Where v here T1 and T2 in turn stand for any variable name and T, for lambda terms. Lambda terms can be simplified by beta- reduction, with the application ( λv.E a) is replaced by the replacement E [ v: = a].
Combinatorial logic is a computational model that is equivalent to the lambda calculus, but does not require the abstraction.
The combinatorial calculus
Since abstraction is used in the lambda calculus to model functions, there must be something similar in the combinatorial calculus. There is instead the abstraction a few primitive functions ( combinators ), from which other functions can be composed now.
Combinatorial Terme
Combinatorial terms consist of
- Combinators P
- Applications ( T1 T2)
T1 and T2 are in turn combinatorial terms. The application is, as in the lambda calculus, left-associative, ie T1 T2 T3 T4 is equivalent to ((( T1 T2) T3) T4).
Examples of combinators
X, y, etc. denote the following arbitrary terms.
The simplest combinator is I, the Identitätskombinator. For him, the following applies:
Another, simpler combiner is K, the Konstantenkombinator: (K x) then modeled a function that always returns x for a further argument, thus:
A third combiner is S, it represents a generalized version of the application:
S applies x on y, except that before z in both a.
I is actually unnecessary, if one S and K, as
Note: While it is true ( (SKK) x ) = (I x) for all x, but (SKK) not reducible to I. This is called extensional equality.
Fixpunktkombinator
Even more interesting is the Fixpunktkombinator Y, which is used to implement recursion.
Also Y is unnecessary. It may, if no typing is required, as
Are shown.
Completeness of the basis S- K
It is amazing that you can only consist of S and K combinators that are extensionally equal to any lambda term, and therefore, according to the thesis of Church, extensional equal to any computable function. As evidence serves a transformation T [], which transforms lambda terms in a CL- term equivalents. The only requirement is that to be transformed lambda term contains no free variables.
T [ ] can be defined as follows
The transformation of a lambda expression to a CL- term
We try, for example, the term λx.λy. ( yx ) translate into a CL- Term:
If we now apply this x and y combinator on two terms, the reduction is as follows:
The combinatorial representation (S ( K (SI )) ( S ( KK) I) ) is much longer than the lambda term λx.λy. ( yx ). This is typical for the transformation. In general it may happen that a T [] structure in a lambda expression of length n converts Θ (3n ) into a combiner length.
Explanation of T [] transform
The motivation of the T [] transformation is the elimination of abstractions. Three of the rules are trivial: Rule 4 λx.x transformed into its unique equivalence I, Rule 3 λx.E transformed to (KT [E ] ), but this only works if the bound variable x is not used in E ( ie: in e is not free ). Rule 2 transforms the application of two terms, which is also allowed in the terms of the CL.
Rule 1 is kind of difficult because it converts variables: Variables can only be resolved by Rule 4, so it'll stay for now obtained. Since there are no free variables in the overall term, and each transformation of abstractions, the bound variables considered ( rules 3,4,5,6 ), all variables are eventually resolved.
Rules 5 and 6 move the abstractions until they can be resolved by rule 4 inside the function body. Rule 5 is converted to the first body of the outer abstraction, then the abstraction itself Rule 6 distributes the abstraction via an application on their subterms:
? x. (E1 E2) is a function which takes an argument and the lambda expression (E1 E2 ) are used for x. This is exactly what the combiner S, only for functions E1 [ x] and E2 [ x]:
Therefore applies, in accordance with extensional equality:
. To find such a combiner for? X (E1 E2), it is sufficient for a combiner (S λx.E1 λx.E2 ) to find, so:
Simplification of the transformation
η - reduction
The combinators that delivers T [] will be shorter if we use the η - reduction in the lambda calculus:
T [? X. (E x) ] = T [ e ] ( only if x is not free in E) [. [? x (S x )]] is the function which takes an argument x, and uses the function E; this is extensionally equal to the E function itself Therefore, it is sufficient simply to transform E into its combinatorial form.
With this simplification, the above example becomes:
This combiner is ( extensionally ) equal to the longer of the previous example:
Similarly, the normal T [] would transform the identity function λf.λx. ( fx) transform into (S ( S ( KS) (S ( KK) I) ) ( KI ) ). With the new η - reduction rule is from λf.λx. ( fx) just I.
The combinators B, C Curry
The combinators S and K appear already in the work of Schönfinkel on (though there was K C), Curry led his dissertation Fundamentals of combinational logic continues to B, C, W ( and K). B and C can simplify many reductions, they are as follows:
For these two combinators, the rules are extended as follows:
For example, the transformation of λx.λy. ( yx ) looks like this:
In fact, reduced (C x I y) (y x):
( I x C y) = ( I y x) = (Y x) B and C represent restricted versions of S. In S While a value in both the applicants has as well as in the argument begins, C sets this only in the applicants has and B only in the argument.
Reverse transformation
The transformation L [ ] of CL -terms in lambda terms is easy because we have all the possibilities in the lambda calculus that are also in the CL are available:
But it is important to know that this is the inverse transformation of T [] transformation is not, since T [L [x] ] Although extensional equal to x, but the term is not necessarily obtained.
Undecidability of the combinatorial calculus
It is undecidable whether a general combiner has a normal form if two combinators are equal, etc. This follows already from the similarity to the lambda calculus, but here again a direct proof:
The term
Has no normal form, since it reduces to three steps back to yourself:
And there can be no other way of making the combiner shorter.
N is now a combiner, which tests to normal shape, so that
(T and F are the corresponding combinators here to true and false from the lambda calculus:
)
Now let
Z = (C (C (B N (S I I) ) Ω ) I) Let's examine the term ( S I I Z). Has (S I I Z ) is a normal form? If yes, the following derivations must have a normal form:
Now we turn north on (S I I Z). Either ( SIIZ ) a normal form or not. If so, then would be:
(N (S I I Z ) Ω I) = (K Ω I) (definition of N ) = Ω but Ω has no normal form, so this leads to a contradiction. If ( SIIZ ) has no normal form, the term is reduced as follows:
(N (S I I Z ) Ω I) = ( KI Ω I) (definition of N ) = (I i) I which means that ( SIIZ ) is simply I, so again a contradiction. Therefore, there can be no such N combiner.
Areas of application
Compilation of functional programming languages
Functional programming languages are often based on the simple but universal semantics of the lambda calculus.
David Turner used CL for the language SASL.
Credentials
- "On the building blocks of mathematical logic," Moses Schönfinkel, 1924, translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879-1931, ed Jean van Heijenoort, Harvard University Press, 1977 ISBN 0-674-32449-8. - The original publication on combinatorial logic.
- Combinatory Logic.. Curry, Haskell B. et al, North -Holland, 1972, ISBN 0-7204-2208-6 -. A comprehensive overview of CL, including the historical outlines.
- Functional Programming. Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. ISBN 0-201-19249-7
- " Lectures on the Curry - Howard isomorphism ". Sørensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1998.
- " Principal Type - Schemes and Condensed Detachment ", Hindley and Meredith, Journal of Symbolic Logic ( JSL ), Volume 55 (1990 ), Number 1, pages 90-105