eng
episciences.org
Logical Methods in Computer Science
1860-5974
2022-03-01
Volume 18, Issue 1
10.46298/lmcs-18(1:35)2022
6195
journal article
Hilbert's Tenth Problem in Coq (Extended Version)
Dominique Larchey-Wendling
Yannick Forster
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. Additionally, we prove the reverse direction and show that every
Diophantine relation is recognisable by $\mu$-recursive functions and give a
certified compiler from $\mu$-recursive functions to Minsky machines.
https://lmcs.episciences.org/6195/pdf
Computer Science - Logic in Computer Science