Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.9
URN: urn:nbn:de:0030-drops-123311
URL: https://drops.dagstuhl.de/opus/volltexte/2020/12331/
Dudenhefner, Andrej
Undecidability of Semi-Unification on a Napkin
| pdf-format: |
|
Abstract
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.
BibTeX - Entry
@InProceedings{dudenhefner:LIPIcs:2020:12331,
author = {Andrej Dudenhefner},
title = {{Undecidability of Semi-Unification on a Napkin}},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-155-9},
ISSN = {1868-8969},
year = {2020},
volume = {167},
editor = {Zena M. Ariola},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12331},
URN = {urn:nbn:de:0030-drops-123311},
doi = {10.4230/LIPIcs.FSCD.2020.9},
annote = {Keywords: undecidability, semi-unification, mechanization}
}
| Keywords: | undecidability, semi-unification, mechanization | |
| Seminar: | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) | |
| Issue date: | 2020 | |
| Date of publication: | 28.06.2020 | |
| Supplementary Material: | https://github.com/uds-psl/2020-fscd-semi-unification |
