Document Open Access Logo

Hilbert’s Tenth Problem in Coq

Authors Dominique Larchey-Wendling , Yannick Forster

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.27.pdf
  • Filesize: 0.59 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Type theory
Keywords
  • Hilbert’s tenth problem
  • Diophantine equations
  • undecidability
  • computability theory
  • reduction
  • Minsky machines
  • Fractran
  • Coq
  • type theory

Metrics

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

Abstract

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem - in our case by a Minsky machine - is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN language as intermediate layer.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.27

Author Details

Dominique Larchey-Wendling
  • Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France
Yannick Forster
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Larchey-Wendling, Dominique: partially supported by the https://ticamore.logic.at/ project (http://www.agence-nationale-recherche.fr/?Projet=ANR-16-CE91-0002).

Acknowledgements

We would like to thank Gert Smolka, Dominik Kirst and Simon Spies for helpful discussion regarding the presentation.

Supplementary Materials

References

  1. Mario Carneiro. A Lean formalization of Matiyasevič’s theorem, 2018. URL: http://arxiv.org/abs/1802.01795.
  2. John H. Conway. FRACTRAN: A Simple Universal Programming Language for Arithmetic, pages 4-26. Springer New York, New York, NY, 1987. Google Scholar
  3. Martin Davis. Arithmetical problems and recursively enumerable predicates 1. The Journal of Symbolic Logic, 18(1):33-41, 1953. Google Scholar
  4. Martin Davis. Hilbert’s Tenth Problem is Unsolvable. The American Mathematical Monthly, 80(3):233-269, 1973. Google Scholar
  5. Martin Davis and Hilary Putnam. A computational proof procedure; Axioms for number theory; Research on Hilbert’s Tenth Problem. Air Force Office of Scientific Research, Air Research and Development, 1959. Google Scholar
  6. Martin Davis, Hilary Putnam, and Julia Robinson. The decision problem for exponential Diophantine equations. Annals of Mathematics, pages 425-436, 1961. Google Scholar
  7. Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. TYPES 2018, 2018. Google Scholar
  8. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-Related Computational Reductions in Coq. In ITP 2018, pages 253-269. Springer, 2018. Google Scholar
  9. Yannick Forster, Dominik Kirst, and Gert Smolka. On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. In CPP 2019, pages 38-51, 2019. Google Scholar
  10. Yannick Forster and Dominique Larchey-Wendling. Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic. Workshop on Syntax and Semantics of Low-level Languages, Oxford, 2018. Google Scholar
  11. Yannick Forster and Dominique Larchey-Wendling. Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. In CPP 2019, pages 104-117. ACM, 2019. URL: http://dx.doi.org/10.1145/3293880.3294096.
  12. Yannick Forster and Gert Smolka. Weak Call-By-Value Lambda Calculus as a Model of Computation in Coq. In ITP 2018, pages 189-206. Springer, 2017. Google Scholar
  13. 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
  14. Warren D. Goldfarb. The undecidability of the secondorder unification problem. Theoretical Computer Science, 13:225-230, 1981. Google Scholar
  15. David Hilbert. Mathematical problems. Bulletin of the American Mathematical Society, 8(10):437-479, 1902. Google Scholar
  16. J. P. Jones and Y. V. Matijasevič. Register Machine Proof of the Theorem on Exponential Diophantine Representation of Enumerable Sets. J. Symb. Log., 49(3):818-829, 1984. URL: http://dx.doi.org/10.2307/2274135.
  17. Dominique Larchey-Wendling. Typing Total Recursive Functions in Coq. In ITP 2017, pages 371-388. Springer, 2017. Google Scholar
  18. Edouard Lucas. Théorie des Fonctions Numériques Simplement Périodiques. [Continued]. American Journal of Mathematics, 1(3):197-240, 1878. Google Scholar
  19. Yuri V. Matijasevič. Enumerable sets are Diophantine. In Soviet Mathematics: Doklady, volume 11, pages 354-357, 1970. Google Scholar
  20. Yuri V. Matiyasevich. A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers. J. Math. Sci., 87(1):3228-3233, 1997. Google Scholar
  21. Yuri V. Matiyasevich. On Hilbert’s Tenth Problem. Expository Lectures 1, Pacific Institute for the Mathematical Sciences, University of Calgary, February 2000. URL: http://www.mathtube.org/sites/default/files/lecture-notes/Matiyasevich.pdf.
  22. Yuri V. Matiyasevich. Martin Davis and Hilbert’s Tenth Problem. In Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Springer, 2016. Google Scholar
  23. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  24. Karol Pąk. The Matiyasevich Theorem. Preliminaries. Formalized Mathematics, 25(4):315-322, 2017. Google Scholar
  25. Karol Pąk. Diophantine sets. Preliminaries. Formalized Mathematics, 26(1):81-90, 2018. Google Scholar
  26. 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
  27. Julia Robinson. Existential definability in arithmetic. Transactions of the American Mathematical Society, 72(3):437-449, 1952. Google Scholar
  28. Benedikt Stock et al. Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle. Isabelle Workshop 2018, 2018. URL: http://dx.doi.org/10.29007/3q4s.
  29. The Coq Proof Assistant. http://coq.inria.fr, 2019.
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