Nominal algebra includes $\alpha$-equality and freshness constraints on nominal terms endowed with a nominal set semantics that facilitates reasoning about languages with binders. Nominal unification is decidable and unitary, however, its extension with equational axioms such as Commutativity (which has a finitary first-order unification type) is no longer finitary unless permutation fixed-point constraints are used. In this paper, we extend the notion of nominal algebra by introducing fixed-point constraints and provide a sound semantics using strong nominal sets. We show, by providing a counter-example, that the class of nominal sets is not a sound denotation for this extended nominal algebra. To recover soundness we propose two different formulations of nominal algebra, one obtained by restricting to a class of fixed-point contexts that are in direct correspondence with freshness contexts and another obtained by using a different set of derivation rules.

翻译：名义代数包含对名义项的α等价性与新鲜度约束，并赋予一种名义集语义，便于对带有绑定结构的语言进行推理。名义可判定且具有单一性，然而，当将其扩展至包含交换性等等式公理时（该公理具有有限一阶合一类型），除非使用置换固定点约束，否则扩展不再具有有限性。本文通过引入固定点约束扩展了名义代数的概念，并利用强名义集提供了一种可靠的语义。我们通过构造反例证明，名义集类并非这一扩展名义代数的可靠指称。为恢复可靠性，我们提出了两种不同的名义代数形式化方案：一种是通过限制到与新鲜度上下文直接对应的固定点上下文类来实现；另一种则是通过采用不同的推导规则集来实现。