Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
Andrej Dudenhefner
TL;DR
This work establishes the undecidability of higher-order $\beta$-matching in the simply typed $\lambda$-calculus via a novel reduction from the restricted string rewriting problem $\mathbf{0}^+ \Rightarrow^* \mathbf{1}^+$. Departing from prior lambda-definability-based proofs, it encodes word expansion and rule applications using a carefully crafted, typed term construction, yielding a concise, verifiable reduction. The authors mechanize the proof in Coq and integrate it with the Coq Library of Undecidability Proofs, providing a rigorous, axiom-free verification. They also draw connections to intersection type inhabitation and $\lambda$-definability, offering a uniform framework that jointly applies to multiple undecidability results. The work also clarifies order bounds (undecidability at order $6$) and outlines potential extensions to richer type systems such as Coppo-Dezani intersection types, underscoring the practical value of formalized proofs in this area.
Abstract
Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from lambda-definability. The present work provides a novel undecidability proof for higher-order beta-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from lambda-definability, the presented proof encodes a restricted form of string rewriting as higher-order beta-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 beta-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order beta-matching, lambda-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.