Nominal Unification [ps]

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)