10
$\begingroup$

No Time Hierarchy theorem is known for $\mathsf{BPTIME}$, however, consider the following simple modification of the definition:

A language is in $\mathsf{ProvableBPTIME}[f(n)]$ if there is a randomized Turing-machine $T$ that decides membership with error $\le \frac 13$ in time $f(n)$ [so far usual definition of $\mathsf{BPTIME}$] and it can be proved that $T$ accepts every $x$ with probability $\ge \frac 23$ or with probability $\le \frac 13$ [so there is a proof that $T$ satisfies the $\mathsf{BP}$ condition].

Note that this definition is completely different from that of $\mathsf{PromiseBPTIME}$.

For $\mathsf{ProvableBPTIME}$ there is a Time Hierarchy: On input $(T,\Psi,x)$, reject if $\Psi$ is not a proof that $T$ satisfies the $\mathsf{BP}$ condition, otherwise simulate $T$ on input $(T,\Psi,x)$ (until our running time permits), then negate the answer. Using standard tricks, hierarchy results can be established also about $\mathsf{RTIME}$ and similar classes.

This method almost gives a Time Hierarchy theorem for $\mathsf{BPTIME}$ as well, the only issue is that if there is a $T$ that satisfies the $\mathsf{BP}$ condition but this cannot be proved. (Think about fast primality tests using the Generalized Riemann Hypothesis.) In fact, I find the situation quite plausible that there are some fast algorithms whose correctness cannot be proved. If this is the case, it would be quite hard to diagonalize against them with an algorithm that must provably satisfy the $\mathsf{BP}$ condition.

So my questions would be:
1, Has $\mathsf{ProvableBPTIME}$ been defined before?
2, Are there known hierarchy theorems using some kind of provability?
3, Is there a way to take care somehow of the unprovably correct algorithms?

Related questions: Hierarchy for BPP vs derandomization, Is there a Quantum equivalent of the Time hierarchy theorem ?,
https://cs.stackexchange.com/questions/132936/does-promisebptime-have-a-time-hierarchy-theorem

Update 2020/12/24: Joshua pointed out that in Chapter 6 of Hartmanis: Feasible Computations and Provable Complexity Properties a similar definition was considered but only for the provability of the time/space bound $f(n)$ of deterministic classes. I would instead define $\mathsf{ProvableDTIME}[f(n)]$ as deterministic algorithms whose correctness can be proven. (Again think about primality tests using the GRH.) Then we can ask the following.

$\mathsf{DTIME}[f(n)]\neq\mathsf{ProvableDTIME}[f(n)]$ for some time-constructible function $f(n)$? Could $\mathsf{P}$ and $\mathsf{ProvableP}$ differ?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ In your definition you write: "and it can be proved that". But then you should also specify the logic fragment in which this proof is done. $\endgroup$
    – Gamow
    Dec 23, 2020 at 21:34
  • 1
    $\begingroup$ Yes, but I didn't want to go into these details. $\endgroup$
    – domotorp
    Dec 23, 2020 at 22:01
  • 2
    $\begingroup$ I don't remember if Hartmanis defined it for BPTIME in particular, but his monograph nicely lays out the kind of theory you're asking about, I think. See eg cstheory.stackexchange.com/a/36088/129 $\endgroup$
    – Joshua Grochow
    Dec 24, 2020 at 1:49
  • 2
    $\begingroup$ @Joshua Indeed the proof of his Theorem 6.3 is practically the same as the one sketched above! But he only studies provable time and space bounds for deterministic Turing machines, denoted $\mathsf{F-TIME}$ and $\mathsf{F-SPACE}$. He proves $\mathsf{F-TIME}[f(n)]\ne \mathsf{TIME}[f(n)]$ for some recursive $f(n)$, exploiting that $f(n)$ is not time-constructible. $\endgroup$
    – domotorp
    Dec 24, 2020 at 6:29

0

Reset to default

Your Answer

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