3
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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).

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Roy O. Jul 15 '14 at 11:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.