Publication details

Saarland University Computer Science

Undecidability of Semi-Unification on a Napkin

Andrej Dudenhefner

5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Paris, France, pp. 9:1-9:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020

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.

Download PDF        Show BibTeX        Download slides (PDF)       

Login to edit

Legal notice, Privacy policy