Undecidability of Higher-Order Unification Formalised in Coq
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.
Mon 20 Jan Times are displayed in time zone: Saskatchewan, Central America change
15:35 - 16:40: Decidability and complexityCPP at Maurepas Chair(s): Kathrin StarkPrinceton University, USA | |||
15:35 - 15:56 Talk | Verified Programming of Turing Machines in Coq CPP Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University DOI Pre-print Media Attached | ||
15:56 - 16:18 Talk | A Functional Proof Pearl: Inverting the Ackermann Hierarchy CPP Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore DOI Pre-print Media Attached | ||
16:18 - 16:40 Talk | Undecidability of Higher-Order Unification Formalised in Coq CPP DOI Pre-print Media Attached |