Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
In: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) ; https://inria.hal.science/hal-03280264 ; 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021, Buenos Aires, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.18⟩, 2021
Online
Konferenz
Zugriff:
International audience ; We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative subexponential 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.
Titel: |
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
|
---|---|
Autor/in / Beteiligte Person: | Larchey-Wendling, Dominique ; Logic, Proof Theory and Programming (TYPES) ; Department of Formal Methods (LORIA - FM) ; Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
Link: | |
Zeitschrift: | 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) ; https://inria.hal.science/hal-03280264 ; 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021, Buenos Aires, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.18⟩, 2021 |
Veröffentlichung: | HAL CCSD ; LIPIcs - Leibniz International Proceedings in Informatics. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), 2021 |
Medientyp: | Konferenz |
DOI: | 10.4230/LIPIcs.FSCD.2021.18 |
Schlagwort: |
|
Sonstiges: |
|