8

IP = PSPACE is a famous result (and indeed paper) by Adi Shamir in 1992. Furthermore, we clearly have NP $\subseteq$ PSPACE and coNP $\subseteq$ PSPACE, but we don't know how NP relates to coNP. There are several reasons to believe that determining the relationship between NP and coNP is difficult, some of which are discussed in this recent thread.


6

Wikipedia outlines such an example. Consider the coNP-complete problem UNSAT: given a CNF $\varphi$ on $n$ variables, we want to convince the verifier that $\varphi$ is not satisfiable. We arithmetize $\varphi$ to a polynomial $p$ and choose some large prime $q$. Let $$p(x_1,\ldots,x_k) = \sum_{x_{k+1}=0}^1 \cdots \sum_{x_n=0}^1 p(x_1,\ldots,x_n).$$ The ...


5

You understand incorrectly. That is not how logic programming works. The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of $\forall x \in \mathbb{N} \,.\, \phi(x)$ are $\phi(0)$, $\phi(1)$, $\phi(2)$, $\phi(3)$, $\phi(3 + 2)$, $\phi(x \cdot 2)$, and so on. Generating all consequences is infeasable ...


5

It could be that both definitions are used by different authors. Whenever you use the concept of rounds, make sure to tell the reader what you mean by a round. In any case, the two concepts differ by a factor of $2$.


4

Your protocol is not very clear. What do you mean at step 3 by "it chooses one variable, re-computes the formula"? I assume the verifier just sets that variable to 1 and re-computes the formula without that variable. Then, this protocol still has some problems. Let's say that there are two sets of variables that satisfy the formula: $\{x\}$ and $\{y,z\}$. ...


4

I can see some similarity too, but only in a loose sense; there are also some significant differences. Here's the similarity. Define $H_2(x)$ to be the first $d$ bits of $H(x||D)$. Then you can think of the Bitcoin proof-of-work as being: find $x$ such that $H_2(x)=0$. This is loosely similar to the Goldwasser-Sipser protocol; you could imagine that ...


4

This is of course a consequence of $coNP \subset PH \subset PSPACE = IP$. But it can also be proven directly for UNSAT. The basic idea is reducing the problem to zero-testing a sum over a polynomial in a suitable finite field. It's a bit too technical to repeat neatly here, but I can give you an informal idea of how it is done. Let's consider a formula $\...


3

Goldreich and Oren, in their paper Definitions and properties of zero-knowledge proof systems, show that if the verifier is deterministic then interactive proofs trivialize to RP, whereas if the prover is deterministic then interactive proofs trivialize to BPP. See Section 4 of their paper. Blum, de Santis, Micali and Persiano constructed noninteractive ...


3

I think the usual way of doing this is that you hash each record (with a known cryptographically secure hash) and provide the client with $N$ hash values. The client chooses $k$ out of those hash values and you reply with the corresponding $k$ records. The client can then verify that the hash values match up correctly with the provided records plus whatever ...


3

If $x \in L$ then the probability that $(P,V)(x,r) = 1$ is positive, where $r$ is the randomness involved; the probability is over the choice of $r$. In particular, there is some $r$ such that $(P,V)(x,r) = 1$. In contrast, when $x \notin L$, the probability that $(P,V)(x,r) = 0$. That is, there is no $r$ such that $(P,V)(x,r) = 1$. States differently, ...


2

There is no relativizing technique to show that $\mathrm{IP}$ is closed under complement. Clearly, $\mathrm{NP}\subseteq\mathrm{IP}$. Fortnow and Sipser gave an oracle relative to which $\mathrm{co}$-$\mathrm{NP}$ does not have interactive proof system. So, you have to study the arithmetization technique that settles down this conjecture (long ago). Are ...


2

Yes. We could have defined MIP to allow an exponential number of provers but that is basically the PCP model which is equivalent to MIP with a polynomial (or just two) provers.


2

In Haskell there are more programs than there are Coq proofs because Haskell has general recursion whereas Coq does not. (In fact Coq allows you to extract proofs into Haskell code.) The reason that Coq does not have general recursion is that with it we can "prove" anything, simply by saying "to prove $t$ just make a recursive call to itself": ...


1

Suppose you have a (randomized) verifier $V$ such that, for all $Q,w$, $$\begin{align*} w\in L &\implies \Pr[V\leftrightarrow P\text{ accepts }w]\geq2/3\\ w\notin L &\implies \Pr[V\leftrightarrow Q\text{ accepts }w]= 0. \end{align*}$$ Since $P$ is one possible value of $Q$, it follows that $$w\notin L \implies \Pr[V\leftrightarrow P\text{ accepts }...


1

Here's a deterministic zero-knowledge proof of sorts, if there are any logic gaps please let me know!: This zero knowledge proof involves proving you have a solution to three-colouring a map. The common zero knowledge proof for this scenario (Hats & Crayons for example)involves the Prover tries to convince the Verifier that you have found a solution by ...


1

At the very core of Zero Knowledge proof systems, lies the fact that proofs are published by asking the party to prove the correctness of its knowledge, via any one of many methods to verify a solution. Since knowing the question in advance allows a party to forge another proof, the only way to get a reliable proof is via asking a random question out of a ...


1

$AM$ is defined to be $AM[2]$, i.e. languages with 2-rounds Arthur-Merlin protocol, which is equal to $AM[k]$ for any constant $k$. Two extra rounds are required to overcome the fact that the coins are public, i.e. $IP[k]\subseteq AM[k+2]$ for any $k$ , constant or not, as stated in complexity zoo. This means that $IP[poly]=AM[poly]=PSPACE$ (which answers ...


1

To answer the question: No implementation of Haskell to my knowledge has ever represented datatypes as church encodings. I believe that church-style encodings (or variants such as Scott encodings) work equally well for coinductive types.


Only top voted, non community-wiki answers of a minimum length are eligible