  Nominal terms extend first-order terms with binding. They lack some
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; it is not always possible to
'alpha-convert a bound variable symbol' or to 'quotient by alpha-equivalence';
the notion of unifier is not based just on substitution.
  Permissive nominal terms closely resemble nominal terms but they recover
these properties, and in particular the 'always fresh' and 'always rename'
properties. In the permissive world, freshness contexts are elided, equality is
fixed, and the notion of unifier is based on substitution alone rather than on
nominal terms' notion of unification based on substitution plus extra freshness
conditions.
  We prove that expressivity is not lost moving to the permissive case and
provide an injection of nominal terms unification problems and their solutions
into permissive nominal terms problems and their solutions. We investigate the
relation between permissive nominal unification and higher-order pattern
unification. We show how to translate permissive nominal unification problems
and solutions in a sound, complete, and optimal manner, in suitable senses
which we make formal.
