高阶β匹配的机械化不可判定性（扩展版）
Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
AI总结：
本文通过字符串重写系统证明了高阶β匹配的不可判定性，并利用Coq验证了该结果。
摘要：
高阶β匹配是一个决策问题：给定两个简单类型λ项，第一个项能否被实例化以使其与第二个项β等价？该问题由Huet于1970年代提出，并于2003年由Loader通过归约到λ可定义性证明了不可判定性。本文提供了一个新的不可判定性证明，旨在通过证明助手验证该结果。不同于从λ可定义性出发，本文的证明将受限形式的字符串重写编码为高阶β匹配。该方法与Urzyczyn对交集类型可居性不可判定性的结果相似。本文的方法有以下优势：首先，由于重写系统的简单形式，证明更容易完整验证；其次，字符串重写的不可判定性已通过Coq证明助手认证；因此，我们获得了从停机问题到高阶β匹配的许多一还原。第三，本文的方法识别出一种统一的构造，展示了高阶β匹配、λ可定义性以及交集类型可居性的不可判定性。本文的不可判定性证明在Coq证明助手中被机械化，并贡献于现有的不可判定性证明Coq库。
英文摘要：
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, found 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 approach showing undecidability of 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 Rocq Prover. 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 Rocq Prover and contributed to the existing Coq Library of Undecidability Proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
