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.
