Elegant algorithm to semi-decide if two lambda calculus terms are equivalent
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”.