# 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:

1. $[x].M \equiv \mathsf{K}M$ $\hspace{29.8mm}$if $x \not\in FV(M)$
2. $[x].x \equiv \mathsf{I}$
3. $[x].Ux \equiv U$ $\hspace{33mm}$if $x \not\in FV(U)$
4. $[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).

You are right that $Axy$ is not a syntactically strict. In strict combinatory logic, each term is either (0) an atom (i.e. a variable), (1) a combinator (or a $\lambda$ expression) or (2) a pair $(f g)$, read "$f$ applied to $g$". The expression $Axy$ is really shorthand for $((Ax)y)$. We see two conventions in play here:

1. The application operator can also be expressed by just juxtaposition. Compare with the usual notation for multiplication: $ab$ stands for $(a \times b)$.

2. Function application associates to the left. So the correct way of parenthesizing $Axy$ is $((Ax)y)$ rather than the other way around, $(A(xy))$. Compare subtraction and division: $3-2-1 = ((3-2)-1)$.

The combinator $K$, to take an example, satisfies the equation $Kxy = x$. What that really means is that $(Kx)$ is the function $\lambda y.x$, and so $((Kx)y) = ((\lambda y.x)y) = x$. Here $x,y$ are variables or atoms, if we allow the latter.

How should you simplify an expression like $Kx$? The usual convention in combinatory logic, to the best of my knowledge, is not to simplify. So only simplify a combinator if it has enough "arguments". This way you never get to see the intermediate $\lambda$ expressions.

• You are of course correct about the correspondence between $\lambda$ and CL, but in my opinion it is misleading to reduce combinatory logic to lambda-calculus. Combinatory logic precedes lambda calculus historically and it is also a simpler theory than $\lambda$. So we don't really have that $((Kx)y) = ((\lambda y.x)y)$ in any formal sense, we just have the weak reduction relation $\rhd_w$ that specifies $Kxy \rhd_w x$ in CL. $Kx$, then, cannot be reduced because there is no rewriting rule that is applicable. Within CL it does not make sense to speak of intermediary $\lambda$ expressions. – Roy Jul 15 '14 at 11:57