Many year ago, I was introduced to a formalism called "combinatory language". I quite fell in love with it, but that my personal taste. Combinatory logic, according to Wikipedia, was originally introduced as a notation to remove variables from logic. However, in the presentation I'm familiar with variables are used [1]. In fact, I have seen it a computation model: combinatory language is proved equivalent to lambda calculus (trivial) and as such it is also a computation model (and a possible foundation for functional programming).
The fundamental units are combinators, that is to say elementary (higher order) functions. The result of the computation comes from function application (but the elementary functions are so simple that it is possible to see implement the evaluation just as a simple rewrite system). In fact, just two combinators are needed S and K (definition follows). Usually the I combinator is defined as well, but that can be defined in terms of K and S, so it is not "primitive".
Quite interestingly, it is possible to use combinatory logic to define regular first order logic. So it can be a model for mathematics as well... and some rather important (and difficult to prove) theorems in logic are rather elementary and easy results in combinatory logic. But well... to the metal.
Let us have an infinite sequence of variables (lowercase) and a finite or infinite sequence of constants (uppercase), including the three fundamental combinators I, K, S. Variables and constants are atoms. The definition of combinatory term is as follows:
Since combinatory logic is very "operative" we define the fundamental computation tool, which is the weak reduction.
The B combinator is not fundamental, and can be easily defined as S(KS)K. So now we have a pretty clear idea of what combinators are. I corresponds to the identity function. K is "like" a function returning a constant whatever arguments we pass. In fact K is a "function" which given something yields the function always returning that something. B is a function composition operator. S is a bit harder to understand (but wait to see the Y combintor! ;) ),
My first significant lisp program years ago was the implementation (in lisp) of the the basic computable functions (primitive recursive and mu operator, IIRC what I did). I thought that a nice example of another lisp program could be implementing the combinators in Lisp. After doing some more theory (e.g., we haven't yet stated how to "compute" programs or represent numbers), we can go for the implementation.
References
The fundamental units are combinators, that is to say elementary (higher order) functions. The result of the computation comes from function application (but the elementary functions are so simple that it is possible to see implement the evaluation just as a simple rewrite system). In fact, just two combinators are needed S and K (definition follows). Usually the I combinator is defined as well, but that can be defined in terms of K and S, so it is not "primitive".
Quite interestingly, it is possible to use combinatory logic to define regular first order logic. So it can be a model for mathematics as well... and some rather important (and difficult to prove) theorems in logic are rather elementary and easy results in combinatory logic. But well... to the metal.
Let us have an infinite sequence of variables (lowercase) and a finite or infinite sequence of constants (uppercase), including the three fundamental combinators I, K, S. Variables and constants are atoms. The definition of combinatory term is as follows:
- Every atom is a combinatory term
- If X and Y are combinatory terms, (XY) is a combinatory term as well
Since combinatory logic is very "operative" we define the fundamental computation tool, which is the weak reduction.
- IX -> X
- KXY -> X
- SXYZ -> XZ(YZ)
- X -> X
- I(f) = f
- (K(a))(x) = a
- (S(f, g))(x) = f(x, g(x))
- (B(f, g))(x) = f(g(x))
The B combinator is not fundamental, and can be easily defined as S(KS)K. So now we have a pretty clear idea of what combinators are. I corresponds to the identity function. K is "like" a function returning a constant whatever arguments we pass. In fact K is a "function" which given something yields the function always returning that something. B is a function composition operator. S is a bit harder to understand (but wait to see the Y combintor! ;) ),
My first significant lisp program years ago was the implementation (in lisp) of the the basic computable functions (primitive recursive and mu operator, IIRC what I did). I thought that a nice example of another lisp program could be implementing the combinators in Lisp. After doing some more theory (e.g., we haven't yet stated how to "compute" programs or represent numbers), we can go for the implementation.
References
- R. Hindley, B. Lercher, J. P. Seldin, Introduction to combinatory logic (CUP Archive, 1972), p. 170
Powered by ScribeFire.
No comments:
Post a Comment