论名义语法与置换不动点
On Nominal Syntax and Permutation Fixed Points
AI总结：
本文提出基于置换不动点约束的新名义α等价公理化，推导新鲜度关系，并定义模A/C/AC理论的统一化，证明C-统一化有限性且给出完备算法。
摘要：
我们提出了一种新的关于名义项的α等价关系的公理化，该公理化基于不动点约束的原始概念。我们证明了原子与项之间的标准新鲜度关系可以从更原始的置换不动点概念推导出来，并利用这一结果证明了新的α等价公理化的正确性。这产生了一种新的名义统一化概念，其中统一问题的解是一对由不动点上下文和替换组成的对。尽管与基于新鲜度约束的标准名义统一化概念相比，这可能显得不那么自然，但在考虑等式理论时，基于不动点约束的统一化概念表现得更好：例如，在存在交换性的情况下，名义统一化仍然是有限性的，而当统一化用新鲜度上下文表示时，它则变成无限性的。我们提供了模等式理论的α等价定义，这些等式理论考虑了A、C和AC理论。基于这一等价概念，我们证明了C-统一化是有限性的，并提供了一个可靠且完备的C-统一化算法，作为迈向模AC及其他具有置换性质的等式理论的名义统一化发展的第一步。
英文摘要：
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $α$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $α$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
