Equational reasoning with binders and structural congruence is difficult due to the interaction between name binding and algebraic laws. Equational theories such as commutativity induce forms of permutation invariance on names that are not captured by standard approaches to the formalisation of syntax with binders. We show that in the nominal setting, this limitation can be addressed by using generalised permutation fixed-point constraints to make invariance explicit. This yields a uniform framework for reasoning about equality of nominal terms modulo α-equivalence and arbitrary equational theories. We introduce a proof system and show that it is sound and complete with respect to a nominal-set semantics, which explains how symmetry can be internalised via fixed-point constraints viewed as N-quantified stabiliser conditions. We provide examples in Milner’s π-calculus - a well-known model of concurrent computation that includes binders and non-trivial structural congruences.

Abstract Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and $$\alpha $$ α -renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in $$\alpha $$ α -equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the $$\pi $$ π -calculus.