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.

翻译：高阶beta匹配是如下判定问题：给定两个简单类型lambda项，第一个项能否通过实例化成为与第二个项beta等价的项？该问题由Huet于1970年代提出，并由Loader于2003年通过lambda可定义性的归约证明其不可判定性。本研究为高阶beta匹配提供了一种新颖的不可判定性证明，旨在通过证明辅助工具验证该结果。与从lambda可定义性出发不同，本证明将受限形式的字符串重写编码为高阶beta匹配。该方法与Urzyczyn关于交集类型可居性的不可判定性结果具有相似性。所提出的方法具有若干优势：首先，由于采用形式简单的重写系统作为起点，该证明更易于进行完整细节验证；其次，所考虑的字符串重写问题的不可判定性已通过Coq证明辅助工具完成形式化验证。因此，我们获得了从停机问题到高阶beta匹配的经过验证的多一归约。第三，该方法构建了统一框架，可同时证明高阶beta匹配、lambda可定义性及交集类型可居性的不可判定性。本不可判定性证明已在Coq证明辅助工具中实现机械化，并贡献至现有的Coq不可判定性证明库。