Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

TL;DR

This paper presents a new, simpler undecidability proof for higher-order beta-matching, mechanized in Coq, by encoding string rewriting and reducing from the Halting Problem, unifying several undecidable problems.

Contribution

It introduces a novel, verified undecidability proof for higher-order beta-matching using string rewriting encoding, simplifying verification and connecting multiple undecidable problems.

Findings

Undecidability of higher-order beta-matching is established via a new proof.

The proof is mechanized and verified in the Coq proof assistant.

A uniform construction links undecidability of beta-matching, lambda-definability, and intersection type inhabitation.

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.