Dominique Larchey-Wendling
email: dominique.larchey-wendling@loria.fr

Yannick Forster
email: forster@ps.uni-saarland.de

Hilbert's Tenth Problem in Coq

Keywords: 2012 ACM Subject Classification Theory of computation → Models of computation; Theory of computation Hilbert's tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory Digital Object Identifier 10.4230/LIPIcs.FSCD.2019.27

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.

Introduction

Hilbert's tenth problem (H10) was posed by David Hilbert in 1900 as part of his famous 23 problems [START_REF] Hilbert | Mathematical problems[END_REF] and asked for the "determination of the solvability of a Diophantine equation. " A Diophantine equation1 is a polynomial equation over natural numbers (or, equivalently, integers) with constant exponents, e.g. x 2 + 3z = yz + 2. When Hilbert asked for "determination, " he meant, in modern terms, a decision procedure, but computability theory was yet several decades short of being developed.

The first undecidable problems found by Church, Post and Turing were either native to mathematical logic or dependent on a fixed model of computation. H10, to the contrary, can be stated to every mathematician and its formulation is independent from a model of computation. Emil Post stated in 1944 that H10 "begs for an unsolvability proof" [START_REF] Post | Recursively enumerable sets of positive integers and their decision problems[END_REF]. From a computational perspective, it is clear that H10 is recursively enumerable (or recognisable), meaning there is an algorithm that halts on a Diophantine equation iff it is solvable.

27:2 Hilbert's Tenth Problem in Coq

Post's student Martin Davis conjectured that even the converse is true, i.e. that every recognisable set is also Diophantine. More precisely, he conjectured that if A ⊆ N k is recognisable then (a 1 , . . . , a k ) ∈ A ↔ ∃x 1 . . . x n , P (a 1 , . . . , a k , x 1 , . . . , x n ) = 0 holds for some polynomial P in k + n variables. He soon improved on a result by Gödel [START_REF] Gödel | Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I[END_REF] and gave a proof of his conjecture, however requiring up to one bounded universal quantification [START_REF] Davis | Arithmetical problems and recursively enumerable predicates 1[END_REF]: (a 1 , . . . , a k ) ∈ A ↔ ∃z, ∀y < z, ∃x 1 . . . x n , P (a 1 , . . . , a k , x 1 , . . . , x n , y, z) = 0. Davis and Putnam [START_REF] Davis | A computational proof procedure; Axioms for number theory[END_REF] further improved on this, and showed that, provided a certain number-theoretic assumption holds, every recognisable set is exponentially Diophantine, meaning variables are also allowed to appear in exponents. Julia Robinson then in 1961 modified the original proof to circumvent the need for the assumption, resulting in the DPR theorem [START_REF] Davis | The decision problem for exponential Diophantine equations[END_REF], namely that every recognisable set is exponentially Diophantine. Due to another result from Robinson [START_REF] Robinson | Existential definability in arithmetic[END_REF], the gap now only consisted of proving that there is a Diophantine equation exhibiting exponential growth. In 1970, Yuri Matiyasevich showed that the Fibonacci sequence grows exponentially while being Diophantine, closing the gap and finishing the proof of the theorem nowadays called DPRM theorem, ultimately establishing that exponentiation is Diophantine itself [START_REF] Matijasevič | Enumerable sets are Diophantine[END_REF] (known as "Matiyasevich's theorem").

Even the most modern and simpler proofs of the DPRM theorem still require many preliminaries and complicated number-theoretic ideas, for an overview see [START_REF] Matiyasevich | Martin Davis and Hilbert's Tenth Problem[END_REF]. We formalise one such proof as part of our ongoing work on a library of undecidable problems [START_REF] Forster | Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic[END_REF] in the proof assistant Coq [START_REF]The Coq Proof Assistant[END_REF]. Since H10 is widely used as a seed [START_REF] Dudenhefner | A Simpler Undecidability Proof for System F Inhabitation[END_REF][START_REF] Goldfarb | The undecidability of the secondorder unification problem[END_REF] for showing the undecidability of problems using many-one reductions, this will open further ways of extending the library. Given that our library already contains a formalisation of Minsky machines [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF], we follow the approach of Jones and Matijasevič [START_REF] Jones | Register Machine Proof of the Theorem on Exponential Diophantine Representation of Enumerable Sets[END_REF], who use register machines, being very well-suited since they already work on numbers. They encode full computations of register machines as Diophantine equations in one single, monolithic step. To make the proof more tractable for both mechanisation and explanation, we factor out an intermediate language, John Conway's FRACTRAN [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF], which can simulate Minsky machines.

We first introduce three characterisations of Diophantine equations over natural numbers, namely Diophantine logic DIO_FORM (allowing to connect Diophantine equations with conjunction, disjunction and existential quantification), elementary Diophantine constraints DIO_ELEM (a finite set of constraints on variables, oftentimes used for reductions [START_REF] Dudenhefner | A Simpler Undecidability Proof for System F Inhabitation[END_REF][START_REF] Goldfarb | The undecidability of the secondorder unification problem[END_REF]) and single Diophantine equations DIO_SINGLE, including parameters, as described above. H10 then asks about the solvability of single Diophantine equations with no parameters.

Technically, the reduction chain to establish the unsolvability of H10 starts at the halting problem for single-tape Turing machines Halt, reduced to the Post correspondence problem PCP in [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF]. In previous work [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF] we have reduced PCP to a specialised halting problem for Minsky machines, which we use here in a slightly generalised form as MM. We then reduce Minsky machine halting to FRACTRAN termination. FRACTRAN is very natural to describe using polynomials, and the encoding does not rely on any complicated construction. The technical difficulty then only lies in the Diophantine encoding of the reflexive-transitive closure of a relation which follows from the direct elimination of bounded universal quantification, given that the proof in [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] involves no detour via models of computation. In total, we obtain the following chain of reductions to establish the undecidability of H10:

Halt PCP MM FRACTRAN DIO_FORM DIO_ELEM DIO_SINGLE H10

In the present paper, we focus on explaining this factorisation of the proof and give some details for the different stages. While we contribute Coq mechanisations of Matiyasevich's theorem and the elimination of bounded universal quantification, we treat them mainly as black-boxes and only elaborate on their challenging formalisation rather than the proofs themselves, a good explanation of which would anyways not fit in the given page limit.

To the best of our knowledge, we are the first to give a full verification of the DPRM theorem and the undecidability of Hilbert's tenth problem in a proof assistant. We base the notion of recognisability in the DPRM theorem on Minsky machines.

When giving undecidability proofs via many-one reductions, it is critical to show that all reduction functions are actually computable. We could in theory verify the computability of all functions involved using an explicit model of computation. In pen-and-paper proofs, this approach is however almost never used, because implementing high-level mathematical transformations as provably correct low-level programs is a daunting task. Instead, we rely on a synthetic approach [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF][START_REF] Forster | On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem[END_REF][START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF] based on the computability of all functions definable in Coq's constructive type theory, which is closer to the practice of pen-and-paper proofs. In this approach, a problem P is considered undecidable if there is a reduction from an obviously undecidable problem, e.g. Halt P .

The axiom-free Coq formalisation of all the results in this paper is available online and the main lemmas and theorems in the pdf version of the paper are hyper-linked with the html version of the source code at https://uds-psl.github.io/H10. Starting from our already existing library which included most of the Minsky machine code [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF], the additional code for proving the undecidability of H10 and the DPRM theorem consists of about 8k loc including 3k loc for Matiyasevich's results alone, together with a 4k loc addition to our shared libraries; see Appendix A for more details. The paper itself can be read without in-depth knowledge of Coq or type theory.

Contribution.

Apart from the full formalisation, we consider the novel refactoring of the proof via FRACTRAN a contribution to the explainability of the DPRM theorem.

Preliminaries. Regarding notation, we may write x.y for multiplication of natural numbers x, y : N and we will leave out the symbol where convenient. We write L X for the type of lists over X and l + + l for the concatenation of two lists. We write X n for vectors v over type X with length n, and F n for the finite type with exactly n elements. For p : F n , we write v[p] for the p-th component of v : X n . Notations for lists are overloaded for vectors. If P : X → P is a predicate (on X) and Q : Y → P is a predicate, we write P Q if there is a function f : X → Y s.t. ∀x : X, P x ↔ Q(f x), i.e. a many-one reduction from P to Q.

Diophantine Relations

Diophantine relations are composed of polynomials over natural numbers. There are several equivalent approaches to characterise these relations and oftentimes, the precise definition is omitted from papers. Basically, one can form equations between polynomial expressions and then combine these with conjunctions, disjunctions, and existential quantification. 2 For instance, these operations are assumed as Diophantine producing operators in e.g. [START_REF] Jones | Register Machine Proof of the Theorem on Exponential Diophantine Representation of Enumerable Sets[END_REF][START_REF] Matijasevič | Enumerable sets are Diophantine[END_REF][START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF][START_REF] Matiyasevich | On Hilbert's Tenth Problem[END_REF]. Sometimes, Diophantine relations are restricted to a single polynomial equation. Sometimes, the exponentiation function x, y → x y is assumed as Diophantine [START_REF] Jones | Register Machine Proof of the Theorem on Exponential Diophantine Representation of Enumerable Sets[END_REF]. To complicate the picture, Diophantine relations might equivalently range over Z (instead of N) but expressions like x y implicitly assume that y never gets a negative value.

Although seemingly diverging, these approaches are not contradictory because in the end, they characterise the same class of relations on natural numbers. However, mechanisation does not allow for such implicit assumptions. To give some mechanisable structure to some 2 Universal quantification or negation are not accepted as is.

Diophantine Logic

We define the types D expr of Diophantine expressions and D form of Diophantine formulae for the abstract syntax of Diophantine logic. Diophantine expressions are polynomials built from natural number constants and variables. An atomic Diophantine logic formula is just expressing the identity between two Diophantine expressions and we combine those with binary disjunction, binary conjunction, and existential quantification.

p, q : D expr ::

= x i : V | n : N | p + q | p × q A, B : D form ::= p = q | A ∧ B | A ∨ B | ∃ A
The letters p, q ranges over expressions and the letters A, B range over formulae. We use standard De Bruijn syntax with variables x 0 , x 1 , . . . of type V := N for better readability.

If we have x i : V, we write x 1+i for the next variable in V. As an example, the meta-level formula ∃y, (y = 0 ∧ ∃z, y = z + 1) would be represented as ∃(x 0 = 0 ∧ ∃(x 1 = x 0 + 1)), i.e. the variable x i refers to the i-th binder in the context. We provide a semantics for Diophantine logic. Given a valuation for variables ν : V → N, we define the interpretation p ν : N of the expression p : D expr by recursion:

x i ν := ν x i n ν := n p + q ν := p ν + q ν p × q ν := p ν × q ν
The interpretation of formulae cannot be done with a constant valuation ν : V → N because of existential quantifiers. The interpretation A ν of the formula A : D form is given by the following recursive rules:

A ∧ B ν := A ν ∧ B ν p = q ν := p ν = q ν A ∨ B ν := A ν ∨ B ν ∃ A ν := ∃n : N, A n•ν with n•ν (x 0 ) := n n•ν (x 1+i ) := ν x i
where n•ν : V → N is the standard De Bruijn extension of a valuation ν by n.

We give a first formal characterisation of Diophantine polynomial expressions D P and Diophantine relations D R . Diophantine polynomials are represented by some members of type f : (V → N) → N mapping valuations ν to values f ν : N which must moreover arise as instances of λν. p ν for some p : D expr . And Diophantine relations are members of type R : (V → N) → P arising as instances of λν. A ν . We give an informative content to these sub-types of (V → N) → N and (V → N) → P to be able to do some computations with the witness (either p or A) of Diophantineness, typically when moving to another formal representation like elementary Diophantine constraints in Section 3.

Definition 1.

We define the class of Diophantine polynomials and Diophantine relations as informative sub-types of (V → N) → N and (V → N) → P respectively:

D P f := p : D expr , ∀ν, p ν = f ν D R R := A : D form , ∀ν, A ν ↔ R ν
Note that Σ denotes type-theoretic dependent pairs. Hence an inhabitant w of D R R is a (dependent) pair (A, H A ) where A = π 1 (w) is a Diophantine formula and H A = π 2 (w) a proof that A (•) and R are extensionally equivalent. With these definitions, we will show that the sub-types D P and D R have the desired closure properties: D P contains variables, constants and is closed under the + and × pointwise operators over (V → N) → N; D R contains polynomial equations and is closed under conjunction, disjunction and existential quantification. Proposition 2. Let x i : V, n : N, and f, g : (V → N) → N be s.t. D P f and D P g hold.

Then D P (λν.ν x i ) , D P (λν.n) , D P (λν.f ν + g ν ) and D P (λν.f ν × g ν ) hold. Proposition 3. Let f , g be s.t. D P f and D P g hold. Then D R (λν.True) , D R (λν.False) , D R (λν.f ν = g ν ) , D R (λν.f ν ≤ g ν ) , D R (λν.f ν < g ν ) and D R (λν.f ν = g ν ) hold.
Proof. For e.g. λν. f ν < g ν , we first get the witnesses for w f : D P f and w g : D P g by the projections p f := π 1 (w f ) and p g := π 1 (w g ). If we denote by ρ the "lift by one renaming" ρ := λx i .x 1+i and then the witness ∃ 1 +x 0 +ρ (p f ) = ρ (p g ) can be used for λν. f ν < g ν .

From a mechanisation point of view, having to provide explicit witnesses is a painful task and we now describe how it can be almost entirely automated. We use the Coq unification mechanism to analyse a meta-level expression of Diophantine shape and reflect it into the corresponding object-level witness of types either D expr or D form together with the proof that it is an appropriate witness. The following lemma provides a way to process a goal such as D R R depending on the meta-level syntax of R. Lemma 4. Let R, S : (V → N) → P and T : N → (V → N) → P. We have the maps:

1. D R R → D R S → D R (λν.R ν ∧ S ν) 2. D R R → D R S → D R (λν.R ν ∨ S ν) 3. D R λν.T (ν x 0 ) (λx i .ν x 1+i ) → D R λν.∃u, T u ν 4. (∀ν, S ν ↔ R ν) → D R R → D R S .
With maps 1-3, we cope with conjunction, disjunction, existential quantification. Atomic or already established Diophantine relations are captured by Propositions 2 and 3 or later established results which are declared as hints for Coq proof-search tactics. The map number 4 provides a way to replace D R S with D R R once a proof that they are logically equivalent is established. Hence, if S cannot be analysed because it does not currently have a Diophantine shape, it can still be replaced by an equivalent relation R, hopefully better behaved.

Example of a Mechanised Diophantineness Proof

With the example of the "does not divide" relation u v := ¬(∃k, v = k × u), we describe how to use those results to automate the production of the object-level D R witness A of Definition 1 from the meta-level representation of a relation of Diophantine shape.

Proposition 5 . ∀f g : (V → N) → N, D P f → D P g → D R (λν.f ν g ν ).
Proof. u v := ¬(∃k, v = k×u) obviously is not in Diophantine shape. We thus first prove the equivalence u v ↔ (u = 0∧v = 0∨∃a b, v = a×u+b∧0 < b < u) and this new expression now has a Diophantine shape, relying on the Diophantine shape of Euclidean division. Using this equivalence in combination with map 4 of Lemma 4, we replace the goal D R (λν.f ν g ν ) with

D R (λν.f ν = 0 ∧ g ν = 0 ∨ ∃a b, g ν = a × f ν + b ∧ 0 < b ∧ b < f ν )
and then apply maps 1-3 of Lemma 4 until a shape such as those of Proposition 3 appears.

Once established, we can add the map D P f → D P g → D R (λν.f ν g ν ) in the Diophantine hint database so that later encountered proof goals D R (λν.f ν g ν ) can be immediately solved. We implemented the Coq tactic dio_rel_auto to automate all this work. Apart from the equivalence for u v and its proof, which cannot be guessed, the rest is effortless.

The recovery of witnesses of Definition 1 from meta-level syntax is automatic and hidden by the use of the dio_rel_auto tactic associated with the ever growing hint database. This way, we can proceed as in e.g. Matiyasevich papers where he just transforms a relation into an equivalent Diophantine shape, accumulating more and more Diophantine shapes on the way. This is a very welcome simplification over having to program witnesses by hand.

Exponentiation and Bounded Universal Quantification

For now, we introduce the elimination of the exponential relation and then of bounded universal quantification as black boxes expressed in the theory of Diophantine relations. However we do contribute implementations for both of these hard results. It is not possible for these two mechanised proofs to be described in detail given the page limit. Nonetheless we postpone some remarks and discussions about these proofs in Section 5.

Theorem 6 (Exponential). ∀f g h,

D P f → D P g → D P h → D R λν.f ν = g hν ν .
To prove it, one needs a meta-level Diophantine shape for the exponential relation, the proof of which is nothing short of extraordinary. This landmark result is due to Matiyasevich [START_REF] Matijasevič | Enumerable sets are Diophantine[END_REF], but we have implemented the shorter and more up-to-date proof of [START_REF] Matiyasevich | On Hilbert's Tenth Problem[END_REF].

Theorem 7 (Bounded U. Quantification). For f : (V → N) → N and T : N → (V → N) → P, we have a map D P f → D R λν.T (ν x 0 ) (λx i .ν x 1+i ) → D R λν.∀u, u < f ν → T u ν .
This map can be compared with map 3 of Lemma 4 and allows to recognise bounded universal quantification as a legitimate Diophantine shape. We have implemented the direct proof of Matiyasevich [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] which does not involve a detour through a model of computation. Notice that the bound f ν in ∀u, u < f ν → . . . is not constant otherwise the elimination of the quantifier would proceed as a simple reduction to a finitary conjunction.

Reflexive-Transitive Closure is Diophantine

With these tools -elimination of the exponential relation and of bounded universal quantification -we can show that the reflexive and transitive closure of a Diophantine binary relation is itself Diophantine. We assume a binary relation R : N → N → P over natural numbers. The Diophantineness of R can be formalised by assuming that e.g. λν.R (ν x 1 ) (ν x 0 ) is a Diophantine relation. We show that the i-th iterate of R is Diophantine (where i is non-constant).

Lemma 8 . Under hypothesis H

R : D R λν.R (ν x 1 ) (ν x 0 ) , for any f, g, i : (V → N) → N we have a map D P f → D P g → D P i → D R λν.R iν f ν g ν .
Proof. Using Euclidean division, we define the is_digit c q n d predicate stating that d is the n-th digit of the base q development of number c, as a Diophantine sentence:

is_digit c q n d := d < q ∧ ∃a b t, t = q n ∧ c = (a.q + d).t + b ∧ b < t
The Diophantineness of this follows from Theorem 6. Then we define the is_seq R c q i predicate stating that the first i + 1 digits of c in base q form an R-chain, again with a Diophantine expression by H R and Theorem 7:

is_seq R c q i := ∀n, n < i → ∃u v, is_digit c q n u ∧ is_digit c q (1 + n) v ∧ R u v
Then we encode R i u v by stating that there exists a (large enough) q and a number c such that the first i + 1 digits of c in base q form an R-chain starting at u and ending at v: R i u v ↔ ∃q c, is_seq R c q i ∧ is_digit c q 0 u ∧ is_digit c q i v and this expression is accepted as Diophantine by Lemma 4.

Proof. We show the result by structural induction on A.

If A is p = q with p, q : D expr then we encode p and q as a directed list of constraints. See Appendix B for a detailed explanation on an example;

When A is B ∧ C,

Single Diophantine Equations

In this section, we show how a list of elementary Diophantine constraints can be simulated by a single identity between two Diophantine polynomials. We use the following well known convexity identity to achieve the reduction, the proof of which can be found in Appendix C. Proposition 13 . Let (p 1 , q 1 ), . . . , (p n , q n ) be a sequence of pairs in N × N. Then

n i=1 2p i q i = n i=1 p 2 i + q 2 i ↔ p 1 = q 1 ∧ • • • ∧ p n = q n .
We define Diophantine polynomials similar to the Diophantine expressions D expr of Section 2.1 except that we now distinguish the types of bound variables (i.e. U) and of parameters (or free variables) (i.e. V) and that the types U and V are not fixed copies of N anymore, but type parameters of arbitrary value. Definition 14 . The type of Diophantine polynomials D poly (U, V) and the type of single Diophantine equations D single (U, V) are defined by: p, q : D poly (U, V)

::= u : U | x i : V | n : N | p + q | p × q E : D single (U, V) ::= p = q
For ϕ : U → N and ν : V → N we define the semantic interpretations of polynomials p ϕ ν : N and single Diophantine equations E ϕ ν : P in the obvious way.

Theorem 15 . For any list l : L D cstr of elementary Diophantine constraints, one can compute a single Diophantine equation

E : D single (N, N) such that ∀ν∀ϕ, E ϕ ν ↔ l ϕ ν .
Proof. We write l = [p 1 = q 1 ; . . . ; p n = q n ] and then use Proposition 13. In the code, we moreover show that the size of E is linear in the length of l. If needed, one could also show that the degree of the polynomial is less than 4.

Corollary 16 . Let R : (V → N) → P. Assuming D R R, one can compute a single Diophantine equation p = q : D single (N, V) such that ∀ν, R ν ↔ ∃ϕ, p ϕ ν = q ϕ ν .
Proof. Direct combination of Definition 1 and Theorems 10 and 15. In the formalisation, we also show that the size of the obtained single Diophantine equation is linearly bounded by the size of the witness formula contained in the proof of D R R.

We have shown that the automation we designed to recognise relations of Diophantine shape entail that these relations are also definable by satisfiability of a single equation between Diophantine polynomials, so these tools are sound w.r.t. a formally restrictive characterisation of Diophantineness. One could argue that the above existential quantifier ∃ϕ encodes infinitely many existential quantifiers but it can easily be replaced by finitely many existential quantifiers over the bound variables that actually occur in p or q. Proposition 17 . For any single Diophantine equation p = q : D single (N, V), one can compute n : N and a new single Diophantine equation p = q : D single (F n , V) such that for any ν : V → N, (∃ϕ :

N → N, p ϕ ν = q ϕ ν ) ↔ (∃ϕ : F n → N, p ϕ ν = q ϕ ν ).
Proof. We choose n greater that the number of bound variables which occur in either p or q.

Then this subset of N can be faithfully embedded into the finite type F n and we use such a renaming to compute (p , q ). Remark that the size of (p , q ) is the same as that of (p, q).

By Corollary 16 and Proposition 17, we see that a Diophantine logic formula A : D form potentially containing inner existential quantifiers and representing the Diophantine relation λν. A ν can effectively be reduced to a single Diophantine equation p = q : D single (F n , V)

such that A ν ↔ ∃ϕ : F n → N, p ϕ ν = q ϕ ν .
Because F n is the finite type of n elements, the (higher order) existential quantifier ∃ϕ simply encodes n successive (first order) existential quantifiers. The existential quantifiers that occur deep inside A are not erased by the reduction, they are moved at the outer level and are ultimately understood as solvability for some polynomial equation of which the parameters match the freely occurring variables of A.

Remarks on the Implementation of Matiyasevich's Theorems

Matiyasevich's theorem stating that there is a Diophantine description of the exponential relation x = y z is a masterpiece. It was the last missing step finishing the line of work by Davis, Putnam and Robinson which started with Davis' conjecture in 1953. Already in 1952, Julia Robinson discovered that in order to show the exponential relation Diophantine, it suffices to find a single binary Diophantine relation exhibiting exponential growth [START_REF] Robinson | Existential definability in arithmetic[END_REF], a so-called Robinson predicate, i.e. a predicate J(u, v) in two variables s.t. J(u, v) implies v < u u and for every k there are u, v with J(u, v) and v > u k . Robinson's insight meant the only thing missing to prove what is nowadays called the DPRM theorem, was a single polynomial equation capturing any freely chosen Robinson predicate. Similar to other famous hard problems of mathematics, the question is easy to state, but from the start of the study of Diophantine equations to the late 1960s, no such relation was known, rendering the problem one of the most baffling questions for mathematicians and computer scientists alike.

In 1970 [START_REF] Matijasevič | Enumerable sets are Diophantine[END_REF], Yuri Matiyasevich discovered that v = fib 2u is both a Robinson predicate and Diophantine. Here (fib n ) n∈N is the well known Fibonacci sequence defined by the second order recurrence relation fib 0 = 0, fib 1 = 1 and fib n+2 = fib n+1 + fib n . Combined with previous results, this concluded the multi-decades effort to establish the Diophantineness of all recursively enumerable predicates, implying a negative solution to Hilbert's tenth problem. That proof which included the original proof of Matiyasevich [START_REF] Matijasevič | Enumerable sets are Diophantine[END_REF] was later simplified. For instance, exploiting similar ideas but in the easier context of the solutions of another second order equation -namely Pell's equations x 2 -(a 2 -1)y 2 = 1 with parameter a > 1, -Martin Davis [START_REF] Davis | Hilbert's Tenth Problem is Unsolvable[END_REF] gave a standalone proof of the DPRM-theorem where recursively enumerable predicates are characterised by a variant of µ-recursive functions. In that paper, Davis also provided a proof of the admissibility of bounded universal quantification using the Chinese remainder theorem to encode finite sequences of numbers. There exists more recent and simpler proofs of this admissibility result as well, see e.g. [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF].

Before we discuss the mechanisation of the Diophantineness of both the exponential relation and of bounded universal quantification, we want to remark on the difficulty of mechanising the former proof. Both on its own and as a stepping stone towards the negative solution to Hilbert's tenth problem, it is clear that Matiyasevich's theorem was an extremely difficult question which required tremendous intellectual resources to be solved. The mechanisation of a modernised form of the proof, although not trivial, cannot be compared to the difficulty of finding a solution. In particular, the modern proof relies on very mature background theories, lowering the number of possible design choices for the mechanisation. Moreover, very detailed pen and paper accounts of the proof are available, which can be followed closely.

An aspect that is more challenging in mechanisation than on paper are proofs regarding the computability of certain functions. Since paper proofs oftentimes rely on a vague notion of algorithm, most of the reasoning about these algorithms is hand-waved away by computer scientists, relying on the implicit understanding of what is an algorithm. By using a synthetic approach to computability [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF][START_REF] Forster | On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem[END_REF][START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF], we make the notion of an algorithm precise and thus enable mechanisation, at the same time circumventing the verification of low-level programs.

Exponential is Diophantine (Theorem 6)

For our mechanised proof, we rely on a more recent account of Matiyasevich's theorem from [START_REF] Matiyasevich | On Hilbert's Tenth Problem[END_REF], which, among the many options we considered, seemed the shortest. The proof employs Pell's equation Once α b (n) is proven Diophantine, one can recover the exponential relation x, y, z → x = y z using the eigenvalue λ of the matrix B b which satisfies λ 2 -bλ -1 = 0. By wisely choosing m = bq -q 2 -1, one gets λ ≡ q mod m and thus, using the corresponding eigenvector, one derives qα b (n) -α b (n -1) ≡ q n mod m. For a large enough value of m, hence a large enough value7 of b, this gives a Diophantine representation of q n . In our code, we get a Diophantine logic formula of size 1689 as a witness (see dio_rel_expo_size ).

A b (n) = (B b ) n with A b (n) := α b (n + 1) -α b (n) α b (n) -α b (n -1)
The main libraries which are needed to solve Pell's equation and characterise its solutions are linear algebra (or at least square 2 × 2 matrices) over commutative rings such as Z and Z/pZ, a good library for modular algebra (Z/pZ), and the binomial theorem over rings. Without the help of the Coq ring tactic, such a development would be extremely painful. These libraries are then used again to derive the Diophantine encoding of the exponential.

Admissibility of Bounded Universal Quantification (Theorem 7)

As hinted earlier, we provide an implementation of the algorithm for the elimination of bounded universal quantification described in [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF]. It does not involve the use of a model of computation, hence does not create a chicken-and-egg problem when used for the proof of the DPRM theorem. The technique of [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] uses the exponential function and thus Theorem 6 (a lot), and a combination of arithmetic and bitwise operations over N through base 2 and base 2 q representations of natural numbers.

The

C k n is the k-th digit of the development of (1 + q) n = n i=0 C i n q i in base q = 2 n+1
. This gives a Diophantine representation using Theorem 6 and the relation is_digit defined for Lemma 8.

The rest of the admissibility proof for bounded universal quantification ∀i, i < n → A is a very nice encoding of vectors of natural numbers of type N n into natural numbers N such that regular addition + (resp. multiplication ×) somehow performs parallel/simultaneous additions (resp. multiplications) on the encoded vectors. More precisely, a vector (a 1 , . . . , a n ) ∈ [0, 2 q -1] n of natural numbers is encoded as the "cipher" a 1 r 2 + a 2 r 4 + a 3 r8 + • • • + a n r 2 n with r = 2 4q . In these sparse ciphers, only the digits occurring at r 2 i are non-zero. We remark that none of the parameters, including n or q, are constant in the encoding.

Besides a low-level inductive proof of Lucas' theorem, the essential library for the removal of bounded universal quantification consists of tools to manipulate the type N simultaneously and smoothly both as (a) usual natural numbers and (b) sparse base r = 2 4q encodings of vectors of natural numbers in [0, 2 q -1]. Notice that r is defined as r = 2 2q in [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] but we favour the alternative choice r = 2 4q which allows for an easier soundness proof for vector multiplication because there is no need to manage for digit overflows (see Appendix D).

A significant step in the Diophantine encoding of + and × on N n is the Diophantine encoding of u = n i=1 r 2 i and u 1 = n+1 i=2 r 2 i as the ciphers of the constant vectors (1, . . . , 1) ∈ N n and (0, 1, . . . , 1) ∈ N n+1 respectively, obtained by masking u 2 with w = 2 n+1 i=0 r i and 2w. Finally, it should be noted that prior to the elimination of the quantifier in ∀i, i < n → A, the Diophantine formula A is first normalised into a conjunction of elementary constraints using Theorem 10, and then the elimination is performed on that list of elementary constraints, encoding e.g. v 0 = v 1 + v 2 and v 0 = v 1 × v 2 with their respective sparse cipher counterparts.

Minsky Machines Reduce to FRACTRAN

In previous work, we have reduced the halting problem for Turing machines to PCP [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF] and on to a specialised halting problem for Minsky machines [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF] in Coq. The specialised halting problem asked whether a machine on a given input halts in a configuration with all registers containing zeros. In order to define Minsky machine recognisability, we consider a general halting problem which allows any final configuration. The adaption of the formal proofs reducing PCP via binary stack machines to Minsky machines is quite straightforward and reuses the certified compiler for low-level languages defined in [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF].

We first show that one can remove self loops from Minsky machines, i.e. instructions which jump to their own location, using the compositional reasoning techniques developed in [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF]. We then formalise the FRACTRAN language [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF] and show how the halting problem for Minsky machines can be encoded into the halting problem for FRACTRAN programs. While the verification of Minsky machines can be complex and needs preliminary thoughts on compositional reasoning, the translation from Minsky machines to FRACTRAN is elementary and needs no heavy machinery.

Minsky Machines

We employ Minsky machines [START_REF] Minsky | Computation: finite and infinite machines[END_REF] with instructions ι :

I n ::= INC (α : F n ) | DEC (α : F n ) (p : N).
A Minsky machine with n registers is a sequence of consecutively indexed instructions s : ι 0 ; . . . s + k : ι k ; represented as a pair (s : N, [ι 0 ; . . . ; ι k ] : L I n ). Its state (i, v) is a program counter (PC) value i : N and a vector of values for registers v : N n . INC α increases the value of register α and the PC by one. DEC α p decreases the value of register α by one if that is possible and increases the PC, or, if the register is already 0, jumps to PC value p. Given a Minsky machine (s, P ), we write (s, P ) // M (i 1 , v 1 ) n (i 2 , v 2 ) when (s, P ) transforms state (i 1 , v 1 ) into (i 2 , v 2 ) in n steps of computation. For (s, P ) to do a step in state (i, v) the instruction at label i in (s, P ) is considered. When a label i is outside of the code of (s, P ) we write out i (s, P ) and in that case (and only that case), no computation step can occur. We define the halting problem for Minsky Machines as

MM n : N, P : L I n , v : N n := (1, P ) // M (1, v) ↓
where (s, P ) // M (i, v) ↓ := ∃n j w, (s, P ) // M (i, v) n (j, w) ∧ out j (s, P ), meaning that the machine (s, P ) has a terminating computation starting at state (i, v). We refer to [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF] for a more in-depth formal description of those counter machines. Note that the halting problem defined there is more specific than the problem MM above defined but both are proved undecidable in our library .

We say that a machine has a self-loop if it contains an instruction of the form i : DEC α i, i.e. jumps to itself in case the register α has value 0, leading necessarily to non-termination. For every machine P with self-loops, we can construct an equivalent machine Q using one additional register α 0 with constant value 0, which has the same behaviour but no self-loops. Since the effect of a self loop i : DEC α i is either decrement and move to the next instruction at i+1 if α > 0 or else enter in a forever loop at i, it is easily simulated by a jump to a length-2 cycle, i.e. replacing i : DEC α i with i : DEC α j and adding j : DEC α 0 (j + 1); j + 1 : DEC α 0 j somewhere near the end of the program. machine. We first fix two infinite sequences of prime numbers p 0 , p 1 , . . . and q 0 , q 1 , . . . all distinct from each other. We define the encoding of n-register Minsky machine states as (i, v) := p i q x0 0 . . . q xn-1 n-1 where v = [x 0 , . . . , x n-1 ]: To simulate the step semantics of Minsky machines for i : INC α, we divide the encoded state by p i and multiply by p i+1 for the change in PC value, and increment the register α by multiplying with q α , hence we add the fraction p i+1 q α /p i ;

To simulate i : DEC α j when v[α] = 1 + n we divide by p i , multiply by p i+1 and decrease register α by dividing by q α , hence we add the fraction p i+1 /p i q α ; To simulate i : DEC α j when v[α] = 0 we divide by p i and multiply by p j . To make sure that this is only executed when the previous rule does not apply, we add the fraction p j /p i after the fraction p i+1 /p i q α . In short, we define the encoding of labelled instructions and then programs as (i, INC α) := [p i+1 q α /p i ] (i, DEC α j) := [p i+1 /p i q α ; p j /p i ] (i, [ι 0 ; . . . ; ι k ]) := (i, ι 0 ) + + • • • + + (i + k, ι k ).

Notice that we only produce regular programs and that a self loop like i : DEC α i, jumping on itself when v[α] = 0, will generate the fraction p i /p i potentially capturing any state (j, v) even when j = i. So this encoding does not work on Minsky machines containing self loops. Proof. Let (i, P ) be a Minsky machine with no self loops. We show that the simulation of (i, P ) by (i, P ) is 1-1, i.e. each step is simulated by one step. We first show the forward simulation, i.e. that (i, P ) // M (i 1 , v 1 ) (i 2 , v 2 ) entails (i, P ) // F (i 1 , v 1 ) (i 2 , v 2 ), by case analysis. Conversely we show that if (i, P ) // F (i 1 , v 1 ) st holds then st = (i 2 , v 2 ) for some (i 2 , v 2 ) such that (i, P ) // M (i 1 , v 1 ) (i 2 , v 2 ). Backward simulation involves the totality of MM one step semantics and the determinism of regular FRACTRAN one step semantics combined with the forward simulation.

Using these two simulation results, the desired equivalence follows by induction on the length of terminating computations. 1 . . . q xn n ↓ holds for any x 1 , . . . , x n .

Proof. Using Theorem 18, we first compute a Minsky machine (1, P 1 ) equivalent to (1, P ) but with one extra 0-valued spare register and no self loops. Then we apply Lemma 19 to (1, P 1 ) and let Q := (1, P 1 ). The program Q is obviously regular and given v = [x 1 ; . . . ; x n ], the encoding of the starting state (1, 0 :: v) for (1, P 1 ) is p 1 q 0 0 q x1 1 . . . q xn n hence the result.

This gives us a formal constructive proof that (regular) FRACTRAN is Turing complete as a model of computation and is consequently undecidable. Proof. Theorem 20 gives us a reduction from MM to FRACTRAN which can be combined with the reduction of Halt to PCP from [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF] and a slight modification of PCP to MM from [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF].

F

  Problem in Coqof these approaches, we propose three increasingly restricted characterisations of Diophantine relations: Diophantine logic, elementary Diophantine constraints and single Diophantine equations, between which we provide computable transformations in Sections 3 and 4.

F

  we get a representation in [u a , u a+n A [ by induction. Hence, let (E B , r B ) be the representation of B in [u a , u a+n B [. Then, inductively again, let (E C , r C ) be a representation of C at [u a+n B , u a+n B +n C [. We define r A := u a+n A +n B and E A := (r A = r B + r C ) :: E B + + E C and then (E A , r A ) represents A = B ∧ C in [u a , u a+1+n B +n C [; 5 The case of B ∨ C is similar: simply replace r A = r B + r C with r A = r B × r C ; We finish with the case when A is ∃ B. Let (E B , r B ) be a representation of B in [u a , u a+n B [. Let σ be the substitution mapping parameters in V and defined by σ(x 0 ) := u a+n B and σ(x 1+i ) := x i ; existential variables in U are left unmodified by this substitution. Then (σ(E B ), r B ) is a representation of A = ∃ B in [u a , u a+1+n B [. This concludes the recursive construction of a representation of λν. A ν .

x 2 -

 2 bxy + y 2 = 1 for b ≥ 2. We use the second order recurrence relation α b (-1) = -1, α b (0) = 0 and α b (n + 2) = bα b (n + 1) -α b (n) to describe the set of solutions of Pell's equation by (α b (n), α b (n + 1)) | n ∈ N . The recurrence can be characterised by the following square 2 × 2 matrix equation:

and B b := b -1 1 0

 1 Then, studying the properties of the sequence n → α b (n) in N or Z, one can show that α 2 (n) = n and n → α b (n) grows exponentially for b ≥ 3. Studying the properties of the same sequence in Z/pZ (for varying values of the modulus p), one can for instance show that n = α 2 (n) ≡ α b (n) mod b-2, which relates n and α b (n) modulo (b-2). With various intricate but elementary results, 6 such as e.g. α b (k) | α b (m) ↔ k | m and α 2 b (k) | α b (m) ↔ kα b (k) | m (both for b ≥ 2 and any k, m ∈ N), one can show that a, b, c → 3 < b ∧ a = α b (c) has a Diophantine representation. In our formalisation, we get a Diophantine logic formula of size 490 as a witness (see dio_rel_alpha_size ).

  Diophantine admissibility of bitwise operations over N is based on the relation stating that every bit of a is lower or equal than the corresponding bit in b and denoted a b. The equation a b ↔ C a b is odd (where C a b denotes the binomial coefficient) gives a Diophantine representation for a b and then bitwise operators are derived from in combination with regular addition +, in particular, the digit by digit AND operation called "projection. " To obtain that a b holds if and only if C a b ≡ 1 mod 2, we prove Lucas' theorem [18] which allows for the computation of the binomial coefficient in base p. It states that C a b ≡ C an bn × • • • × C a0 b0 mod p holds when p is prime and a = a n p n + • • • + a 0 and b = b n p n + • • • + b 0 are the respective base p representations of a and b. 8 A Diophantine representation of the binomial coefficient can be obtained via the binomial theorem:

Theorem 18 .

 18 Given a Minsky machine P with n registers one can compute a machine Q with 1+n registers and no self loops s.t. for any v, (1, P ) // M (1, v) ↓ ↔ (1, Q) // M (1, 0 :: v) ↓.

Lemma 19 .

 19 If (1, P ) has no self loops then (1, P ) // M (1, v) ↓ ↔ (1, P ) // F (1, v) ↓.

Theorem 20 .

 20 For any n-register Minsky machine P one can compute a regular FRACT-RAN program Q s.t. (1, P ) // M (1, [x 1 ; . . . ; x n ]) ↓ ↔ Q // F p 1 q x1

Corollary 21 .

 21 Halt reduces to FRACTRAN.

Named after the Greek mathematician Diophantus of Alexandria, who started the study of polynomial equations in the third century.

Proving Theorem 10 directly involves renamings of existential variables and might produce exponential blow-up in the number of constraints when handled naively.

We denote the size of A with |A|. The actual statement in the code is a bit more complicated because we also show that the number of elementary constraints can be bounded by 1 + 3|A|.

Since the intervals [ua, ua+n B [ and [ua+n B , ua+n B +nC [ are built disjoint, there is no difficulty in merging valuations whereas this usually involves renamings when existential variables are not carefully chosen.

by elementary we certainly do not mean either simple or obvious, but we mean that they only involve standard tools from modular and linear algebra.

the largeness of which is secured using α itself again, but with other input values.

With the usual convention that C a b = 0 when a > b. F S C D 2 0 1

For any Minsky machine (1, P ), if it starts on large enough register values, for instance if they are all greater than the length of P , then no jump can occur and the machine terminates after its last instruction executes. Such unfortunate behavior can be circumvented with a 0-valued spare register.

No FRACTRAN program can ever stop when it contains a fraction having an integer value like 2/1.F S C D 2 0 1 9

Which means we do not need to encode the algorithm that actually computes them.

v we abusively identify the vector v : N n (resp. w : N m ) with the valuation λ(i : Fn). v[i] (resp. λ(j : Fm). w[j]) that accesses the components of the vector v (resp. w).

Acknowledgements

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

Funding Dominique Larchey-Wendling: partially supported by the TICAMORE project (ANR grant 16-CE91-0002).

//uds-psl.github.io/H10, Coq library of undecidable problems: https://github.com/uds-psl/coq-library-undecidability

We fill in Lemma 8 in the Diophantine hint database and we derive the Diophantineness of the reflexive-transitive closure as a direct consequence of the equivalence R * u v ↔ ∃i, R i u v. Theorem 9 . For any binary relation R : N → N → P and any f, g : (V → N) → N, we have the map D P f → D P g → D R λν.R (ν x 1 ) (ν x 0 ) → D R λν.R * f ν g ν .

Elementary Diophantine Constraints

Elementary Diophantine constraints are very simple equations where only one instance of either + or × is allowed. We give a direct proof that any Diophantine logic formula is semantically equivalent to the satisfiability of a list of elementary Diophantine constraints.

Starting from two copies of N, one called U with u, v, w ranging over U for existentially quantified variables, and another one V = {x 0 , x 1 , . . .} for parameters, we define the type of elementary Diophantine constraints by:

where n : N Notice that these constraints do not have a "real" inductive structure, they are flat and of size either 3 or 5. Given two interpretations, ϕ : U → N for variables and ν : V → N for parameters, it is trivial to define the semantics c ϕ ν : P of a single constraint c of type D cstr :

Given a list l : L D cstr of constraints, we write l ϕ ν when all the constraints in l are simultaneously satisfied, i.e. l ϕ ν := ∀c, c ∈ l → c ϕ ν . We show the following result: Theorem 10 . For any Diophantine formula A : D form one can compute a list of elementary Diophantine constraints l : L D cstr such that ∀ν : V → N, A ν ↔ ∃ϕ : U → N, l ϕ ν . I.e. for any given interpretation of parameters ν, A ν holds if and only if the constraints in l are simultaneously satisfiable. Hence any Diophantine logic formula is equivalent to the satisfiability of the conjunction of finitely many elementary Diophantine constraints.

The proof of Theorem 10 spans the rest of this section. We will strengthen the result a bit to be able to get an easy argument by induction on A. Definition 11 . Given a relation R : (V → N) → P and an interval [u a , u a+n [ ⊆ U, a representation of R in [u a , u a+n [ is given by: 1. a list E : L D cstr of constraints and a reference variable r : U; 2. proofs that r and the (existentially quantified) variables occurring in E belong to [u a , u a+n [; 3. a proof that the constraints in E are always (simultaneously) satisfiable, i.e. ∀ν∃ϕ E ϕ ν ; 4. a proof that the list (r = 0) ::

27:13

Proof. We explain how any Minsky machine (1, P ) with n registers can be transformed into an equivalent one that uses an extra 0 valued spare register α 0 = 0 ∈ F 1+n and avoids self loops. Let k be the length of P and let P be the Minsky machine with 1 + n registers defined by performing a 1-1 replacement of instructions of ( proper inside jumps i : DEC α j for i = j and 1 ≤ j ≤ k are replaced by i : DEC (1 + α) j; and outside jumps i : DEC α j for j = 0 ∨ k < j are replaced by i : DEC (1 + α) 0. Then we define Q := P + + [DEC α 0 0; DEC α 0 (3 + k); DEC α 0 (2 + k)]. Notice that P is immediately followed DEC α 0 0, i.e. by an unconditional jump to 0 (because α 0 has value 0), and that (1, Q) ends with the length-2 cycle composed of 2+k : DEC α 0 (3+k); 3+k : DEC α 0 (2+k). We show that (1, Q) is a program without self loops (obvious) that satisfies the required simulation equivalence. Indeed, self loops are replaced by jumps to the length-2 cycle that uses the unmodified register α 0 to loop forever. One should just be careful that the outside jumps of (1, P ) do not accidentally fall into that cycle and this is why we redirect them all to PC value 0.

A predicate R : N n → P is MM-recognisable if there exist m : N and a Minsky machine P : L I n+m of (n+m) registers such that for any v :

The last m registers serve as spare registers during the computation. Notice that not allowing for spare registers would make e.g. the empty predicate un-recognisable. 9 It is possible to limit the number of (spare) registers but that question is not essential in our development.

FRACTRAN

We formalise the language FRACTRAN, introduced as a universal programming language for arithmetic by Conway [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF]. A FRACTRAN program Q consists of a list of positive fractions [p 1 /q 1 ; . . . ; p n /q n ]. The current state of a FRACTRAN program is just a natural number s. The first fraction p i /q i in Q such that s.(p i /q i ) is still integral determines the successor state, which then is s.(p i /q i ). If there is no such fraction in Q, the program terminates.

We make this precise inductively for Q being a list of fractions p/q : N × N:

i.e. at state x the first fraction p/q in Q where q divides p.x is used, and x is multiplied by p and divided by q. For instance, the FRACTRAN program [5/7; 2/1] runs forever when starting from state 7, producing the sequence 5 = 7.(5/7), 10 = 5.(2/1), 20 = 10.(2/1) ... 10 We say that a FRACTRAN program Q = [p 1 /q 1 ; . . . ; p n /q n ] is regular if none of its denominators is 0, i.e. if q 1 = 0, . . . , q n = 0. For a FRACTRAN program Q : L (N × N) and s : N, we define the decision problem as the question "does Q halt when starting from s":

Following [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF], we now show how (regular) FRACTRAN halting can be used to simulate Minsky machines halting. The idea is to use a simple Gödel encoding of the states of a Minsky

27:15 7 Diophantine Encoding of FRACTRAN

We show that a single step of FRACTRAN computation is a Diophantine relation.

Proof. The map is built by induction on Q.

by map 4 of Lemma 4, Proposition 5 and the induction hypothesis, these last steps being automated by the dio_rel_auto tactic.

In addition, the "Q has terminated at x" predicate is Diophantine for any FRACTRAN program Q. The proof is similar to the previous one:

by map 4 of Lemma 4, Proposition 5 and the induction hypothesis.

We can now deduce a core result of the paper which states that FRACTRAN programs have Diophantine termination predicates.

Proof. By definition we have

) and hence we obtain the claim using Theorem 9 in conjunction with Lemma 22 and Lemma 23.

We conclude with the undecidability of Hilbert's tenth problem by a reduction chain starting from the Halting problem for single tape Turing machines:

Theorem 25 (Hilbert's tenth problem). We have the following reduction chain

Halt PCP MM FRACTRAN DIO_FORM DIO_ELEM DIO_SINGLE H10

and as a consequence, H10 is undecidable .

Proof. The proof combines the previous results like Theorems 20 and 24 and Corollary 16.

The Davis-Putnam-Robinson-Matiyasevich Theorem

We conclude the paper with a proof of the DPRM theorem stating that recursively enumerable predicates are Diophantine. Here we assume that the informal notion of "recursive enumerability" can be characterised by Minsky machines recognisability (see Section 6.1). ). Notice that p 1 and the q i 's are hard-coded 11 in the Diophantine representation but we of course use Theorem 6. Then we end the proof by a combination with Theorem 24.

Lemma 26 . For

Theorem 27 (DPRM). Any MM-recognisable relation R : N n → P is Diophantine: one can compute a single Diophantine equation p = q : D single (F m , F n ) with n parameters and m variables s.t.

Proof. By definition, R : N n → P is recognised by some Minsky machine P with (n + m)

Notice that the value ν x i of any parameter of p = q greater than x n does not influence solvability. Now let m be an upper bound of the number of (existentially quantified) variables in p = q. We injectively map those variables in F m and we project the parameters of p = q onto F n by replacing every parameter greater than x n with the 0 constant. We get a Diophantine equation p = q : D single (F m , F n ) of which the solvability at v is equivalent to R v.

Related and Future Work

Regarding formalisations of Hilbert's tenth problem, there are various unfinished and preliminary results in different proof assistants: Carneiro [START_REF] Carneiro | A Lean formalization of Matiyasevič's theorem[END_REF] formalises Matiyasevich's theorem (Diophantineness of exponentiation) in Lean, but does not consider computational models or the DPRM theorem. Pąk formalises results regarding Pell's equation [START_REF] Pąk | The Matiyasevich Theorem[END_REF] and proves that Diophantine sets are closed under union and intersection [START_REF] Pąk | Diophantine sets. Preliminaries[END_REF], both as parts of the Mizar Mathematical Library. Stock et al. [START_REF] Stock | Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle[END_REF] report on an unfinished formalisation of the DPRM theorem in Isabelle based on [START_REF] Matiyasevich | On Hilbert's Tenth Problem[END_REF]. They cover some parts of the proof, but acknowledge for important missing results like Lucas' or "Kummer's theorem" and a "formalisation of a register machine. " Moreover, none of the cited reports considers the computability of the reductions involved or the verification of a universal machine in the chosen model of computation yet, one of them being a necessary proof goal for an actual undecidability result in the classical meta-theories of Isabelle/HOL and Mizar.

Regarding undecidability proofs in type theory, Forster, Heiter, and Smolka [START_REF] Forster | Verification of PCP-Related Computational Reductions in Coq[END_REF] reduce the halting problem of Turing machines to PCP. Forster and Larchey-Wendling [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF] reduce PCP to provability in linear logic via the halting problem of Minsky machines, which we build on. Forster, Kirst and Smolka develop the notion of synthetic undecidability in Coq and prove the undecidability of various notions in first-order logic [START_REF] Forster | On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem[END_REF].

In future developments, we want to connect our work to the formalisation of the recent simplified undecidability proof for System F inhabitation by Dudenhefner and Rehof [START_REF] Dudenhefner | A Simpler Undecidability Proof for System F Inhabitation[END_REF], which builds on elementary Diophantine constraints. The undecidability of second-order unification shown by Goldfarb [14] is also by reduction from elementary Diophantine constraints. We want to formalise his proof as an addition to our library of undecidable problems.

27:17

In the present paper, we prove that every MM-recognisable problem is Diophantine. This result can be extended to an equivalence, and furthermore to other formalised models of computation like µ-recursive functions [START_REF] Larchey-Wendling | Typing Total Recursive Functions in Coq[END_REF], Turing machines, or the untyped λ-calculus [START_REF] Forster | Weak Call-By-Value Lambda Calculus as a Model of Computation in Coq[END_REF].

A Some numerical Details about the Coq Code Contents

We give a detailed overview of the structure of the code corresponding to the results presented in this paper, and which was contributed to our Coq library of undecidable problems . The following lines of code (loc) measurements combine both definitions and proof scripts but do not account for comments. Notice that there are more files in the whole library than those needed to actually cover H10, but here, we only present the latter. In total, we contribute 12k loc to our undecidability project, 4k being additions to its shared libraries as extensions of the Coq standard library.

Concerning the multi-purpose shared libraries in Shared/Libs/DLW/Utils : we implemented finitary sums/products (over monoids) up to the binomial theorem (Newton) over non-commutative rings in sums.v and binomial.v for a total of 550 loc; we implemented bitwise operations over N, both a lists of bits in bool_list.v and Peano nat in bool_nat.v for a total of 1700 loc; we implemented many results about Euclidean division and Bézout's identity in gcd.v , prime numbers and their unboundedness in prime.v , and base p representations in power_decomp.v for a total of 1200 loc; we implemented miscellaneous libraries for the reification of bounded_quantification.v (120 loc), the Pigeon Hole Principle in php.v (350 loc) and iterations of binary relations in rel_iter.v (230 loc). Concerning the libraries for Minsky machines and FRACTRAN programs: by a slight update to the existing code [START_REF] Forster | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines[END_REF], we proved in mm_comp.v that MMtermination (on any state) is undecidable (10 loc). Both the pre-existing result (undecidability of MM-termination on the zero state) and the new result derive from the correctness of the compiler of binary stack machines into Minsky machines; we implemented the removal of self-loops in Minsky machines in mm_no_self.v (340 loc); we construct two infinite sequences of primes p i and q i in prime_seq.v (240 loc); FRACTRAN definitions and basic results occur in fractran_defs.v (310 loc) and the verified compiler from Minsky machines to FRACTRAN occurs in mm_fractran.v (300 loc); Concerning the libraries for proving Matiyasevich's theorems:

we implemented a library for modular arithmetic (Z/pZ) in Zp.v (920 loc); we implemented a library for 2 × 2-matrix computation including exponentiation and determinants in matrix.v (210 loc); we implemented an elementary proof of Lucas' theorem in luca.v (290 loc);

B Atomic Formulae as Elementary Constraints (Lemma 12)

We complete the postponed part of the proof of Lemma 12. We compute a representation for an atomic logical formula p = q : D form in an interval [u a , u a+n [ ⊆ U. 13 We describe the technique on the example of the atomic formula x 1 + (x 2 × 5) = x 3 which we represent in the interval [u 0 , u 10 [. Let us consider the following definitions:

The second line of E encodes the expression x 1 + (x 2 × 5) in [u 4 , u 9 [, and the third line encodes the expression x 3 in [u 9 , u 10 [ in a directed way: the values of the u i 's are uniquely determined by the values of the x i 's and the value of u 4 (resp. u 9 ) is always the same as the value of x 1 + (x 2 × 5) (resp. x 3 ). By "directed" we mean that the encoding is oriented bottom-up by the syntactic tree of sub-expressions: each variable in [u 4 , u 9 [ (resp. [u 9 , u 10 [) encodes a sub-expression of x 1 + (x 2 × 5) (resp. x 3 ) and its value is always the same as the value of the corresponding sub-expression. The first line encodes the identity sign in x 1 + (x 2 × 5) = x 3 . Indeed, whatever the values of u 4 and u 9 , the three constraints of the first line give enough freedom (in the choice of 13 The value of a is an input but the value of n is an output.

F S C D 2 0 1 9

27:20 Hilbert's Tenth Problem in Coq u 1 , u 2 , u 3 ) to always be satisfiable (requirement 3 of Definition 11). But when the single constraint u 0 = 0 is added (because r is u 0 ), then u 1 and u 2 must evaluate to 0 (because of u 0 = u 1 + u 2 ) and then u 3 must have the same value as both u 4 (because of u 3 = u 1 + u 4 ) and u 9 (because of u 3 = u 2 + u 9 ), hence the identity x 1 + (x 2 × 5) = x 3 must be satisfied (requirement 4 of Definition 11).

C Proof of a Convexity Identity (Proposition 13)

We give an elementary arithmetic justification of the result, proof which involves none of the high-level tools of mathematical analysis. We first show the statement for any a, b :

Assuming without loss of generality that a ≤ b, we can write b = a + δ with δ ∈ N and then, for ∈ {≤, =} we have 2ab a 2 + b 2 ↔ 2a 2 + 2aδ a 2 + a 2 + 2aδ + δ 2 ↔ 0 δ 2 hence the desired result.

Then we proceed with the proof of n i=1 2p i q i = n i=1 p 2 i + q 2 i ↔ p 1 = q 1 ∧ • • • ∧ p n = q n . The if case is obvious so we only describe the only if case. If there is u ∈ [1, n] such that p u = q u then we have 2p u q u < p 2 u + q 2 u , and 2p j q j ≤ p 2 j + q 2 j for all the other j ∈ [1, n] -{u}, in all cases by Statement (1). Hence we get n i=1 2p i q i < n i=1 p 2 i + q 2 i and the identity is not possible. So the only way to get the identity is when p u = q u holds for any i ∈ [1, n]. Despite its "classical logic" taste, this argument can easily be transformed into a constructive one by reasoning inductively on n.

D Avoiding Overflows in the Proof of Theorem 7

The section explains why we slightly modified the original proof of the elimination of bounded universal quantification [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] to avoid overflows when multiplying ciphers. Considering Equation (40) of page 3232, we compute the following product of ciphers (a i b j + a j b i )r 2 i +2 j and we remark that a i b j + a j b i overflows over r = 2 2q for e.g. a i = a j = b i = b j = 2 q -1. This slight overflow makes the implementation of the proof that the right part i<j (a i b j + a j b i )r 2 i +2 j is masked out in Equation (40) significantly harder. On the other hand, for r alternatively chosen as e.g. r = 2 4q , the overflow does not occur any more. With this remark, we do not imply that Equation (40) of [START_REF] Matiyasevich | A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers[END_REF] is incorrect in any way. However, its formal proof is really more complicated when overflows occur and that situation is straightforward to avoid.