HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Does a verifier means decidability

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
decidabilityverifierdoesmeans

Problem

If, for example, there is a problem B which have exponential time verifier - a verifier that verify on exponential time - Does it 100% means that B decidable?

On one hand I thought - If there is a verifier - why can't I just decide for each input - using the verifier? On the other hand - from what I know - if it doesn't halt we wouldn't know it...

Thanks.

Solution

I'll start with an intuitive explanation as to why $B$ is decidable. Given input $x$, we can start trying every possible witness $y$ and check whether the verifier $V$ accepts $(x,y)$. This is a semi-algorithm, since it doesn't necessarily halt.

However, we note that since $V$ has exponential running time, then considering witnesses that are "too long", i.e. so long that $V$ won't be able to read all the witness, is irrelevant. So we can in fact stop after a bounded number of witnesses, which makes our procedure a halting algorithm.

Now let's formalize this.

Let's assume that the language $B$ has a verifier $V$ that runs in time $f(n)$ for some function $f$ (in your question, $f$ is an exponential function, but this is not important). A crucial property of $f$ is that it's computable. That is, given $n$ we can compute $f(n)$. It is easy to see that functions such as polynomials and exponentials are computable.

Since $V$ is a verifier for $B$, then we have can write the following:
$$B=\{x: \exists y \text{ such that } (x,y)\in L(V)\}$$
where $V$ has the property that given input $(x,y)$, $V$ halts in time at most $f(|x|)$.

We now make the following key observation: if $V$ accepts $(x,y)$ for some $y$, then there exists $y'$ such that $|y'|\le f(|x|)$ such that $V$ accepts $(x,y')$. That is, if there is a witness, then there is also a "short" witness.

This observation is correct since if $y>f(|x|)$ then $V$ cannot read more than $f(|x|)$ letters of $y$, so it's enough to consider a prefix of $y$.

From this it is easy to see why the procedure we described above works.

Context

StackExchange Computer Science Q#68268, answer score: 5

Revisions (0)

No revisions yet.