Skip to Main content Skip to Navigation
Conference papers

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Dominique Larchey-Wendling 1 
1 TYPES - Logic, Proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadata

https://hal.inria.fr/hal-03280264
Contributor : Dominique Larchey-Wendling Connect in order to contact the contributor
Submitted on : Wednesday, July 7, 2021 - 11:06:10 AM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM

File

LIPIcs-FSCD-2021-18.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021, Buenos Aires, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.18⟩. ⟨hal-03280264⟩

Share

Metrics

Record views

36

Files downloads

40