允许性名义项及其合一：一种无限、共无限的名义技术方法
计算机科学中的逻辑
2023-12-27 v1
摘要
名义项将一阶项扩展为带绑定。它们缺乏一阶项和高阶项的一些性质：项必须在“新鲜性假设”的上下文中进行推理；并不总是可以为名义项“选择一个新鲜变量符号”；并不总是可以“对绑定变量符号进行alpha转换”或“通过alpha等价进行商化”；合一的概念不仅仅基于替换。允许性名义项与名义项非常相似，但它们恢复了这些性质，特别是“始终新鲜”和“始终重命名”性质。在允许性世界中，新鲜性上下文被省略，等式是固定的，合一的概念仅基于替换，而不是基于名义项中基于替换加上额外新鲜性条件的合一概念。我们证明了在转向允许性情况时不会失去表达能力，并提供了名义项合一问题及其解到允许性名义项问题及其解的注入。我们研究了允许性名义合一与高阶模式合一之间的关系。我们展示了如何以合理、完备和最优的方式翻译允许性名义合一问题和解，这些概念我们将在形式化中明确。
引用
@article{arxiv.2312.15651,
title = {Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques},
author = {Gilles Dowek and Murdoch J. Gabbay and Dominic Mulligan},
journal= {arXiv preprint arXiv:2312.15651},
year = {2023}
}