Document Open Access Logo

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

Authors Melissa Antonelli , Ugo Dal Lago , Davide Davoli, Isabel Oitavem , Paolo Pistone

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.10.pdf
  • Filesize: 0.89 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof theory
Keywords
  • Bounded Arithmetic
  • Randomized Computation
  • Implicit Computational Complexity

Metrics

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 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.

Cite As Get BibTex

Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone. Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.10

Author Details

Melissa Antonelli
  • Helsinki Institute for Information Technology, Finland
Ugo Dal Lago
  • Bologna University, Italy
  • Inria, Université Côte d'Azur, Sophia Antipolis, France
Davide Davoli
  • Inria, Université Côte d'Azur, Sophia Antipolis, France
Isabel Oitavem
  • Center for Mathematics and Applications (NOVA Math), NOVA FCT, Caparica, Portugal
  • Department of Mathematics, NOVA FCT, Caparica, Portugal
Paolo Pistone
  • Bologna University, Italy

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).

References

  1. M. Antonelli, U. Dal Lago, D. Davoli, I. Oitavem, and P. Pistone. Enumerating error bounded polytime algorithms through arithmetical theories, 2023. URL: https://arxiv.org/abs/2311.15003.
  2. M. Antonelli, U. Dal Lago, and P. Pistone. On measure quantifiers in first-order arithmetic. In Proc. of CiE 2021, pages 12-24. Springer-Verlag, 2021. Google Scholar
  3. S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. Google Scholar
  4. S. Bellantoni and S. Cook. A New Recursion-Theoretic Characterization of the Polytime Functions. Computational Complexity, 2:97-110, 1992. Google Scholar
  5. P. Billingsley. Probability and Measure. Wiley, 1995. Google Scholar
  6. S. Buss, A.L. Kolodziejczyk, and N. Thapen. Fragments of Approximate Counting. Journal of Symbolic Logic, 79(2):496-525, 2014. Google Scholar
  7. S.R. Buss. Bounded Arithmetic. PhD thesis, Princeton University, 1986. Google Scholar
  8. S.R. Buss. First-Order Proof Theory of Arithmetic. In S.R: Buss, editor, Handbook of Proof Theory. Elsavier, 1998. Google Scholar
  9. A. Church. An Unsolvable Problem of Elementary Number Theory. American J. of Mathematics, 58(2):345-363, 1992. Google Scholar
  10. A. Cobham. The intrinsic computational difficulty of functions. In Proc. of the 1964 International Congress on Logics, Methodology and Philosophy of Science, pages 24-30. North-Holland Publishing, 1965. Google Scholar
  11. E.F. Codd. Relational Completeness of Data Base Sublanguages. In Proc. of 6th Courant Computer Science Symposium., pages 65-98, 1972. Google Scholar
  12. S. Cook. The Complexity of Theorem Proving Procedures. In Proc. of STOC 1971, pages 151-158, 1971. Google Scholar
  13. S. Cook and A. Urquhart. Functional Interpretations of Feasibly Constructive Arithmetic. Annals of Pure and Applied Logic, 63(2):103-200, 1993. Google Scholar
  14. S.A. Cook. Feasibly constructive proofs and the propositional calculus. In ACM Press, editor, Proc. of STOC 1975, pages 83-97, 1975. Google Scholar
  15. S.A. Cook and R.A. Reckhow. Efficiency of Propositional Proof Systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  16. C. Cornaros and C. Dimitracopoulos. The Prime Number Theorem and Fragments of PA. Archive for Mathematical Logic, 33:265-281, August 1994. Google Scholar
  17. H. B. Curry. Functionality in Combinatory Logic. Proceedings of the National Academy of Sciences, 20(11):584-590, 1934. Google Scholar
  18. U. Dal Lago, R. Kahle, and I. Oitavem. A Recursion-Theoretic Characterization of the probabilistic Class PP. In Proc. of MFCS 2021, pages 1-12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  19. U. Dal Lago, R. Kahle, and I. Oitavem. Implicit Recursion-Theoretic Characterizations of Counting Classes. Archive for Mathematical Logic, May 2022. Google Scholar
  20. U. Dal Lago and P. Parisen Toldin. A Higher-Order Characterization of Probabilistic Polynomial Time. Information and Computation, 241:114-141, 2015. Google Scholar
  21. K. Eickmeyer and M. Grohe. Randomisation and Derandomisation in Descriptive Complexity Theory. In Proc. of CSL 2010. Springer, 2010. Google Scholar
  22. R. Fagin. Generalized first-order spectra and polynomial-time recognizable sets. Complexity of computation, 7:43-73, 1974. Google Scholar
  23. F. Ferreira. Polynomial-Time Computable Arithmetic and Conservative Extesions. Ph.D. Dissertation, December 1988. Google Scholar
  24. F. Ferreira. Polynomial-Time Computable Arithmetic. In W. Sieg, editor, Logic and Computation, volume 106 of Contemporary Mathematics, pages 137-156. AMS, 1990. Google Scholar
  25. F. Ferreira. Stockmeyer induction, pages 161-180. Birkhäuser Boston, Boston, MA, 1990. URL: https://doi.org/10.1007/978-1-4612-3466-1_9.
  26. G. Ferreira and I. Oitavem. An Interpretation of S¹₂ in Σ^b₁-NIA. Portugaliae Mathematica, 63:137-156, 2006. Google Scholar
  27. L. Fortnow. Comparing notions of full derandomization. In Proceedings of the 16th Annual IEEE Conference on Computational Complexity, pages 28-34, Chicago, IL, USA, 2001. IEEE Computer Society. Google Scholar
  28. H. Gaifman and C. Dimitracopoulos. Fragments of Peano’s arithmetic and the MRDP theorem. Logic and Algorithmic, Monograph. Enseign. Math., 30:187-206, 1982. Google Scholar
  29. D. Gajser. Verifying Time Complexity of Turing Machines. Informatica, 40:369-370, 2016. Google Scholar
  30. J.-Y. Girard. Light Linear Logic. Information and Computation, 2(143):175-204, 1998. Google Scholar
  31. J.-Y. Girard and Y. Lafont. Advances in Linear Logic. Cambridge University Press, 1995. Google Scholar
  32. J.-Y. Girard, A. Scedrov, and P. Scott. Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theoretical Computer Science, 97(1):1-66, 1992. Google Scholar
  33. K. Gödel. Über Formal Unentscheidbare Sätze der Principia Mathematica and Verwandter Systeme. Monatshefte für Mathematik und Physik, 38:173-198, 1931. Google Scholar
  34. P. Hájek. Arithmetical Hierarchy and Complexity of Computation. Theoretical Computer Science, 8(2):227-237, 1979. Google Scholar
  35. P. Hájek and P. Pudlák. Metamathematics of First-Order Arithmetic. Springer, Berlin-Heidelberg, 1998. Google Scholar
  36. J. Hartmanis and R.E. Stearns. On the Computational Complexity of Algorithms. Transactions of the AMS, 117:285-306, 1965. Google Scholar
  37. M. Hofmann. Programming Languages Capturing Complexity Classes. SIGACT News, 31(1):31-42, March 2000. Google Scholar
  38. H. A. Howard. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980. Google Scholar
  39. N. Immerman. Descriptive Complexity. Springer, 1999. Google Scholar
  40. E. Jeřábek. Dual Weak Pigeonhole Principle, Boolean Complexity, and Derandomization. Annals of Pure and Applied Logic, 129(1):1-37, 2004. Google Scholar
  41. E. Jeřábek. Approximate Counting in Bounded Arithmetic. Journal of Symbolic Logic, 72(3):959-993, 2007. Google Scholar
  42. J. Krajíček and P. Pudlák. Propositional Proof Systems, the Consistency of First-Order Theories and the Complexity of Computations. Journal of Symboic Logic, 54(3):1063-1079, 1989. Google Scholar
  43. J. Krajíček, P. Pudlák, and G. Takeuti. Bounded Arithmetic and the Polynomial Hierarchy. Annals of Pure and Applied Logic, 52:143-153, 1991. Google Scholar
  44. Y. Lafont. Soft Linear Logic and Polynomial Time. Theoretical Computer Science, 1/2(318):163-180, 2004. Google Scholar
  45. D. Leivant. Ramified Recurrence and Computational Complexity I: Word Recurrence and Polytime. In P. Clote and J. Remmel, editors, Feasible Mathematics II, pages 320-343. Springer, 1995. Google Scholar
  46. H. Michalewski and M. Mio. Measure Quantifiers in Monadic Second Order Logic. In Proc. of LFCS, pages 267-282, Cham, 2016. Springer. Google Scholar
  47. J. Mitchell, M. Mitchell, and A. Scedrov. A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time. In Proc. of FOCS 1998, pages 725-733. IEEE Computer Society, 1998. Google Scholar
  48. C. Morgenstern. The Measure Quantifier. Journal of Symbolic Logic, 44(1):103-108, 1979. Google Scholar
  49. R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, Cambridge; NY, 1995. Google Scholar
  50. C.H. Papadimitriou. Computational Complexity. Pearson Education, 1993. Google Scholar
  51. R. Parikh. Existence and Feasibility in Arithmetic. Journal of Symbolic Logic, 36:494-508, 1971. Google Scholar
  52. P. Pudlák and N. Thapen. Random Resolution Refutations. Computational Complexity, 28:185-239, 2019. Google Scholar
  53. E.S. Santos. Probabilistic Turing Machines and Computability. AMS, 22(3):704-710, 1969. Google Scholar
  54. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. Google Scholar
  55. A. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proc. London Mathematical Society, pages 2-42, 230-265, 1936-37. Google Scholar
  56. G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT press, 1993. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact