9/18/19
Combinatory logic is 'simplified' way of doing the lambda calculus. In the lambda calculus there are variables and constants, applications, and abstractions; combinatory logic makes do with variables and constants, and applications only—abstractions are done away with. There are more rules for reduction in combinatory logic, but since all variables are free there are none of the complications of capturing, sound substitutions, and name rewrites. Let us take a simple example, in the lambda calculus the identity combinator is λx.x and its effect when applied to an arbitrary argument, say y, is to reduce to y
(λx.x y) ⇒ y
In combinatory logic there is a combinator for identity, written I (*note the boldface*) and it is governed by the reduction rule
I y ⇒ y
(*Notice here we are using juxtaposition, with a space between the items, for application and left association with that, so 'I y' amounts to '(I y)'. Both of these conventions are fairly standard. Left association fits in with currying, so 'X arg1 arg2 arg3' means '(((X arg1) arg2) arg3)' ie multiple arguments are swallowed one at a time in the order they appear. The conventions are also standard in straight lambda calculus. We did not have to invoke them there because for clarity for teaching we were putting all applications in brackets anyway.*)
Roughly, combinatory logic takes the combinators of lambda calculus, leaves out their internal structure, and presents directly the rules for their reduction.
Syntax of combinator expressions
<combex> ::= <atom> | <application> | (<combex>)
<atom> ::= <variable>|<constant>|<combinator>
<application> ::= <combex> <combex>
for example, x,y, L avariable, M avariable y x are all combinator expressions. (*As mentioned, it is usual to use juxtaposition, with a space, for application (so, again, application is a silent operator, for example I y means I@y), together with left association and, round brackets to improve clarity or to get right association.*)
A distinguished combinator expression, which has a reduction rule, is usually called a combinator and it written in boldface (not the easiest to do with pen and paper).
You can see what the problem is going to be for combinators. In the lambda calculus the occurrences of the variable of abstraction within the body of an abstraction are just place markers to indicate where the argument is going to go when there is a beta-reduction. The problem for combinators is whether they can pick out all possible positions of the place markers. It turns out that theoretically everything can be done with just two combinators, the S and K combinators. Let us start by looking at them.
S K I combinators
The reduction rule for K is:-
K x y ⇒ x
The combinator K consumes two arguments and reduces to the first argument. So K is just a projection function, sometimes called a cancellator.
The reduction rule for S is:-
S x y z ⇒ x z (y z)
The combinator S consumes three arguments and reduces to the first argument applied to the third argument applied to the second argument applied to the third argument.
Let us write the silent application in for one moment... S@x@y@z ⇒ x@z@(y@z)
What S does is somewhat lacking in an intuitive counterpart. Part of it is composition— the first argument applied to the third argument applied to the second argument applied to the third argument— is the composition of two function applications. But the first function application here is the first argument applied to the third argument, which is a sort of substitution. So... S does is not have an easy interpretation, but it is a substitution-and-composition function (sometimes called a distributor).
S and K are called the standard combinators. A combinator expression in which the only combinators are the standard ones is called a standard combinator expression.
It is handy to have the identity combinator (or identificator)
I =df. S K K
( * note that this reduces I x =df. S K K x and S K K x ⇒K x (K x)⇒ x which is what we want. *)
(*For the exercises below... Select a line. Choose Rewrite Rules. Select a specific Rewrite Rule. Select a (sub)expression that you wish to rewrite with that rule. Press Go.*)
Try to prove the following:-
a) I a ⇒ a
b) K a b ⇒ a
c) S a b c ⇒ a c (b c)
d) S K K a ⇒ a
e) S I I I arg ⇒ arg
[Click on a formula to select it, choose a rule from the menu.]
Here's a little hint for doing these as they get more difficult. So called 'normal order reduction' will produce a normal form if there is one (more on that later). And in this case normal order reduction can be just working from left to right. Now, each of the combinator reduction rules starts with a different letter (e.g. B, C, I, K, S, Y..). So, all you need do is match the leftmost combinator letter in the expression against the relevant reduction rule and do the reduction. (Repeat until finished.)
Here is an animation of Proof 5.
More combinators
It is usual to move beyond pure SK expression combinators and allow in all sorts of other combinators (which, of course, could be defined in terms of SK). This is primarily to reduce the length and complexity of the expressions.
Straight translations of lambda expressions into SK combinators are usually astonishingly long e.g. the translation of a simple addition function λx.λy.(+ x y) has 18 combinators in it (and many nested brackets). However at a conceptual and theoretical level, combinators and combinator graph reduction are extraordinarily simple. And combinator reduction is naturally lazy (being from left to right)
B x y z ⇒ x (y z) (* compositor *)
C x y z ⇒ x z y (* permutator*)
I x ⇒ x (* identificator *)
K x y ⇒ x (* cancellator *)
S x y z ⇒ x z (y z) (* distributor *)
W x y ⇒ x y y (* duplicator*)
Y f ⇒ f (Y f) (* fixpoint. Just as a matter of interest define A as B (S I ) (S I I ) then Y is A A *)
Try to prove the following:-
a) I a ⇒ a
b) S K K a ⇒ a /* S K K produces the same effect as I */
c) B a b c ⇒ a (b c)
d) S (K S) K a b c ⇒ a (b c) /* S (K S) K produces the same effect as B */
[Click on a formula to select it, choose a rule from the menu.]
Here is an animation of Proof 4, being provided as an example
Try to prove the following:-
a) C a b c ⇒ a c b
b) S (S (K (S (K S) K)) S) (K K) a b c ⇒ a c b /* S (S (K (S (K S) K)) S) (K K) produces the same effect as C */
c) W a b ⇒ a b b
d) S S (S K) a b ⇒ a b b /* S S (S K) produces the same effect as W */
e) Y f ⇒ f (Y f )
[Click on a formula to select it, choose a rule from the menu.]
Although combinators strictly speaking have only one argument (and use currying), we can talk of some of them expecting several arguments in as much as maybe several arguments are needed before the reduction rule can be invoked. e.g. B is a combinator of three arguments, I is a combinator of one.