# Simon Spies: Bachelor's Thesis

# Formalising the Undecidability of Higher-Order Unification

**Advisors:** Gert Smolka, Yannick Forster

## Abstract

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