Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

2023/11/25 by Antonelli, Melissa, Lago, Ugo Dal, Davoli, Davide +2
#F.1.3 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2311.15003

Abstract

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in the theory T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T where T=IΔ₀+Exp is a well-studied theory based on bounded induction.

Related

• An Arithmetic Theory for the Poly-Time Random Functions
• A polytime proof of correctness of the Rabin-Miller algorithm from Fermat's little theorem
• Deterministic Identity Testing for Sum of Read-Once Oblivious Arithmetic Branching Programs
• Probabilistic Recursion Theory and Implicit Computational Complexity (Long Version)
• A polytime complexity analyser for Probabilistic Polynomial Time over imperative stack programs