Document Open Access Logo

Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq

Authors Yannick Forster , Felix Jahn



PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.21.pdf
  • Filesize: 0.9 MB
  • 21 pages

Document Identifiers

Author Details

Yannick Forster
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
  • Inria, Gallinette Project-Team, Nantes, France
Felix Jahn
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Acknowledgements

We thank Dominik Kirst, Gert Smolka, Lennard Gäher, and Andrej Dudenhefner for discussions and feedback on the drafts of this paper, as well as the reviewers for their comments.

Cite AsGet BibTex

Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.21

Abstract

We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post’s problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post’s problem for truth-table reducibility). In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • type theory
  • computability theory
  • constructive mathematics
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  2. Andrej Bauer. Synthetic mathematics with an excursion into computability theory. University of Wisconsin Logic seminar, 2021. URL: http://math.andrej.com/asset/data/madison-synthetic-computability-talk.pdf.
  3. Douglas Bridges and Fred Richman. Varieties of constructive mathematics, volume 97. Cambridge University Press, 1987. Google Scholar
  4. Nigel Cutland. Computability: An introduction to recursive function theory. Cambridge university press, 1980. Google Scholar
  5. James C. E. Dekker. A theorem on hypersimple sets. Proceedings of the American Mathematical Society, 5:791-796, 1954. Google Scholar
  6. Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
  7. Yannick Forster. Computability in Constructive Type Theory. PhD thesis, Saarland University, 2021. URL: https://doi.org/10.22028/D291-35758.
  8. Yannick Forster. Parametric Church’s Thesis: Synthetic computability without choice. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 70-89, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-93100-1_6.
  9. Yannick Forster and Dominik Kirst. Synthetic Turing reducibility in constructive type theory. 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022. Google Scholar
  10. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38-51, 2019. Google Scholar
  11. Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.17.
  12. Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. working paper or preprint, March 2022. URL: https://hal.inria.fr/hal-03596267.
  13. Richard M Friedberg and Hartley Rogers Jr. Reducibility and completeness for sets of integers. Mathematical Logic Quarterly, 5(7-13):117-125, 1959. URL: https://doi.org/10.1002/malq.19590050703.
  14. Felix Jahn. Synthetic One-One, Many-One, and Truth-Table Reducibility in Coq. Bachelor’s thesis, Saarland University, 2020. Google Scholar
  15. Steven C. Kleene and Emil L. Post. The upper semi-lattice of degrees of recursive unsolvability. The Annals of Mathematics, 59(3):379, May 1954. URL: https://doi.org/10.2307/1969708.
  16. Georg Kreisel. Mathematical logic. Lectures in modern mathematics, 3:95-195, 1965. URL: https://doi.org/10.2307/2315573.
  17. Bassel Mannaa and Thierry Coquand. The independence of markov’s principle in type theory. Logical Methods in Computer Science, 13, 2017. Google Scholar
  18. Andrei Andreevich Markov. The theory of algorithms. Trudy Matematicheskogo Instituta Imeni VA Steklova, 42:3-375, 1954. Google Scholar
  19. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  20. Albert Abramovich Munik. On strong and weak reducibility of algorithmic problems. Sibirskii Matematicheskii Zhurnal, 4(6):1328-1341, 1963. Google Scholar
  21. Piergiorgio Odifreddi. Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier, 1992. Google Scholar
  22. Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. Google Scholar
  23. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option. In European Symposium on Programming, pages 245-271. Springer, 2018. Google Scholar
  24. Emil L Post. Recursively enumerable sets of positive integers and their decision problems. bulletin of the American Mathematical Society, 50(5):284-316, 1944. Google Scholar
  25. Emil L. Post. Degrees of recursive unsolvability - preliminary report. In Bulletin of the American Mathematical Society, volume 54, pages 641-642. American Mathematical Society (AMS), 1948. Google Scholar
  26. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  27. Hartley Rogers. Theory of recursive functions and effective computability. CUMINCAD, 1987. Google Scholar
  28. Robert I Soare. Recursively enumerable sets and degrees: A study of computable functions and computably generated sets. Springer Science & Business Media, 1999. Google Scholar
  29. The Coq Development Team. The Coq Proof Assistant, version 8.11.0. https://doi.org/10.5281/zenodo.3744225, January 2020.
  30. The Coq std++ Team. An extended "standard library" for Coq. https://gitlab.mpi-sws.org/iris/stdpp, 2020.
  31. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. vol. i, volume 121 of. Studies in Logic and the Foundations of Mathematics, 26, 1988. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail