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.

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