6
$\begingroup$

In lambda calculus, one can prove that two expressions compute the same function if they are equivalent under both beta reduction and eta conversion, where eta conversion consists of eta reduction, $$ (\lambda x.A x) \to A \qquad\text{if $x$ is not free in $A$} $$ and eta expansion, $$ A \to (\lambda x.Ax) \qquad\text{where $x$ is not free in $A$.} $$ Thus, while one cannot computationally check whether two expressions compute the same function, one can computationally verify a proof that they do, if someone produces a sequence of beta reductions and eta conversions that takes one expression to the other. The reason that determining equality between expressions is undecidable has to do with the need to use eta expansions as well as contractions, so you have to backtrack to search for a proof.

My first question is: is the above characterisation correct? It seems to be from what I've read, but I haven't seen it explained in exactly that way and I might have misunderstood.

My second question is, does eta conversion exist in the combinator calculus, or is there an equivalent? In other words, is there a set of formal manipulations on combinator expressions that can be used to show that two are equivalent to one another?

As a simple example, the expressions $S\,K\,K$ and $S\,K\,S$ are equivalent. (They are both the identity function.) I can show this by explicitly evaluating both of them: $$ (S\,K\,K)\,x = (K\,x)\,(K\,x) = x, $$ whereas $$ (S\,K\,S)\,x = (K\,x)\,(S\,x) = x. $$ But this involves introducing variables (i.e. moving away from "pure" SK combinator expressions), and it doesn't proceed by starting from one expression and manipulating it to convert it into the other. Is there a set of syntactic moves that can be used to show this equivalence, analogously to eta conversions in lambda calculus?

$\endgroup$
  • $\begingroup$ IIRC, in the Barendregt lambda calculus book there's an equational axiomatization of combinatory logic, which should prove your goal. It contains several non trivial equations. $\endgroup$ – chi May 12 '16 at 7:12
  • $\begingroup$ @chi I've ordered the Barendregt book (just prior to asking this question) but I live in Japan and Amazon has a five week delivery time for that book. If an answer can be found in Barendregt, posting it here will be a great help both for me and for future visitors. $\endgroup$ – Nathaniel May 12 '16 at 9:31
5
$\begingroup$

From the Barendregt lambda calculus book, we can find theory $CL$ (combinatory logic) defined as follows

$$ K P Q = P \qquad S P Q R = P R (Q R) $$

where $K,S$ are constant symbols (for the well known combinators), while $P,Q,R$ range over all the possible $CL$ terms (built from $K,S$, variables and application). The relation $=$ is postulated to be a congruence.

The $CL$ theory can be extended with the following $A_\beta$ axioms:

$$ \begin{array}{ll} A.1 & K = S(S(KS)(S(KK)K))(K(SKK)) \\ A.2 & S = S(S(KS)(S(K(S(KS)))(S(K(S(KK)))S)))(K(K(SKK))) \\ A.3 & S(S(KS)(S(KK)(S(KS)K)))(KK)=S(KK) \\ A.4 & S(KS)(S(KK)) = \\ & \qquad S(KK)(S(S(KS)(S(KK)(SKK)))(K(SKK))) \\ A.5 & S(K(S(KS)))(S(KS)(S(KS))) = \\ & \qquad S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))S))))(KS) \end{array} $$

(I have double checked these, but I can't swear I got them right.)

Corollary 7.3.15 states that $CL\ +\ A_\beta$ is equivalent to $\lambda$ (the theory of the $\lambda$ calculus with $\beta$ conversion, but no $\eta$ or extensionality).

Hence, in principle one can use "only" the above laws to prove $SKK=SKS$.

The convenience of the above laws is self-evident, I think.

A similar set of axioms is found in the same book for $\lambda\eta = \lambda + \bf ext$. These are $A.3,A.4,A.5$ (hence no $A.1,A.2$) and

$$ \begin{array}{ll} A.6 & S(S(KS)K)(K(SKK)) = SKK \end{array} $$

$\endgroup$
  • $\begingroup$ Gosh, now I see what you meant by "non trivial equations"! Many thanks, this is super helpful. I'll wait for the book to arrive rather than asking you to type out the equations for $\lambda + \mathbf{ext}$ :) $\endgroup$ – Nathaniel May 12 '16 at 11:56
  • 1
    $\begingroup$ @Nathaniel Luckily, the $\bf ext$ axioms overlap a lot, so I added the changes for that case as well. $\endgroup$ – chi May 12 '16 at 12:05
  • $\begingroup$ "The convenience of the above laws is self-evident, I think." I'm hoping this is tongue-in-cheek :) $\endgroup$ – cody May 12 '16 at 13:50
  • $\begingroup$ @cody Indeed it is. :-P $\endgroup$ – chi May 12 '16 at 17:28

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.