<p>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 <a href="http://store.elsevier.com/Realizability/Jaap-van-Oosten/isbn-9780080560069/" rel="noreferrer">Jaap van Oosten's book</a>. I don't have any other books with me right now, but am sure almost any book on this topic will have the result, <a href="https://books.google.si/books/about/The_lambda_calculus.html?id=eMtTAAAAYAAJ&amp;redir_esc=y" rel="noreferrer">Barendregt's book</a> surely does.</p>

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

CC BY-SA 3.0
2016-05-08T08:41:41.590Z
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.
N. Virgo
CC BY-SA 3.0
2016-05-08T08:43:01.510Z
If they're at this level they may be better suited for cs.stackexchange.com. This isn't really "research level".
Andrej Bauer
CC BY-SA 3.0
2016-05-08T08:48:55.623Z
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?
N. Virgo
CC BY-SA 3.0
2016-05-08T17:44:09.460Z
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.
Andrej Bauer
CC BY-SA 3.0
2016-05-08T08:25:34.567Z
2016-05-08T08:25:34.567Z
Andrej Bauer
<p>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.</p>
<p>Thus, for instance, both <span class="math-container">$S K K$</span> and <span class="math-container">$S K (S (S S) K)$</span>, will reduce under <a href="https://github.com/RockBrentwood/Combo" rel="nofollow noreferrer">Combo</a>, which I put on GitHub, to <span class="math-container">$I$</span>, as will <span class="math-container">$S K a$</span>, for any term <span class="math-container">$a$</span> (even <span class="math-container">$a = (λx·x x) (λx·x x x)$</span>, which it compiles as <span class="math-container">$a = D (W D)$</span>) when running it with the extensionality axiom on. Similarly, <span class="math-container">$B f I$</span> and <span class="math-container">$B I f$</span> will both reduce to <span class="math-container">$f$</span>, while <span class="math-container">$B (B f g) h$</span> reduces to <span class="math-container">$B f (B g h)$</span>, under extensionality.</p>

CC BY-SA 4.0
2024-03-14T04:39:31.453Z
2024-03-14T04:39:31.453Z
NinjaDarth
<p>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.</p>

<p>"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?</p>

<p>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.</p>

<p>I note that there is a <a href="https://cstheory.stackexchange.com/questions/14132/is-it-possible-to-compute-whether-two-functions-are-extensional-equal">similar question</a> 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. </p>

CC BY-SA 4.0
2024-03-14T16:07:14.643Z
This is arguably the first and most famous of undecidable problems :)
cody
<lambda-calculus><combinatory-logic><extensionality>
Algorithm for extensional equality in combinator calculus
N. Virgo
# Algorithm for extensional equality in combinator calculus

(Asked by: username_0 on 2016-05-08)

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](https://cstheory.stackexchange.com/questions/14132/is-it-possible-to-compute-whether-two-functions-are-extensional-equal) 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.

**Tags:** lambda-calculus, combinatory-logic, extensionality

> **Comments:**
> **username_1**: This is arguably the first and most famous of undecidable problems :)  

---

## 2 answers

### Answer by username_2 on 2016-05-08. Score: 5 | Accepted answer

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](http://store.elsevier.com/Realizability/Jaap-van-Oosten/isbn-9780080560069/). 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](https://books.google.si/books/about/The_lambda_calculus.html?id=eMtTAAAAYAAJ&redir_esc=y) 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).

> **Comments:**
> **username_0**: 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.  
> **username_2**: If they're at this level they may be better suited for cs.stackexchange.com. This isn't really "research level".  
> **username_0**: 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?  
> **username_2**: 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.  

---

### Answer by username_3 on 2024-03-14. Score: 1

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](https://github.com/RockBrentwood/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.


---

