Document Open Access Logo

Undecidability of Semi-Unification on a Napkin

Author Andrej Dudenhefner

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.9.pdf
  • Filesize: 466 kB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Computability
Keywords
  • undecidability
  • semi-unification
  • mechanization

Metrics

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

Abstract

Semi-unification (unification combined with matching) has been proven undecidable by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument reduces Turing machine immortality via Turing machine boundedness to semi-unification. The latter part is technically most challenging, involving several intermediate models of computation.
This work presents a novel, simpler reduction from Turing machine boundedness to semi-unification. In contrast to the original argument, we directly translate boundedness to solutions of semi-unification and vice versa. In addition, the reduction is mechanized in the Coq proof assistant, relying on a mechanization-friendly stack machine model that corresponds to space-bounded Turing machines. Taking advantage of the simpler proof, the mechanization is comparatively short and fully constructive.

Cite As Get BibTex

Andrej Dudenhefner. Undecidability of Semi-Unification on a Napkin. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.9

Author Details

Andrej Dudenhefner
  • Saarland University, Saarbrücken, Germany

Supplementary Materials

References

  1. Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, and Michaël Rusinowitch. Unification modulo synchronous distributivity. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 14-29. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_4.
  2. Andrej Dudenhefner. Mechanization of a Reduction from Uniform Boundedness of Deterministic Simple Stack Machines to Semi-unification. https://github.com/uds-psl/2020-fscd-semi-unification. Accessed: 2019-12-19. URL: https://github.com/uds-psl/2020-fscd-semi-unification.
  3. Andrej Bauer. First steps in synthetic computability theory. Electr. Notes Theor. Comput. Sci., 155:5-31, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  4. Josef Berger. The fan theorem and uniform continuity. In S. Barry Cooper, Benedikt Löwe, and Leen Torenvliet, editors, New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 8-12, 2005, Proceedings, volume 3526 of Lecture Notes in Computer Science, pages 18-22. Springer, 2005. URL: https://doi.org/10.1007/11494645_3.
  5. The Coq Proof Assistant. https://coq.inria.fr/. Accessed: 2019-12-19. URL: https://coq.inria.fr/.
  6. Lucılia Figueiredo and Carlos Camarao. Semi-unification and periodicity of turing machines. URL: https://www.researchgate.net/publication/268426611_Semi-unification_and_Periodicity_of_Turing_Machines.
  7. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-related computational reductions in Coq. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, pages 253-269, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_15.
  8. 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.
  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 The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020), 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  10. Fritz Henglein. Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):253-289, 1993. URL: https://doi.org/10.1145/169701.169692.
  11. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society, 146:29-60, 1969. Google Scholar
  12. 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.
  13. Said Jahama and Assaf J. Kfoury. A general theory of semi-unification. Technical report, Boston University Computer Science Department, 1993. Google Scholar
  14. 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.
  15. Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. The Undecidability of the Semi-Unification Problem (Preliminary Report). In Harriet Ortiz, editor, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, May 13-17, 1990, Baltimore, Maryland, USA, pages 468-476. ACM, 1990. URL: https://doi.org/10.1145/100216.100279.
  16. Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):290-311, 1993. URL: https://doi.org/10.1145/169701.169687.
  17. Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. The undecidability of the semi-unification problem. Inf. Comput., 102(1):83-101, 1993. URL: https://doi.org/10.1006/inco.1993.1003.
  18. Hans Leiß and Fritz Henglein. A decidable case of the semi-unification problem. In Andrzej Tarlecki, editor, Mathematical Foundations of Computer Science 1991, 16th International Symposium, MFCS'91, Kazimierz Dolny, Poland, September 9-13, 1991, Proceedings, volume 520 of Lecture Notes in Computer Science, pages 318-327. Springer, 1991. URL: https://doi.org/10.1007/3-540-54345-7_75.
  19. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. URL: https://doi.org/10.1016/0022-0000(78)90014-4.
  20. Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990. Google Scholar
  21. Alan Mycroft. Polymorphic type schemes and recursive definitions. In Manfred Paul and Bernard Robinet, editors, International Symposium on Programming, 6th Colloquium, Toulouse, France, April 17-19, 1984, Proceedings, volume 167 of Lecture Notes in Computer Science, pages 217-228. Springer, 1984. URL: https://doi.org/10.1007/3-540-12925-1_41.
  22. Helmut Schwichtenberg. A direct proof of the equivalence between brouwer’s fan theorem and könig’s lemma with a uniqueness hypothesis. J. UCS, 11(12):2086-2095, 2005. URL: https://doi.org/10.3217/jucs-011-12-2086.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact