Strong Nominal Semantics for Fixed-Point Constraints

Nominal algebra includes -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.