Strong Nominal Semantics for Fixed-Point Constraints

TL;DR

The paper addresses extending nominal algebra with fixed-point constraints to support equational theories such as Commutaivity, showing that naive nominal-set semantics are not sound for this extension and proposing two soundness strategies: (i) restricting to strong models (strong nominal sets) and (ii) adopting stronger derivation rules or fixed-point contexts. It develops a formal semantics for fixed-point constraints, introduces strong nominal Sigma-algebras, and proves soundness under strong models, while also presenting alternative approaches using strong fixed-point contexts and enhanced rules to regain soundness over full nominal-set semantics. The work identifies strong theories that preserve soundness, outlines translations between freshness and fixed-point formalisms, and discusses applications to nominal equational problems and unification modulo associative-commutative theories. The results set the stage for algorithmic developments in nominal equational reasoning and invite future work on completeness and practical unification methods under fixed-point semantics.

Abstract

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 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.

Figures (3)

• Figure 1: Derivation rules; $c_1,c_2,d_1,d_2$ are fresh names. Also, $\overline{\pi \curlywedge_{}\mathtt{Var}(t)} = \{\pi\curlywedge_{} X\mid X\in\mathtt{Var}(t)\}$.
• Figure 2: Derivation rules for strong judgements. Here, $\overline{c}$ denotes a list of distinct atoms $c_1,\ldots,c_n$. In all the rules $\overline{c_0}\subseteq \overline{c}$.
• Figure 3: Standard derivation rules for freshness and $\alpha$-equivalence. Here, $\mathtt{ds}(\pi,\pi') = \{a\in\mathbb{A}\mid \pi(a) \neq \pi'(a)\}$.

Theorems & Definitions (37)

• definition 1: Theory
• definition 2
• lemma 1
• proof
• lemma 2
• proof
• theorem 1
• proof
• definition 3: (Strong) $\Sigma$-algebra
• remark 1