Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0062

TitlePermissive nominal terms and their unification
AuthorsGilles Dowek, Murdoch J Gabbay, Dominic P Mulligan

We introduce permissive nominal terms, and their unification.

Nominal terms are one way to extend first-order terms with binding. However, they lack some useful properties of first-and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable symbol' for a nominal term; and it is not always possible to 'alpha-convert a bound variable symbol'.

Permissive nominal terms closely resemble nominal terms, but they recover these useful 'always fresh' and 'always alpha-rename' properties, familiar from first-and higher- order syntax. In the permissive world, freshness contexts are elided, and the notion of unifier is based on substitution alone, rather than on nominal terms' notion of substitution plus freshness conditions.

We prove that expressivity is not lost moving to the permissive case. We provide a translation from nominal terms into permissive nominal terms and we prove that a nominal unification problem is solvable if and only if its translation into permissive nominal terms is.

Finally, we investigate the precise relation between nominal unification and Miller's higher-order pattern unification. We translate nominal terms into the lambda-calculus and show that the translation may also be applied to unification problems; the result is pattern unification. This cements an existing intuition that higher-order patterns are what is needed to unify encodings of nominal terms. This builds on a translation by Levy and Villaret, and refines it; both translations are parameterised by sets of atoms, but we identify a smaller parameter set and prove that it is as small as possible. We also translate solutions of nominal unification problems to solutions of higher-order pattern unification problems. We exhibit a general class of higher-order pattern solutions and show that every pattern solution in that class is the translation of a nominal unification solution up to a permutative renaming.

GroupDependable Systems Group


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer