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?
