Undecidability of Higher-Order Unification Formalised in Coq
summary
Mechanisation in Coq proves that second-order unification is undecidable and, via a conservative embedding, that all higher-order unification problems are undecidable; reductions go from Hilbert’s tenth (systems of Diophantine equations) to system unification using Church and Goldfarb numerals and additional "hereditary" equations to forbid junk terms. The development uses about 3,000 lines of setup and proofs of roughly 500 and 1,000 lines, and relies on Autosubst and Equations; all constructions check and the formalisation succeeds.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:28What is high or deification
- 1:22What is a typed equation
- 1:46Substitution of P
- 2:06Is this decidable
- 2:58Review
- 4:14Calculus
- 4:50HigherOrder Unification
- 5:37Undecidability
- 6:59Reduction
- 8:14System Unification
- 8:26Reduction Function
- 9:59Further Order Terms
- 10:12Education is decidable
- 10:51For identification
- 11:19Definition
- 13:27Recap
- 15:46Formalization
related talks
31mA Coq Library of Undecidable Problems
59mUnification Modulo Equational Theories in Languages with Binding Operators
01h 34mFormal Logic Undressed
27mAn Equations Tutorial
30mNormalisation for First-Class Universe Levels
14mA Limited Case for Reification by Type Inference
11mLocal algebraic effect theories
19mExtensible Metatheory Mechanization via Family Polymorphism