文章基本信息

标题：Undecidability of Semi-Unification on a Napkin
本地全文：下载
作者：Andrej Dudenhefner
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：9:1-9:16
DOI：10.4230/LIPIcs.FSCD.2020.9
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Semi-unification (unification combined with matching) has been proven undecidable by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument reduces Turing machine immortality via Turing machine boundedness to semi-unification. The latter part is technically most challenging, involving several intermediate models of computation. This work presents a novel, simpler reduction from Turing machine boundedness to semi-unification. In contrast to the original argument, we directly translate boundedness to solutions of semi-unification and vice versa. In addition, the reduction is mechanized in the Coq proof assistant, relying on a mechanization-friendly stack machine model that corresponds to space-bounded Turing machines. Taking advantage of the simpler proof, the mechanization is comparatively short and fully constructive.
关键词：undecidability; semi-unification; mechanization