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 terms naturally arises when working in type theory like in the proof assistant Coq. Two terms are said to be unifiable if there is a substitution such that these terms have the same normal form under the substitution. For first-order terms it is well known that this problem is decidable. For higher-order terms it has been shown that unification is undecidable.

In 1973 Gerard Huet proved that 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 second-order unification 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 want to formalise both reductions in Coq. In this talk I will give some insight into the essence of the Huet reduction. Additionally I will shortly explain the main idea of the Goldfarb reduction.

Legal notice, Privacy policy