License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.27
URN: urn:nbn:de:0030-drops-105342
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10534/
Go to the corresponding LIPIcs Volume Portal

Larchey-Wendling, Dominique ; Forster, Yannick

Hilbert's Tenth Problem in Coq

pdf-format:
LIPIcs-FSCD-2019-27.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{larcheywendling_et_al:LIPIcs:2019:10534,
  author =	{Dominique Larchey-Wendling and Yannick Forster},
  title =	{{Hilbert's Tenth Problem in Coq}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{27:1--27:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10534},
  URN =		{urn:nbn:de:0030-drops-105342},
  doi =		{10.4230/LIPIcs.FSCD.2019.27},
  annote =	{Keywords: Hilbert's tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory}
}

Keywords: Hilbert's tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019
Supplementary Material: Coq formalisation of all results: https://uds-psl.github.io/H10, Coq library of undecidable problems: https://github.com/uds-psl/coq-library-undecidability

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI