Composition of combinators with arities greater than one

In combinatory logic, the axiom of composibility asserts that for any two combinators, $A$ and $B$, there exists a combinator $C$ that composes $A$ and $B$. That is, for all $A,B,x$ there exists a $C$ such that: $CABx = A(Bx)$.

But what if $A$ and $B$ have arities other than 1? In particular, suppose that $A$'s arity is greater than $B$'s. Say $A$ has arity 4 and $B$ has arity 2. Presumably, this would mean that their composition should be $CABvwxyz = A(Bvw)xyz$, so that $A$ would then operate on the four combinators $(Bvw), x, y$ and $z$. Is this correct? Surely not $CABvwxyz = A(Bv)wxyz = (A(Bv))wxyz$.

I believe what I am confused about is the use of the 'variable combinator' notation (e.g., $Axy$). It doesn't seem to me to be syntactically strict. I believe it is a meta-notation, intended to express the arity of a combinator; which is fine, except that, given the subtleties of reasoning with combinators (at least for my humble comprehension :-) ), I would very much appreciate having an explicit re-write rule to transform one sequence of combinators into another. Is my thinking mis-guided?

One methodical way of accomplishing this is to construct a corresponding lambda term and to then convert it to a CL term using pseudoabstraction.

First some definitions. You want to compose two combinators $A$ and $B$ with arities $p$ and $q$, respectively. Let $C^\lambda_{p,q}$ represent the lambda term accomplishing this.

$C^\lambda_{p,q}$ must first accept $A$, then $B$, then the $q$ arguments $b_1,\ldots,b_q$ of $B$, and then $p-1$ remaining arguments $a_1, \ldots, a_{p-1}$ of $A$ (note: '$p-1$' because the argument $B(b_1\ldots b_q)$ has already been accepted). So $C^\lambda_{p,q}$ must accept $ p + q + 1$ arguments in total, and it must satisfy:

$$C^\lambda_{p,q} A B b_1 \ldots b_qa_1\ldots a_{p-1} \rhd_\beta A(Bb_1\ldots b_q)a_1 \ldots a_{p-1}$$

This easily works for:

$$C^\lambda_{p,q} \equiv \lambda xyb_1 \ldots b_q a_1 \ldots a_{p-1}.x(yb_1 \ldots b_q)a_1 \ldots a_{p-1}$$

So in your example with $p = 4$ and $q = 2$, we get:

$$C^\lambda_{4,2} \equiv \lambda xyb_1b_2 a_1 a_2 a_3.x(yb_1 b_2)a_1 a_2 a_3 $$

Now for the conversion. To this end we introduce the notion of pseudo-abstraction, as defined below by Hindley & Seldin in Lambda-calculus and Combinators:

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

• $[x].M \equiv \mathsf{K}M$ $\hspace{29.8mm}$if $x \not\in FV(M)$

• $[x].x \equiv \mathsf{I}$

• $[x].Ux \equiv U$ $\hspace{33mm}$if $x \not\in FV(U)$

• $[x].UV \equiv \mathsf{S}([x].U)([x].V)$ $\hspace{3mm}$if neither (1) nor (3) applies

Here, $\equiv$ denotes syntactical equivalence, and $[x]$ is not really part of the language of combinatory logic itself. Intuitively, a term $[x].M$ is just a name for a valid CL term which we can recover using the above definition. The definition will eliminate all bound variables. For example:

$$[xy].xyx$$
$$[x].([y].(xy)x)$$
$$[x].(\mathsf{S}([y].xy)([y].x))\text{(Def. 1.4)}$$
$$[x].(\mathsf{S}([y].xy)(\mathsf{K}x))\text{(Def. 1.1)}$$
$$[x].(\mathsf{S}(x)(\mathsf{K}x))\text{(Def. 1.3)}$$
$$[x].(\mathsf{S}x)(\mathsf{K}x)$$
$$\mathsf{S}([x].\mathsf{S}x)([x].\mathsf{K}x) \text{(Def. 1.4)}$$
$$\mathsf{S}([x].\mathsf{S}x)(\mathsf{K}) \text{(Def. 1.3)}$$
$$\mathsf{S}(\mathsf{S})(\mathsf{K}) \text{(Def. 1.3)}$$
$$\mathsf{SSK}$$

So $[xy].xyx \equiv \mathsf{SSK}$, i.e. when we write $[xy].xyx$, we really mean $\mathsf{SSK}$. You can verify that $\mathsf{SSK}$ captures the intended functionality:

$$\mathsf{SSK}xy \rhd_{1w} (\mathsf{S}x)(\mathsf{K}x)y \rhd_{1w} xy(\mathsf{K}xy) \rhd_{1w} xyx$$

similarly, the CL term $C^{CL}_{p, q}$ for $C^\lambda_{p, q}$ is simply:

$$[xyb_1 \ldots b_q a_1 \ldots a_{p-1}].x(yb_1 \ldots b_q)a_1 \ldots a_{p-1}$$

Of course, to do the elimination of variables manually even for $C^{CL}_{4,2}$ is tedious, but the point is that the meaning is fixed (and the process of elimination could easily be automated).

StackExchange Computer Science Q#27604, answer score: 2