2026-08-01T08:15:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19653 2024-03-06T11:04:33Z ddc:004 open_access

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories Antonelli, Melissa Dal Lago, Ugo Davoli, Davide Oitavem, Isabel Pistone, Paolo Bounded Arithmetic Randomized Computation Implicit Computational Complexity 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 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Melissa Antonelli and Ugo Dal Lago and Davide Davoli and Isabel Oitavem and Paolo Pistone 2024 Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2024.10 urn:nbn:de:0030-drops-196538 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.10 eng https://creativecommons.org/licenses/by/4.0/legalcode