18
$\begingroup$

I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.

  1. their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but
  2. no proof using only efficient concepts is known (i.e. we don't know how to prove their correctness and efficiency in $TV^0$ or $S^1_2$).

I can make artificial examples myself. However I want interesting natural examples, i.e. algorithms studied for their own sake, not created just to answer this type of questions.

$\endgroup$
6
  • 1
    $\begingroup$ Perhaps something from automata theory, where an algorithm is easy, but to show it works one needs to consider all subsets of something or other? $\endgroup$ Apr 5, 2013 at 6:23
  • 2
    $\begingroup$ How about polynomial-time primality checking? That proof is likely to be complicated enough to be hard to stick inside $S^1_2$? $\endgroup$ Apr 5, 2013 at 6:23
  • 4
    $\begingroup$ @Neel, actually Emil's thesis "Weak pigeonhole principle, and randomized computation" is about formalizing probabilistic algorithms. A main axiom needed for formalizing some of these seems to be approximate counting which is not part of $TV^0$ or $S^1_2$. I think it might be simpler to stick to the deterministic polytime case with $TV^0$ and $S^1_2$. $\endgroup$
    – Kaveh
    Apr 5, 2013 at 7:59
  • 1
    $\begingroup$ ps: It would be more interesting if we can prove that the correctness/efficiency of the algorithms are not provable in these theories, or at least are equivalent to statements which are believed to be unprovable in them. However asking for that is probably too much with what we know currently. $\endgroup$
    – Kaveh
    Apr 5, 2013 at 8:11
  • 4
    $\begingroup$ @Neel, most of the relevant probability can be done in first-order systems since you never really need to know the exact probability of an event, you usually only need to compare that probability with certain rational numbers. $\endgroup$ Apr 5, 2013 at 12:56

3 Answers 3

15
$\begingroup$

This is the same idea as Andrej's answer but with more details.

Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.

$\endgroup$
11
$\begingroup$

This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by Hesse, Allender, and Barrington can be proved in the corresponding theory $\mathit{VTC}^0$.

The argument is pretty elementary, and there should be no problem formalizing it in $\mathit{TV}^0$, but with respect to $\mathit{VTC}^0$ it suffers from a chicken-and-egg problem: it makes heavy use of the very functions whose $\mathrm{TC}^0$-computability is furnished by the algorithm.

For another example, the Jacobi symbol $\left(\frac an\right)$ is polynomial-time computable, but its soundness in the form

if $p$ is an odd prime and $\left(\frac ap\right)=1$, then $a$ is a quadratic residue modulo $p$

is not provable in $S^1_2$ unless factoring can be done in probabilistic polynomial time, by the arguments here.

Another class of examples is given by irreducibility testing and factorization algorithms for polynomials (primarily over finite fields and over the rationals). These invariably rely on Fermat’s little theorem or its generalizations (among others), and as such are not known to be formalizable in an appropriate theory of bounded arithmetic. Typically, these algorithms are randomized, but for deterministic polynomial-time examples, one can take Rabin’s irreducibility test or the Tonelli–Shanks square-root algorithm (formulated so that a quadratic nonresidue is required as a part of the input).

$\endgroup$
10
$\begingroup$

The AKS primality test seems like a good candidate if Wikipedia is to be believed.

However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).

$\endgroup$
6
  • 2
    $\begingroup$ Indeed, Emil Jerabek has shown that even the correctness of the Miller-Rabin test is not provable in $S^1_2$ under standard non-collapsing assumptions. [Dual weak pigeonhole principle, Boolean complexity, and derandomization, APAL 129 (2004), 1-37] $\endgroup$ Apr 5, 2013 at 11:59
  • 2
    $\begingroup$ Actually, Emil's argument relies the fact that every prime satisfies Fermat's Little Theorem is not provable in $S^1_2$. The same reasoning applies here, under standard assumptions, it is not provable in $S^1_2$ that every prime passes the AKS test. $\endgroup$ Apr 5, 2013 at 12:10
  • 2
    $\begingroup$ There is a wonderful paper by Krajicek and Pudlak that gives a bunch more examples: karlin.mff.cuni.cz/~krajicek/j-crypto.ps $\endgroup$ Apr 5, 2013 at 13:05
  • 2
    $\begingroup$ @François, why not posting an answer? :) $\endgroup$
    – Kaveh
    Apr 5, 2013 at 14:14
  • 8
    $\begingroup$ So, I get the highest upvote count for making an early lucky guess, while others actually know what is going on. Math is just like MTV. $\endgroup$ Apr 5, 2013 at 19:33

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.