License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.18
URN: urn:nbn:de:0030-drops-142568
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14256/
Larchey-Wendling, Dominique
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
Abstract
We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative sub-exponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.
BibTeX - Entry
@InProceedings{larcheywendling:LIPIcs.FSCD.2021.18,
author = {Larchey-Wendling, Dominique},
title = {{Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-191-7},
ISSN = {1868-8969},
year = {2021},
volume = {195},
editor = {Kobayashi, Naoki},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14256},
URN = {urn:nbn:de:0030-drops-142568},
doi = {10.4230/LIPIcs.FSCD.2021.18},
annote = {Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq}
}
