论文标题
希尔伯特在COQ中的第十个问题（扩展版）
Hilbert's Tenth Problem in Coq (Extended Version)
论文作者
论文摘要
我们在COQ的建设性类型理论中正式化了二磷剂方程的不可溶性，即多项式方程。为此，我们给出了Davis-Putnam-Robinson-Matiyasevich定理的第一个完整机械化，并指出，每个递归枚举的问题 - 在我们的情况下，由Minsky Machine所述）是二磷剂。我们通过使用合成方法来获得优雅且可理解的证明，并通过引入Conway的Fractran语言作为中间层。此外，我们证明了相反的方向，并表明每个双磷灰石关系都可以通过$ $ $ $ - 传动功能来识别，并从$μ$ $ $ secursive函数中提供给Minsky机器的认证编译器。
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 $μ$-recursive functions and give a certified compiler from $μ$-recursive functions to Minsky machines.
