Simon Spies: Bachelor's Thesis

Saarland University Computer Science

Formalising the Undecidability of Higher-Order Unification

Advisors: Gert Smolka, Yannick Forster


The problem of unifying open terms naturally arises when working in a type theory, e.g. the one implemented in the proof assistant Coq. Two terms are said to be unifiable if there is a substitution such that both terms have the same normal form under this substitution. For first-order terms it is well known that this problem is decidable. However, for terms of higher order it has been shown that unification is undecidable.

In 1973 Gerard Huet proved that third-order unification is undecidable with a reduction from the Post correspondence problem. Warren D. Goldfarb improved on this result in 1981 by proving that even unification in a second-order language is undecidable. The proof is obtained by a reduction from Hilbert's 10th problem — Diophantine Equations — to second-order unification.

In my Bachelor's thesis I will formalise both reductions in Coq. In this talk I intend to give some insight into the Huet reduction as well as the formalisation thereof. In addition, I will shortly recap the main idea of the Goldfarb reduction and touch on problems that occur when modernising the proofs.


Legal notice, Privacy policy