Is there some way to give a zero-knowledge proof that two $\lambda$-terms are convertible, i.e. equal modulo $\beta\eta$?
A usual (and not zero-knowledge) proof that two terms are convertible is a path of terms between the two such that each step is either a single $\beta$ reduction or a single $\eta$ expansion, or the reverse of either one. Testing that two terms are convertible is only semi-decidable because no bound can be given a priori on the length of that path.
The question is the following: Alice has two $\lambda$-terms $t_1$ and $t_2$, and a proof that they are convertible. Can she convince Bob that they are convertible without helping Bob find the path?
One way to do this would be that Alice gives Bob a third term $t_3$ that she knows is convertible to the two others, and then Bob gets to ask her either to prove that it's convertible to $t_1$ or that it's convertible to $t_2$. I'm not sure how the term $t_3$ can be chosen though.