Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Larchey-Wendling, Dominique https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-142568
URL:

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

pdf-format:


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}
}

Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq
Seminar: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue date: 2021
Date of publication: 06.07.2021
Supplementary Material: Software (Source Code): https://github.com/uds-psl/coq-library-undecidability/releases/tag/FSCD-2021 archived at: https://archive.softwareheritage.org/swh:1:rev:4115398f10c42a41833036f8c4500f24233cc9a7


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI