TY - GEN
T1 - Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
AU - Antonelli, Melissa
AU - Lago, Ugo Dal
AU - Davoli, Davide
AU - Oitavem, Isabel
AU - Pistone, Paolo
N1 - Funding Information:
Funding The first, second, third and fifth authors’ work is supported by the European Research Council through the project DIAPASoN ERC COoG 818616, and by the French “Agence Nationale de la Recherche” through the project PPS ANR-19-C48-0014. The first author’s work is supported by the Helsinki Institute for Information Technology. The third author’s work is supported by the French “Agence Nationale de la Recherche” through the project UCA DS4H ANR-17-EURE-0004. The fourth author’s work is supported by national funds through the “FCT-Fundação para a Ciência e a Tecnologia, I.P.”, through the projects UIDB/00297/2020 and UIDP/00297/2020 (Center for Mathematics and Applications).
Publisher Copyright:
© Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone; licensed under Creative Commons License CC-BY 4.0.
PY - 2024/2
Y1 - 2024/2
N2 - 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 BPPT and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPPT, where T = I∆0 + Exp is a well-studied theory based on bounded induction.
AB - 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 BPPT and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPPT, where T = I∆0 + Exp is a well-studied theory based on bounded induction.
KW - Bounded Arithmetic
KW - Implicit Computational Complexity
KW - Randomized Computation
UR - http://www.scopus.com/inward/record.url?scp=85185217364&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2024.10
DO - 10.4230/LIPIcs.CSL.2024.10
M3 - Conference contribution
AN - SCOPUS:85185217364
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024
A2 - Murano, Aniello
A2 - Silva, Alexandra
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024
Y2 - 19 February 2024 through 23 February 2024
ER -