Understanding A Recursive Definition of CL-Terms in Combinatory Logic

Question

From page 26 of Lambda-Calculus and Combinators:

Definition 2.18 (Abstraction) For every CL-term $M$ and every variable $x,ドル a CL-term called $[x].M$ is defined by induction on $M,ドル thus:

(a) $[x].M \equiv \mathbf{K}M$ if $x \notin FV(M)$;

(b) $[x].x \equiv \mathbf{I}$;

(c) $[x]Ux \equiv U$ if $x \notin FV(U)$

(f) $[x]UV \equiv \mathbf{S}([x]U)([x].V)$ if neither (a) nor (c) applies.

Here $\mathbf{I}$ is meant to denote the identity operator, $\mathbf{K}$ the constant operator, and $\mathbf{S}$ the "stronger composition operator" where in mathematical notation:

$$ \mathbf{S}(f,g))(x) = f(x, g(x)) \text{ for functions $f,ドル $g$} $$

Question: It seems that (f) of this definition just comes out of nowhere. I have no idea what is motivating it behind the scenes. Does anybody have any insight on where this definition comes from?

Answer 1

Here are some considerations that could have been used to sort of "derive" the (f) rule:

• it is natural to define our type of conversion recursively;
• the general case when the body of "$\lambda$" is an application $(UV)$ needs to be addressed;
• we certainly would like to get $[x].([y].([z].xz(yz)))$ converted into its corresponding combinator $\mathsf{S}$.

Using the above we get an intermediate version of the (f) rule:

$$[x].UV \equiv A([x].U)([x].V),$$ where some closed CL-term $A$ is to be determined. The position of $A$ is chosen so that the subsequent "calls" of the (c) rule would be possible, or all three positions could be tried in turn.

$$\begin{array} ([x].([y].([z].xz(yz)))) &\equiv [x].([y].A([z].xz)([z].yz)) &\text{rule (f)}\\ &\equiv [x].([y].(A x) y) &2 \times \text{rule (c)}\\ &\equiv [x].Ax &\text{rule (c)}\\ &\equiv A &\text{rule (c)}, \end{array}$$ hence $A = \mathsf{S}$ and the final version of the (f) rule $$[x].UV \equiv \mathbf{S}([x].U)([x].V).$$

Note that the above is not a "real derivation", it's just some informal speculations, which I hope can help you to build up some intuition about that conversion.

• George: Could it be said that in the lambda calculus $\lambda,ドル two "functions" next to each other is interpreted as one function being applied to the other. Whereas in the combinatory logic (CL), two "functions" next to each other is interpreted as one function being "strongly composed" with the other (i.e., $\mathbf{S}$)?
• George: So to clarify, I am asserting that in the lambda calculus we have that $(\lambda x. x(\lambda y. y)) = (\lambda y. y)$ yet in CL we have that $([x].x([y].y)) = \mathsf{S}([x].x)([y].y)$. Here our interpretations of similarly formed formulas completely diverge between these two systems. Is my understanding correct?
• Anton Trunov: $(\lambda x. x(\lambda y. y))$ does not reduce to $\lambda y. y,ドル it is in normal form. $[x].x ([y].y) \equiv ([x]. x \mathbf{I}) \equiv (\mathbf{S} ([x]. x) ([x].\mathbf{I}) \equiv (\mathbf{SI(KI)})$. It is easy to see that the last term is equivalent to its $\lambda$-calculus counterpart, because $\mathbf{SI(KI)}x \equiv \mathbf{I}x(\mathbf{KI}x) \equiv x\mathbf{I}$.