Nominal Unification [ps]Christian Urban, Andrew Pitts, Murdoch Gabbay
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
an existing idea and introducing a key new idea. The existing
idea is terms involving explicit substitutions of names for names,
except that here we only use explicit permutations
(bijective substitutions). The key new idea 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 the classical
first-order unification algorithm 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.
The old Isabelle-2002 files can be downloaded here. A "quick and dirty" implementation of nominal unification in Ocaml can be downloaded elsewhere. |
Last modified: Thu Feb 28 20:24:23 CET 2008 [Validate this page.]