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.

  • $\begingroup$ @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. $\endgroup$
    – xavierm02
    Commented Dec 19, 2019 at 0:02
  • $\begingroup$ 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? $\endgroup$
    – D.W.
    Commented Dec 19, 2019 at 4:35

1 Answer 1


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.

  • $\begingroup$ 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? $\endgroup$
    – xavierm02
    Commented Dec 19, 2019 at 17:07
  • $\begingroup$ @xavierm02, quite possibly. I haven't thought it through carefully. Most typically I've seen zero knowledge proofs used with languages that are in NP or PSPACE or some decidable complexity class. In any case, whether it's true or not, I'm not sure how it would be relevant to your question, though... $\endgroup$
    – D.W.
    Commented Dec 19, 2019 at 17:52
  • $\begingroup$ I'm not fully convinced by the impossibility proof sketch, but I can't really pinpoint why. But if there is such an impossibility, the proof is probably clearer at the level of an arbitrary semi-decidable language than instanciated on this particular one. $\endgroup$
    – xavierm02
    Commented Dec 19, 2019 at 20:50
  • $\begingroup$ @xavierm02, fair enough -- I'm not completely convinced either! $\endgroup$
    – D.W.
    Commented Dec 21, 2019 at 5:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.