Zero-knowledge proof of $\beta\eta$ equality

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.

I doubt that a zero-knowledge proof is possible, because it seems likely that any finite proof will leak at least partial information about the length of the path that converts $t_1$ to $t_2$, and hence won't be zero-knowledge. In particular, suppose Alice and Bob's interaction takes $T$ time steps. Then in any reasonable proof I can imagine, Bob would be able to infer that $t_1$ can be converted to $t_2$ using a path of length at most $T$. This is partial knowledge, because there exists a pair $t_1,t_2$ of terms that take strictly more than $T$ time steps to convert.

I suspect that we might need an additional condition, such that there is a fixed and known upper bound $B$ on the length of the path converting $t_1$ to $t_2$. If you have such a bound, there is a zero-knowledge proof protocol whose complexity is polynomial in $B$, as the statement you are proving becomes a NP-statement, and it is known that there are zero-knowledge protocols for every language in NP.

StackExchange Computer Science Q#118679, answer score: 3