Write a Blog >>
Mon 20 Jan 2020 16:18 - 16:40 at Maurepas - Decidability and complexity Chair(s): Kathrin Stark

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

CPP-2020-papers
15:35 - 16:40: CPP 2020 - Decidability and complexity at Maurepas
Chair(s): Kathrin StarkSaarland University, Germany
CPP-2020-papers15:35 - 15:56
Talk
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University
DOI Pre-print Media Attached
CPP-2020-papers15:56 - 16:18
Talk
Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore
DOI Pre-print Media Attached
CPP-2020-papers16:18 - 16:40
Talk
Simon SpiesSaarland University, Yannick ForsterSaarland University
DOI Pre-print Media Attached