Understanding A Recursive Definition of CL-Terms in Combinatory Logic

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?

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.

StackExchange Computer Science Q#68689, answer score: 3