5

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.

xavierm02
  • 1,255
  • 6
  • 14
  • @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. – xavierm02 Dec 19 '19 at 00: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. Dec 19 '19 at 04:35

1 Answers1

3

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.

D.W.
  • 159,275
  • 20
  • 227
  • 470
  • 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? – xavierm02 Dec 19 '19 at 17:07
  • @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... – D.W. Dec 19 '19 at 17:52
  • 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. – xavierm02 Dec 19 '19 at 20:50
  • @xavierm02, fair enough -- I'm not completely convinced either! – D.W. Dec 21 '19 at 05:17