Email Gateway (Apr 24 2026 at 19:35): Email Gateway (Apr 24 2026 at 19:35):From: Tobias Nipkow <nipkow@in.tum.de>
Nominal Unification
Guilherme Borges Brandão, Thomas Ammer , Daniele Nantes Sobrinho, Mauricio
Ayala-Rinción, Christian Urban , Maribel Fernández and Mohammad Abdulaziz
This is an improved and updated formalisation of the nominal unification
algorithm. Nominal unification is a generalisation of the classic first-order
unification to the practically important case of equations between terms
involving binding operations. A simple, possibly capturing substitution of terms
for variables solves such equations if it makes the equated terms
alpha-equivalent, i.e.~equal up to renaming bound names. While nominal
unification can be seen as equivalent to Miller's higher-order pattern
unification (unification problems can be inter-coded), nominal unification has
the advantage of involving only first-order syntax. This means in the presented
formalisation we only need to reason about standard inductive datatypes and
first-order operations. The main improvement of this development is a much
simpler proof for establishing the equivalence relation properties for an
inductive definition characterising when two terms are alpha-equivalent. In the
original literature, this involved a clunky mutual induction over the size of
terms involving three properties. Here we can separate the proofs and use just
structural inductions. This results in a much smoother formalisation of the
nominal unification algorithm.
https://www.isa-afp.org/entries/Nominal_Unification.html
Enjoy!
Last updated: May 02 2026 at 13:17 UTC