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.
@InProceedings{dudenhefner:LIPIcs.FSCD.2025.17, author = {Dudenhefner, Andrej}, title = {{Mechanized Undecidability of Higher-Order Beta-Matching}}, booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)}, pages = {17:1--17:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-374-4}, ISSN = {1868-8969}, year = {2025}, volume = {337}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.17}, URN = {urn:nbn:de:0030-drops-236323}, doi = {10.4230/LIPIcs.FSCD.2025.17}, annote = {Keywords: lambda-calculus, simple types, undecidability, higher-order matching, mechanization, Coq} }
Feedback for Dagstuhl Publishing