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 JanDisplayed time zone: Saskatchewan, Central America change
15:35 - 16:40
Decidability and complexityCPP at Maurepas
Chair(s): Kathrin Stark Princeton University, USA
|Verified Programming of Turing Machines in Coq|
Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland UniversityDOI Pre-print Media Attached
|A Functional Proof Pearl: Inverting the Ackermann Hierarchy|
Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of SingaporeDOI Pre-print Media Attached
|Undecidability of Higher-Order Unification Formalised in Coq|
Simon Spies Saarland University, Yannick Forster Saarland UniversityDOI Pre-print Media Attached