Elegant algorithm to semi-decide if two lambda calculus terms are equivalent

Question

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.

Answer 1

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:

1. if $M$ is a variable
   • if $N \equiv M$, output true
2. 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
3. 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”.

Answer 2

Let me just note that the way you've written your solution it is not guaranteed to work. You need to consider all rewrites of $t_1$ and $t_2$. If you don't you get things like $t_1 \equiv y$, $t_2 \equiv (\lambda x.x) y$.

So, a not-particularly elegant solution is considering all the $αβη$-reductions paths from $t_1, t_2$ and see if there is a common term. If $t_1 =_{βη} t_2$ then there will be common reduct by the Church-Rosser properties of $βη$-reductions.