Dominique Larchey-Wendling ; Yannick Forster - Hilbert's Tenth Problem in Coq (Extended Version)

lmcs:6195 - Logical Methods in Computer Science, March 1, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:35)2022
Hilbert's Tenth Problem in Coq (Extended Version)

Authors: 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.


    Volume: Volume 18, Issue 1
    Published on: March 1, 2022
    Accepted on: December 23, 2021
    Submitted on: March 11, 2020
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 401 times.
    This article's PDF has been downloaded 406 times.