Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
Abstract
We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory \`a 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= is a well-studied theory based on bounded induction.
Cite
@article{arxiv.2311.15003,
title = {Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories},
author = {Melissa Antonelli and Ugo Dal Lago and Davide Davoli and Isabel Oitavem and Paolo Pistone},
journal= {arXiv preprint arXiv:2311.15003},
year = {2023}
}