# 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.

• @D.W. Is it better now? It is undecidable yes, but for positive instances, you can give a witness to prove that they are equal: A path where each step is simple, an hence decidable. Commented Dec 19, 2019 at 0:02
• Presumably we can assume that Bob starts with a commitment to $t_1$ and a commitment to $t_2$, and Alice wants to prove that there exists a way to open the first commitment and the second commitment that yields a convertible pair of $\lambda$-terms? Is that right?
– D.W.
Commented Dec 19, 2019 at 4:35

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.
• Wouldn't your impossibility proof sketch apply to any semi-decidable problem? "If $X$ is semi-decidable then any proof of $x\in X$ will give information on the position of $x$ in the computable enumeration of $X$ and hence won't be zero-knowledge" Is there some specificity of this problem I'm missing? Commented Dec 19, 2019 at 17:07