Coq中的希尔伯特第十问题（扩展版）
摘要：线程的求解是一个不可判定的问题-在Coq的结构性类型理论中，我们形式化了Diophantine方程的可解性，即自然数上的多项式方程。为此，我们首次完全机械化了Davis-Putnam-Robinson-Matiyasevich定理，该定理指出每个可递归枚举问题（在我们的情况下是通过Minsky机器）都是Diophantine方程。通过使用一种合成方法来处理可计算性，并引入康威的FRACTRAN语言作为中间层，我们获得一种优雅且易于理解的证明。此外，我们证明了反向的方向，并展示了每个Diophantine关系都可以通过$mu$-recursive函数识别，并给出了一个从$mu$-recursive函数到Minsky机器的认证编译器。
作者：Dominique Larchey-Wendling and Yannick Forster
论文ID：2003.04604
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22