2026-07-21T11:55:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12331 2024-03-06T10:49:59Z ddc:004 open_access

Undecidability of Semi-Unification on a Napkin Dudenhefner, Andrej undecidability semi-unification mechanization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.9 urn:nbn:de:0030-drops-123311 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.9 eng https://creativecommons.org/licenses/by/3.0/legalcode