Elegant algorithm to semi-decide if two lambda calculus terms are equivalent Given two lambda terms $t_1$ and $t_2$, it is semi-decidable if they are equivalent (i.e. can be rewritten as each other using alpha, beta, and eta conversions). An algorithm to do this is to try every sequence of rewrites starting with $t_1$, and if any of them end with $t_2$, then output true.

What other algorithms can be used? Are there any more "elegant" algorithms?

EDIT: [This] claims that a generalization of the Knuth-Bendix completion algorithm can semidecide the word problem. It has not citations though.
Let’s first suppose we can reduce both $t_1$ and $t_2$ to their $\beta \eta$-normal forms;
$$t_1 \twoheadrightarrow_{\beta \eta} M \qquad \text{and} \qquad t_2 \twoheadrightarrow_{\beta \eta} N$$
If $M$ and $N$ are identical, we are done. Otherwise, we check $\alpha$-equivalence by induction on term complexity:


if $M$ is a variable  


if $N \equiv M$, output true

if $M$ is an abstraction $(\lambda x. M_1)$  


if $N$ is an abstraction $(\lambda y. N_1)$  


output whether $N_1[y:=x]$ and $M_1$ are $\alpha$-equivalent  


if $M$ is an application $(M_1\ M_2)$  


if $N$ is an application $(N_1\ N_2)$


output whether both $M_1$ is $\alpha$-equivalent to $N_1$ and $M_2$ is $\alpha$-equivalent to $N_2$




(You could also use de Bruijn notation and avoid the need for $\alpha$-conversions.)

For non-normalising terms, you can at best use the above procedure after each $\beta \eta$ reduction, but it shouldn't be possible (because of Halting problem) to have anything better than “iterative trying”.