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 - 15:56|
|Verified Programming of Turing Machines in Coq|
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland UniversityDOI Pre-print Media Attached
|15:56 - 16:18|
|A Functional Proof Pearl: Inverting the Ackermann Hierarchy|
Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of SingaporeDOI Pre-print Media Attached
|16:18 - 16:40|
|Undecidability of Higher-Order Unification Formalised in Coq|
CPPDOI Pre-print Media Attached