Nominal Sets

Nominal sets provide a mathematical framework for handling $namebinding$ and $structuralalpha-equivalence$ using group actions. This approach avoids the non-compositional nature of global freshness by treating names as atoms subject to permutation.

Definition

Let $\mathbb{A}$ be an infinite, decidable set of atoms. A nominal set is a set $X$ equipped with a group action $(\cdot ):\text{Perm}(\mathbb{A})\times X\to X$, where $\text{Perm}(\mathbb{A})$ is the group of finite permutations of atoms, such that every element $x\in X$ is finitely supported.

A set $S\subseteq \mathbb{A}$ supports $x\in X$ if for all $\pi \in \text{Perm}(\mathbb{A})$:

$(\forall a\in S.\pi (a)=a)⟹\pi \cdot x=x$

If $x$ is finitely supported, there exists a unique least finite support, denoted $\text{supp}(x)$.

Structural Properties

• Atoms: For $a\in \mathbb{A}$, $\text{supp}(a)=\{a\}$.
• Discrete Sets: For a set $X$ with the trivial action ($\pi \cdot x=x$), $\text{supp}(x)=\varnothing$.
• Products: $X\times Y$ is nominal with $\pi \cdot (x,y)=(\pi \cdot x,\pi \cdot y)$. Note $\text{supp}(x,y)=\text{supp}(x)\cup \text{supp}(y)$.
• Functions: A function $f:X\to Y$ is equivariant if $f(\pi \cdot x)=\pi \cdot f(x)$ for all $\pi ,x$. This is equivalent to saying $\text{supp}(f)=\varnothing$ in the exponential $Y^X$.
• Power Sets: The full power set $\mathcal{P}(X)$ is not generally nominal; we must restrict to the set of finitely supported subsets ${\mathcal{P}}_{\text{fs}}(X)$.

The Freshness Quantifier

The freshness quantifier $\text{И}$ (New) is defined such that $\text{И}a.\varphi (a)$ holds if $\{a\in \mathbb{A}\mid \varphi (a)\}$ is cofinite. In the context of nominal sets:

$\text{И}a.\varphi (a,x)⟺\exists a\in \mathbb{A}.a\notin \text{supp}(x)\wedge \varphi (a,x)$

This quantifier commutes with all first-order logical connectives, including negation, which is not true for $\forall$ or $\exists$.

Name Abstraction

The abstraction set $[\mathbb{A}]X$ quotients $\mathbb{A}\times X$ by $\alpha$-equivalence:

$(a,x)\sim (b,y)⟺\exists c\notin \text{supp}(x,y).(ac)\cdot x=(bc)\cdot y$

This construction satisfies a specific adjunction: the abstraction functor $[\mathbb{A}](-)$ is right-adjoint to the “concretion” or “fresh-star” functor $(-)\star \mathbb{A}$.

Correctness Notes

• Substitution: Capture-avoiding substitution is equivariant provided the substituted terms are themselves finitely supported.
• Topos Theory: $\mathbf{Nom}$ is the Schanuel topos. It is a Grothendieck topos (specifically, the category of continuous $\text{Perm}(\mathbb{A})$-sets).
• Axiom of Choice: AC fails in $\mathbf{Nom}$. For instance, the identity relation on $\mathbb{A}$ does not admit an equivariant choice function that “picks” a representative name.
• Logic: Nominal logic is a version of HOL that integrates the $\text{И}$ quantifier and support requirements.

References

pitts2016-nominal-techniques gabbay2002-new-approach-abstract