Nothing Special   »   [go: up one dir, main page]
Document Open Access Logo

Certified Decision Procedures for Two-Counter Machines

Author Andrej Dudenhefner

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.16.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • TU Dortmund, Germany

Cite AsGet BibTex

Andrej Dudenhefner. Certified Decision Procedures for Two-Counter Machines. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.16

Abstract

Two-counter machines, pioneered by Minsky in the 1960s, constitute a particularly simple, universal model of computation. Universality of reversible two-counter machines (having a right-unique step relation) has been shown by Morita in the 1990s. Therefore, the halting problem for reversible two-counter machines is undecidable. Surprisingly, this statement is specific to certain instruction sets of the underlying machine model. In the present work we consider two-counter machines (CM2) with instructions inc_c (increment counter c, go to next instruction), dec_c q (if counter c is zero, then go to next instruction, otherwise decrement counter c and go to instruction q). While the halting problem for CM2 is undecidable, we give a decision procedure for the halting problem for reversible CM2, contrasting Morita’s result. We supplement our result with decision procedures for uniform boundedness (is there a uniform bound on the number of reachable configurations?) and uniform mortality (is there a uniform bound on the number of steps in any run?) for CM2. Termination and correctness of each presented decision procedure is certified using the Coq proof assistant. In fact, both the implementation and certification is carried out simultaneously using the tactic language of the Coq proof assistant. Building upon existing infrastructure, the mechanized decision procedures are contributed to the Coq library of undecidability proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computability
Keywords
  • constructive mathematics
  • computability theory
  • decidability
  • counter automata
  • mechanization
  • Coq

Metrics

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

Supplementary Materials

References

  1. 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, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 9:1-9:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.9.
  2. Andrej Dudenhefner. Constructive many-one reduction from the halting problem to semi-unification. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.18.
  3. Yannick Forster. Computability in Constructive Type Theory. PhD thesis, Saarland University, 2021. Google Scholar
  4. Yannick Forster and Fabian Kunze. A certifying extraction with time bounds from Coq to call-by-value λ-calculus. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 17:1-17:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.17.
  5. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space. Proc. ACM Program. Lang., 4(POPL):27:1-27:23, 2020. URL: https://doi.org/10.1145/3371095.
  6. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 19:1-19:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.19.
  7. 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.
  8. 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 The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020), 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  9. Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. J. Formaliz. Reason., 3(2):95-152, 2010. URL: https://doi.org/10.6092/issn.1972-5787/1979.
  10. Philip K. Hooper. The undecidability of the Turing machine immortality problem. J. Symb. Log., 31(2):219-234, 1966. URL: https://doi.org/10.2307/2269811.
  11. Sergiu Ivanov, Elisabeth Pelz, and Sergey Verlan. Small universal non-deterministic Petri nets with inhibitor arcs. In Helmut Jürgensen, Juhani Karhumäki, and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems - 16th International Workshop, DCFS 2014, Turku, Finland, August 5-8, 2014. Proceedings, volume 8614 of Lecture Notes in Computer Science, pages 186-197. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09704-6_17.
  12. Jarkko Kari and Nicolas Ollinger. Periodicity and immortality in reversible computing. In Edward Ochmanski and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008, Torun, Poland, August 25-29, 2008, Proceedings, volume 5162 of Lecture Notes in Computer Science, pages 419-430. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85238-4_34.
  13. Ivan Korec. Small universal register machines. Theor. Comput. Sci., 168(2):267-301, 1996. URL: https://doi.org/10.1016/S0304-3975(96)00080-1.
  14. Egor Kuzmin and Dmitry Chalyy. Decidability of boundedness problems for Minsky counter machines. Autom. Control. Comput. Sci., 44(7):387-397, 2010. URL: https://doi.org/10.3103/S0146411610070047.
  15. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s tenth problem in Coq. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 27:1-27:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.27.
  16. Dominique Larchey-Wendling and Jean-François Monin. Simulating induction-recursion for partial algorithms. In 24th International Conference on Types for Proofs and Programs, TYPES 2018, 2018. Google Scholar
  17. Pierre Letouzey. A new Extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, volume 2646 of Lecture Notes in Computer Science, pages 200-219. Springer, 2002. URL: https://doi.org/10.1007/3-540-39185-1_12.
  18. Marvin Minsky. Recursive unsolvability of Post’s problem of "tag" and other topics in theory of Turing machines. Annals of Mathematics, pages 437-455, 1961. Google Scholar
  19. Marvin Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  20. Kenichi Morita. Universality of a reversible two-counter machine. Theor. Comput. Sci., 168(2):303-320, 1996. URL: https://doi.org/10.1016/S0304-3975(96)00081-3.
  21. Kenichi Morita. Reversible computing systems, logic circuits, and cellular automata. In Third International Conference on Networking and Computing, ICNC 2012, Okinawa, Japan, December 5-7, 2012, pages 1-8. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ICNC.2012.10.
  22. Kenichi Morita. Theory of Reversible Computing. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2017. URL: https://doi.org/10.1007/978-4-431-56606-9.
  23. Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356-364, 1980. URL: https://doi.org/10.1145/322186.322198.
  24. Emanuele Rodaro and Pedro V. Silva. Amalgams of inverse semigroups and reversible two-counter machines. Journal of Pure and Applied Algebra, 217(4):585-597, 2013. Google Scholar
  25. Matthieu Sozeau and Cyprien Mangin. Equations v1.2, May 2019. URL: https://doi.org/10.5281/zenodo.3012649.
  26. Simon Spies and Yannick Forster. Undecidability of higher-order unification formalised in Coq. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 143-157. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373832.
  27. The Coq Development Team. The Coq proof assistant, January 2022. URL: https://doi.org/10.5281/zenodo.5846982.
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