Undecidability of higher-order unification formalised in Coq

Abstract

We formalise undecidability results concerning higher-order unification in the simply-typed A-calculus with A-conversion in Coq. We prove the undecidability of general higher-order unification by reduction from Hilbert's tenth problem, the solvability of Diophantine equations, following a proof by Dowek. We sharpen the result by establishing the undecidability of second-order and third-order unification following proofs by Goldfarb and Huet, respectively. Goldfarb's proof for second-order unification is by reduction from Hilbert's tenth problem. Huet's original proof uses the Post correspondence problem (PCP) to show the undecidability of third-order unification. We simplify and formalise his proof as a reduction from modified PCP. We also verify a decision procedure for first-order unification. All proofs are carried out in the setting of synthetic undecidability and rely on Coq's built-in notion of computation.