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