# Algorithm for extensional equality in combinator calculus

I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as $$(S\, K\, K) \qquad\text{and}\qquad (S\, K\, (S\, (S\, S)\, K )),$$ which both represent the identity function, but one of them is needlessly more complicated than the other.

"Extensional equality" is the terminology used when we consider two expressions to be equal if they represent the same function in this way. I would like to know whether there is an algorithm to determine whether two expressions are in fact extensionally equal. That is, can I determine in general whether two expressions represent the same mapping?

I suspect the answer might be "no", since it feels like this is the sort of thing that should be undecidable. On the other hand, it's straightforward to determine in the case above, since the expressions $(S\, K\, K)\, x$ and $(S\, K\, (S\, (S\, S)\, K ))\, x$ both evaluate to $x$, and I'm new enough to this stuff not to trust my intuition that this can't be generalised.

I note that there is a similar question about programs in general rather than the combinator calculus, which seems to confirm my intuition that this is undecidable. There is also plenty of discussion of this issue in the context of the (untyped) lambda calculus, in which $\eta$-conversion plays a pivotal role. However, I would like to know specifically how to think about this in terms of combinator calculus.

• This is arguably the first and most famous of undecidable problems :)
– cody
Commented Mar 14 at 16:07

Equality of terms in the combinator calculus is undecidable. We can encode the natural numbers as Church numerals and then show that every recursive function is represented, see for instance section 1.3.1 of Jaap van Oosten's book. I don't have any other books with me right now, but am sure almost any book on this topic will have the result, Barendregt's book surely does.

For your purposes it might be useful enough to apply a simple heuristic that will cover sufficiently many cases. You could do exactly what you suggest: see if two terms applied to a variable reduce to the same term (but you need to give up after a while).

• This has to be correct I think - it was kind of a silly question really. I have some follow-on questions, but I'll post them separately. Commented May 8, 2016 at 8:41
• If they're at this level they may be better suited for cs.stackexchange.com. This isn't really "research level". Commented May 8, 2016 at 8:43
• Well, fair enough I guess. I was too quick to ask a basic question that had an obvious answer. My follow-on question is about the equivalent of eta conversion for the combinator calculus. I.e. is there a syntactic rule that I can apply repeatedly in order to exhibit a proof that two expressions are in fact equivalent, which could then be verified by a program. Is that better suited to this site or cs.se? Commented May 8, 2016 at 8:48
• In the old times, before the internet thing, people looked in books. The place to look would be Curry and Feys "Combinatory Logic" (two volumes), in case you feel nostalgic. Commented May 8, 2016 at 17:44

If either of two combinator terms has a strong normal form, and are η-equivalent when treated as λ-terms, then they will both have a strong normal form, it will be the same one, and it may be found by the method you suggested.

Thus, for instance, both $$S K K$$ and $$S K (S (S S) K)$$, will reduce under Combo, which I put on GitHub, to $$I$$, as will $$S K a$$, for any term $$a$$ (even $$a = (λx·x x) (λx·x x x)$$, which it compiles as $$a = D (W D)$$) when running it with the extensionality axiom on. Similarly, $$B f I$$ and $$B I f$$ will both reduce to $$f$$, while $$B (B f g) h$$ reduces to $$B f (B g h)$$, under extensionality.