一句话：提出基于置换不动点约束的名义项 α-等价公理化，并建立新的名义合一及 C 理论下的有穷性结果。
论文研究名义语法中 α-等价与名义合一。作者提出以置换不动点约束为原语的新公理化：从原子与项之间的置换不动点关系导出标准新鲜性关系，并证明该 α-等价公理化的正确性。由此得到一种新的名义合一概念，其解由不动点上下文与替换组成。与基于新鲜性约束的标准合一不同，该表示在考虑等式理论时表现更好：例如带交换性 C 的名义合一是 finitary，而使用新鲜性上下文时变为 infinitary。作者还定义模 A、C、AC 理论的 α-等价，并给出可靠且完备的 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 $\alpha$-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 $\alpha$-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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1902-08345,
title = {On Nominal Syntax and Permutation Fixed Points},
author = {Mauricio Ayala-Rincón and Maribel Fernández and Daniele Nantes-Sobrinho},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:19)2020}
}