Document Open Access Logo

Constructive Many-One Reduction from the Halting Problem to Semi-Unification

Author Andrej Dudenhefner

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.18.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • Saarland University, Saarbrücken, Germany

Acknowledgements

The author is grateful for encouragement and assistance by Paweł Urzyczyn and the members of the programming systems lab led by Gert Smolka at Saarland University.

Cite AsGet BibTex

Andrej Dudenhefner. Constructive Many-One Reduction from the Halting Problem to Semi-Unification. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.18

Abstract

The undecidability of semi-unification (unification combined with matching) has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument is by Turing reduction from Turing machine immortality (existence of a diverging configuration). There are several aspects of the existing work which can be improved upon. First, many-one completeness of semi-unification is not established due to the use of Turing reductions. Second, existing mechanizations do not cover a comprehensive reduction from Turing machine halting to semi-unification. Third, reliance on principles such as König’s lemma or the fan theorem does not support constructivity of the arguments. Improving upon the above aspects, the present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes many-one completeness of semi-unification. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. Notably, the mechanization relies on a technique invented by Hooper in the 1960s for Turing machine immortality. An immediate consequence of the present work is an alternative approach to the constructive many-one equivalence of System F typability and System F type checking, compared to the argument established in the 1990s by Wells.

Subject Classification

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

Metrics

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

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. Andrea Asperti and Wilmer Ricciotti. A formalization of multi-tape Turing machines. Theor. Comput. Sci., 603:23-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.07.013.
  3. Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauß, and Klaus U. Schulz. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/b978-044450813-3/50010-2.
  4. O. Bradley Bassler. The surveyability of mathematical proof: A historical perspective. Synth., 148(1):99-133, 2006. URL: https://doi.org/10.1007/s11229-004-6221-7.
  5. Andrej Bauer. First steps in synthetic computability theory. In Martín Hötzel Escardó, Achim Jung, and Michael W. Mislove, editors, Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2005, Birmingham, UK, May 18-21, 2005, volume 155 of Electronic Notes in Theoretical Computer Science, pages 5-31. Elsevier, 2005. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  6. Christopher Bouchard, Kimberly A. Gero, Christopher Lynch, and Paliath Narendran. On forward closure and the finite variant property. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science, pages 327-342. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40885-4_23.
  7. John H. Conway. Fractran: A simple universal programming language for arithmetic. In Open Problems in Communication and Computation, pages 4-26. Springer, 1987. Google Scholar
  8. The Coq Proof Assistant. https://coq.inria.fr/. Accessed: 2020-10-08.
  9. The Coq Proof Assistant Reference Manual. https://coq.inria.fr/distrib/current/refman/. Accessed: 2020-07-30.
  10. 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.
  11. Andrej Dudenhefner. The undecidability of system F typability and type checking for reductionists. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-10. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470520.
  12. Manuel Fähndrich, Jakob Rehof, and Manuvir Das. Scalable context-sensitive flow analysis using instantiation constraints. In Monica S. Lam, editor, Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Vancouver, Britith Columbia, Canada, June 18-21, 2000, pages 253-263. ACM, 2000. URL: https://doi.org/10.1145/349299.349332.
  13. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-related computational reductions in Coq. In Jeremy Avigad and Assia Mahboubi, editors, 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, volume 10895 of Lecture Notes in Computer Science, pages 253-269. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_15.
  14. Yannick Forster and Fabian Kunze. A certifying extraction with time bounds from Coq to call-by-value lambda 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.
  15. Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified programming of Turing machines 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 114-128. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373816.
  16. 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.
  17. 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.
  18. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'État, Éditeur inconnu, 1972. Google Scholar
  19. 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.
  20. 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.
  21. Said Jahama and Assaf J. Kfoury. A general theory of semi-unification. Technical report, Boston University Computer Science Department, 1993. Google Scholar
  22. Emmanuel Jeandel. On immortal configurations in Turing machines. In S. Barry Cooper, Anuj Dawar, and Benedikt Löwe, editors, How the World Computes - Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 18-23, 2012. Proceedings, volume 7318 of Lecture Notes in Computer Science, pages 334-343. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30870-3_34.
  23. Jarkko Kari. The tiling problem revisited (extended abstract). In Jérôme Olivier Durand-Lose and Maurice Margenstern, editors, Machines, Computations, and Universality, 5th International Conference, MCU 2007, Orléans, France, September 10-13, 2007, Proceedings, volume 4664 of Lecture Notes in Computer Science, pages 72-79. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74593-8_6.
  24. 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.
  25. Assaf J. Kfoury, Jerzy Tiuryn, and Paweł 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.
  26. Assaf J. Kfoury, Jerzy Tiuryn, and Paweł 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.
  27. Assaf J. Kfoury, Jerzy Tiuryn, and Paweł Urzyczyn. The undecidability of the semi-unification problem. Inf. Comput., 102(1):83-101, 1993. URL: https://doi.org/10.1006/inco.1993.1003.
  28. Assaf J. Kfoury, Jerzy Tiuryn, and Paweł Urzyczyn. An analysis of ML typability. J. ACM, 41(2):368-398, 1994. URL: https://doi.org/10.1145/174652.174659.
  29. 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.
  30. Hans Leiß. Polymorphic recursion and semi-unification. In Egon Börger, Hans Kleine Büning, and Michael M. Richter, editors, CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings, volume 440 of Lecture Notes in Computer Science, pages 211-224. Springer, 1989. URL: https://doi.org/10.1007/3-540-52753-2_41.
  31. 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.
  32. Yuri V. Matiyasevich and Géraud Sénizergues. Decision problems for semi-Thue systems with a few rules. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 523-531. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561469.
  33. M. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  34. 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.
  35. Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. Google Scholar
  36. Paul Walton Purdom. Detecting looping simplifications. In Pierre Lescanne, editor, Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, volume 256 of Lecture Notes in Computer Science, pages 54-61. Springer, 1987. URL: https://doi.org/10.1007/3-540-17220-3_5.
  37. John C. Reynolds. Towards a theory of type structure. In Bernard Robinet, editor, Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, volume 19 of Lecture Notes in Computer Science, pages 408-423. Springer, 1974. URL: https://doi.org/10.1007/3-540-06859-7_148.
  38. Hartley Rogers. Theory of Recursive Functions and Effective Computability (Reprint from 1967). MIT Press, 1987. URL: http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=3182.
  39. Joe B. Wells. Typability and type checking in system F are equivalent and undecidable. Ann. Pure Appl. Log., 98(1-3):111-156, 1999. URL: https://doi.org/10.1016/S0168-0072(98)00047-5.
  40. Arkadiusz Wojna. Counter machines. Inf. Process. Lett., 71(5-6):193-197, 1999. URL: https://doi.org/10.1016/S0020-0190(99)00116-7.
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