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.

In an appendix we discuss some issues about the relationship between nominal unification and higher-order pattern unification.

All results in the paper have been verified in Isabelle (2004 version). Below are the theory files.

  • Swap.thy
    amongst other facts proves that swapping is a bijection (on atoms)
  • Atoms.thy
    facts about atoms occurring in swappings
  • Terms.thy
    defines terms, occurs check and the notion of subterms
  • Disagreement.thy
    proves various facts about disagreement sets
  • Fresh.thy
    defines the freshness relation and shows facts about its behaviour under swapping
  • PreEqu.thy
    defines the relation capturing the notion of alpha-equivalence (on open terms) and proves a long lemma by mutual induction over the depth of terms which is needed to show that the relation is an equivalence relation
  • Equ.thy
    proves various facts about the equivalence relations
  • Substs.thy
    defines substitutions and composition of substitutions, and establishes some facts of substitution and our equivalence relation
  • Mgu.thy
    defines the notion of unification problems and reduction rules over sets of such problems; proves that every reduction leading to the empty set produces an mgu
  • Termination.thy
    shows that every reduction reduces a (well-founded) measure, thus proves that every reduction sequence must terminate
  • Unification.thy
    proves that all solvable problems reduce only to the empty set (the "ok" configuration which provides an mgu) and all unsolvable problems reduce to a "fail" configuration (for which no unifier exists)

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.]