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.

翻译：名义项通过绑定机制扩展了一阶项。然而，它们缺少一阶项和高阶项的某些性质：项必须在"新鲜性假设"的上下文中进行推理；无法始终为名义项"选择一个新鲜变量符号"；无法始终"对绑定变量符号进行α-转换"或"通过α-等价进行商化"；统一子的概念并非仅基于替换。许可名义项与名义项高度相似，但恢复了这些性质，特别是"始终新鲜"和"始终重命名"特性。在许可领域中，新鲜性上下文被省略，相等性被固定，统一子的概念仅基于替换，而非名义项中基于替换加额外新鲜性条件的统一化概念。我们证明转向许可情形不会损失表达力，并给出了名义项统一化问题及其解到许可名义项问题及其解的注入。我们考察了许可名义统一化与高阶模式统一化之间的关系。我们展示了如何在适当的意义上（我们将给出形式化定义）以可靠、完备且最优的方式翻译许可名义统一化问题及其解。