Document Open Access Logo

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Author Dominique Larchey-Wendling

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.18.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Author Details

Dominique Larchey-Wendling
  • Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France

Funding

  • Larchey-Wendling, Dominique: partially supported by the https://ticamore.logic.at/ project (http://www.agence-nationale-recherche.fr/?Projet=ANR-16-CE91-0002).

Cite AsGet BibTex

Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.18

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Linear logic
  • Theory of computation → Type theory
Keywords
  • Undecidability
  • computability theory
  • many-one reduction
  • Minsky machines
  • Fractran
  • sub-exponential linear logic
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Katalin Bimbó. The decidability of the intensional fragment of classical linear logic. Theoret. Comput. Sci., 597:1-17, 2015. URL: https://doi.org/10.1016/j.tcs.2015.06.019.
  2. Kaustuv Chaudhuri. Expressing additives using multiplicatives and subexponentials. Math. Structures Comput. Sci., 28(5):651–666, 2018. URL: https://doi.org/10.1017/S0960129516000293.
  3. John H. Conway. FRACTRAN: A Simple Universal Programming Language for Arithmetic, pages 4-26. Springer New York, New York, NY, 1987. Google Scholar
  4. Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, page 24–33, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3313276.3316369.
  5. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-complete, 2021. URL: http://arxiv.org/abs/2104.13866.
  6. Andrej Dudenhefner. Undecidability of Semi-Unification on a Napkin. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.9.
  7. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 38-51. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294091.
  8. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 104-117. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294096.
  9. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq Library of Undecidable Problems. In CoqPL 2020, New Orleans, LA, United States, 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  10. Max Kanovich. Linear Logic as a Logic of Computations. Ann. Pure Appl. Logic, 67(1-3):183-212, 1994. Google Scholar
  11. Max Kanovich. The direct simulation of Minsky machines in linear logic. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Note Series, chapter 2, pages 123-145. Cambridge University Press, 1995. Google Scholar
  12. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction, volume 131 of LIPIcs, pages 27:1-27:20, February 2019. Google Scholar
  13. Dominique Larchey-Wendling and Didier Galmiche. Nondeterministic Phase Semantics and the Undecidability of Boolean BI. ACM Trans. Comput. Log., 14(1):6:1-6:41, 2013. URL: https://doi.org/10.1145/2422085.2422091.
  14. Ranko Lazić and Sylvain Schmitz. Non-Elementary Complexities for Branching VASS, MELL, and Extensions. ACM Transactions on Computational Logic, 16(3):20:1-20:30, 2015. URL: https://doi.org/10.1145/2733375.
  15. Jérôme Leroux and Sylvain Schmitz. Demystifying Reachability in Vector Addition Systems. In LICS 2015: Proceedings of the 30th ACM/IEEE Symposium on Logic in Computer Science, pages 56-67. IEEE, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  16. Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive, 2021. URL: http://arxiv.org/abs/2104.12695.
  17. Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. In 31st Annual Symposium on Foundations of Computer Science, volume 2, pages 662-671. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/FSCS.1990.89588.
  18. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC '81, page 238–246, New York, NY, USA, 1981. Association for Computing Machinery. URL: https://doi.org/10.1145/800076.802477.
  19. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. Google Scholar
  20. Lutz Straßburger. On the decision problem for MELL. Theoret. Comput. Sci., 768:91-98, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact