Nominal Unification
We present a generalisation of first-order unification to the
practically important case of equations between terms involving
binding operations. A substitution of terms for variables
solves such an equation if it makes the equated terms
alpha-equivalent, i.e. equal up to renaming bound names.
For the applications we have in mind, we must consider the simple,
textual form of substitution in which names occurring in terms may
be captured within the scope of binders upon substitution. We are
able to take a "nominal" approach to binding in which bound entities
are explicitly named (rather than using nameless, de Bruijn-style
representations) and yet get a version of this form of substitution
that respects alpha-equivalence and possesses good algorithmic
properties. We achieve this by adapting two existing ideas. The
first one is terms involving explicit substitutions of names for
names, except that here we only use explicit permutations
(bijective substitutions). The second one is that the unification
algorithm should solve not only equational problems, but also
problems about the freshness of names for terms. There is a
simple generalisation of classical first-order unification problems
to this setting which retains the latter's pleasant properties:
unification problems involving alpha-equivalence and freshness
are decidable; and solvable problems possess most general solutions.