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 is finitary) 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.

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