Document Open Access Logo

Mechanized Undecidability of Higher-Order Beta-Matching

Author Andrej Dudenhefner

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.17.pdf
  • Filesize: 0.8 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • lambda-calculus
  • simple types
  • undecidability
  • higher-order matching
  • mechanization
  • Coq

Metrics

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

Abstract

Higher-order β-matching is the following decision problem: given two simply typed λ-terms, can the first term be instantiated to be β-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from λ-definability.
The present work provides a novel undecidability proof for higher-order β-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from λ-definability, the presented proof encodes a restricted form of string rewriting as higher-order β-matching. The particular approach is similar to Urzyczyn’s undecidability result for intersection type inhabitation.
The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order β-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order β-matching, λ-definability, and intersection type inhabitation.
The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.

Cite As Get BibTex

Andrej Dudenhefner. Mechanized Undecidability of Higher-Order Beta-Matching. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.17

Author Details

Andrej Dudenhefner
  • TU Dortmund University, Germany

Acknowledgements

I sincerely thank the anonymous reviewers for their constructive suggestions.

Supplementary Materials

References

  1. Roberto M. Amadio and Pierre-Louis Curien. Domains and lambda-calculi, volume 46 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1998. Google Scholar
  2. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. URL: http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
  3. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  4. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. North-Holland, 1972. Google Scholar
  5. Gilles Dowek. Higher-order unification and matching. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 1009-1062. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50018-7.
  6. Andrej Dudenhefner and Jakob Rehof. Undecidability of intersection type inhabitation at rank 3 and its formalization. Fundam. Informaticae, 170(1-3):93-110, 2019. URL: https://doi.org/10.3233/FI-2019-1856.
  7. Yannick Forster. Computability in constructive type theory. Die Publikationen der UdS, 2021. URL: https://doi.org/10.22028/D291-35758.
  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. Gérard P. Huet. The undecidability of unification in third order logic. Inf. Control., 22(3):257-267, 1973. URL: https://doi.org/10.1016/S0019-9958(73)90301-X.
  10. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. URL: https://doi.org/10.1016/0304-3975(75)90011-0.
  11. Thierry Joly. On lambda-definability I: the fixed model problem and generalizations of the matching problem. Fundam. Informaticae, 65(1-2):135-151, 2005. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi65-1-2-07.
  12. Ralph Loader. The undecidability of λ-definability. In Logic, meaning and computation: Essays in memory of Alonzo church, pages 331-342. Springer, 2001. Google Scholar
  13. Ralph Loader. Higher order beta matching is undecidable. Log. J. IGPL, 11(1):51-68, 2003. URL: https://doi.org/10.1093/JIGPAL/11.1.51.
  14. Vincent Padovani. Decidability of fourth-order matching. Mathematical Structures in Computer Science, 10(3):361-372, 2000. URL: http://journals.cambridge.org/action/displayAbstract?aid=44653.
  15. Sylvain Salvati, Giulio Manzonetto, Mai Gehrke, and Henk Barendregt. Loader and Urzyczyn are logically related. In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, volume 7392 of Lecture Notes in Computer Science, pages 364-376. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31585-5_34.
  16. 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.
  17. Richard Statman. Completeness, invariance and lambda-definability. J. Symb. Log., 47(1):17-26, 1982. URL: https://doi.org/10.2307/2273377.
  18. Colin Stirling. Decidability of higher-order matching. Log. Methods Comput. Sci., 5(3), 2009. URL: http://arxiv.org/abs/0907.3804.
  19. The Coq Development Team. The Coq proof assistant, July 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  20. Paweł Urzyczyn. Inhabitation of low-rank intersection types. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 356-370. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_26.
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