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