Publication details

Saarland University Computer Science

Undecidability of Higher-Order Unification Formalised in Coq

Simon Spies, Yannick Forster

9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA, January 2020

We formalise undecidability results concerning higher-order unification in the simply-typed lambda-calculus with beta-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.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy