Document Open Access Logo

Formalizing Computability Theory via Partial Recursive Functions

Author Mario Carneiro

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2019.12.pdf
  • Filesize: 481 kB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Recursive functions
  • Theory of computation → Interactive proof systems
Keywords
  • Lean
  • computability
  • halting problem
  • primitive recursion

Metrics

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

Abstract

We present an extension to the mathlib library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply Gödel numberings where needed and encapsulate the encoding details.

Cite As Get BibTex

Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.12

Author Details

Mario Carneiro
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by AFOSR grant FA9550-18-1-0120 and a grant from the Sloan Foundation.

Acknowledgements

I would like to thank my advisor Jeremy Avigad for his support and encouragement, and for his reviews of early drafts of this work, as well as Yannick Forster, Rob Y. Lewis, and the anonymous reviewers for their many helpful comments.

Supplementary Materials

References

  1. Andrea Asperti and Wilmer Ricciotti. Formalizing turing machines. In International Workshop on Logic, Language, Information, and Computation, pages 1-25. Springer, 2012. Google Scholar
  2. Andrej Bauer. First Steps in Synthetic Computability Theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  3. Alonzo Church. An unsolvable problem of elementary number theory. American journal of mathematics, 58(2):345-363, 1936. Google Scholar
  4. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-388. Springer, 2015. Google Scholar
  5. 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. ACM, 2019. Google Scholar
  6. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 104-117. ACM, 2019. Google Scholar
  7. Yannick Forster and Gert Smolka. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In ITP, 2017. Google Scholar
  8. Kurt Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme i. Monatshefte für mathematik und physik, 38(1):173-198, 1931. Google Scholar
  9. Martin Hofmann. Programming languages capturing complexity classes. ACM SIGACT News, 31(1):31-42, January 2000. URL: https://doi.org/10.1145/346048.346051.
  10. Stephen Cole Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41-73, 1943. Google Scholar
  11. Dominique Larchey-Wendling. Typing total recursive functions in Coq. In International Conference on Interactive Theorem Proving, pages 371-388. Springer, 2017. Google Scholar
  12. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  13. Michael Norrish. Mechanised computability theory. In International Conference on Interactive Theorem Proving, pages 297-311. Springer, 2011. Google Scholar
  14. Alan J Perlis. Special feature: Epigrams on programming. ACM Sigplan Notices, 17(9):7-13, 1982. Google Scholar
  15. Thiago Mendonça Ferreira Ramos, César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, and Anthony Narkawicz. Formalization of the Undecidability of the Halting Problem for a Functional Language. In International Workshop on Logic, Language, Information, and Computation, pages 196-209. Springer, 2018. Google Scholar
  16. Alan M Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London mathematical society, 2(1):230-265, 1937. Google Scholar
  17. Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising turing machines and computability theory in Isabelle/HOL. In International Conference on Interactive Theorem Proving, pages 147-162. Springer, 2013. Google Scholar
  18. Vincent Zammit. A proof of the S^m_n theorem in Coq. Technical Report 9-97, University of Kent, 1997. 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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact