Separation and Renaming in Nominal Sets

TL;DR

This paper introduces separated nominal automata, which are exponentially smaller than classical ones, by relating nominal sets to nominal renaming sets through categorical adjunctions and substitution-based semantics.

Contribution

It establishes a categorical connection between nominal sets and nominal renaming sets and defines separated nominal automata with potential size advantages.

Findings

Separated nominal automata can be exponentially smaller than classical automata.

The categorical adjunction relates separated product to Cartesian product.

Semantics closed under substitutions enables size reduction.

Abstract

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. These automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.

Equations

$$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.65282pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\crcr}}}\ignorespaces{\hbox{\kern-22.65282pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\mathsf{Pm}\text{-}\mathbf{Nom}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 46.79799pt\raise 15.39166pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{F}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 84.4328pt\raise 6.31337pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern 46.65282pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bot}$}}}}}}}{\hbox{\kern 84.43062pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\mathsf{Sb}\text{-}\mathbf{Nom}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 46.76349pt\raise-15.39166pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{U}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 8.58057pt\raise-2.99985pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces,$$

$$\mathsf{Sb}=\{m:\mathbb{A}\to \mathbb{A}\mid m(a)\ne a\text{ for finitely many }a\}$$

$$\mathsf{Pm}=\{g\in \mathsf{Sb}\mid g\text{ is a bijection}\}$$

$$U:\mathsf{Sb}\text{-}\mathbf{Set}\to \mathsf{Pm}\text{-}\mathbf{Set}.$$

$$X\ast Y=\{(x,y)\mid x\#y\}.$$

$$F(X)=\{(m,x)\mid m\in \mathsf{Sb},x\in X\}{/}_{\sim },$$

$$(m,gx)$$

$$(m,x)$$

$$F:\mathsf{Pm}\text{-}\mathbf{Nom}\to \mathsf{Sb}\text{-}\mathbf{Nom},$$

$$\mathsf{Pm}\text{-}\mathbf{Nom}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$p=⟨F({\pi }_1),F({\pi }_2)⟩:F(X\ast Y)\to F(X)\times F(Y)$$

$$m(x)=\{\begin{array}{ll}{m}_1(x)& \text{if }x\in \mathsf{supp}(x)\\ m_2(g^{-1}(x))& \text{if }x\in \mathsf{supp}(y^{\prime })\\ x& \text{otherwise}.\end{array}$$

$$g_0(z)=\{\begin{array}{ll}{g}_x(z)& \text{if }z\in C\\ g_y(z)& \text{if }z\in D.\end{array}$$

$$\{my\mid m\in \mathsf{Sb}\}=\{gy\mid g\in \mathsf{Pm}\}.$$

$$\varphi :(X-\ast U(Y))\to U(F(X){\to }_{\text{fs}}^{\mathsf{Sb}}Y)$$

$$F(X-\ast U(Y))\times F(X)\stackrel{p^{-1}}{\to }F((X-\ast U(Y))\ast X)\stackrel{F(\mathrm{ev})}{\to }FU(Y)\stackrel{ϵ}{\to }Y,$$

$$q:U(X\times Y)\stackrel{=}{\to }U(X)\times U(Y)$$

$$l(x,\epsilon )=o(x),l(x,aw)=l(\delta (x,a),w)$$

$$\Sigma =\{\mathrm{Put}(a)\mid a\in \mathbb{A}\}\cup \{\text{Pop}\},O=\mathbb{A}\cup \{\perp \}.$$

$$Q={\mathbb{A}}^{\le n}\cup \{\perp \}{q}_0=\epsilon o(a_1\dots a_k)=\{\begin{array}{ll}{a}_1& \text{if }k\ge 1\\ \perp & \text{otherwise}\end{array}$$

$$\begin{array}[]{rcl}\delta(a_{1}\ldots a_{k},\mathop{\text{\sf Put}}(b))&=&\begin{cases}a_{1}\ldots a_{k}b&\text{if }k<n\\ \perp&\text{otherwise}\end{cases}\qquad\delta(\bot,x)=\perp\\[10.0pt] \delta(a_{1}\ldots a_{k},\text{\sf Pop})&=&\begin{cases}a_{2}\ldots a_{k}&\text{if }k>0\\ \perp&\text{otherwise}\end{cases}\end{array}$$

$$s(x,\epsilon )=o(x),s(x,aw)=s(\delta (x,a),w)$$

$$\frac{S:(U\Sigma {)}^{(\ast )}\to UO\text{ Pm-equivariant}}{\overline{S}:{\Sigma }^{\ast }\to O\text{ Sb-equivariant}}$$

$$m(a)=\{\begin{array}{ll}{a}_i& \text{ if }a=b_i\text{ for some }i\\ a& \text{ otherwise}\end{array}$$

$$R_{{\mathcal{A}}_{\ast }}={\mathbb{A}}^{(\le n)}\cup \{\perp \}.$$

$$⟨o,{\delta }^{♭}⟩:Q\to O\times (\Sigma {\to }_{\text{fs}}^{M}Q)$$

$$l(x,\epsilon )=o(x),l(x,aw)=l(\delta (x,a),w)$$

$$\mathrm{CoAlg}(B_{\ast })\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\lambda :UO\times (\Sigma -\ast UX)\stackrel{\mathrm{id}\times \varphi }{\to }UO\times U(F\Sigma {\to }_{\text{fs}}^{\mathsf{Sb}}X)\stackrel{\cong }{\to }U(O\times (F\Sigma {\to }_{\text{fs}}^{\mathsf{Sb}}X)),$$

$$\mathsf{Pm}\text{-}\mathbf{Nom}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$(r\circ \beta \circ \alpha \circ \varphi {)}^{♯}(\psi ,x)$$

Full text

1 Introduction

Nominal sets are abstract sets which allow one to reason over sets with names, in terms of permutations and symmetries. Since their introduction in computer science [10], they have been widely used for implementing and reasoning over syntax with binders [19]. Further, nominal techniques have been related to computability theory [4] and automata theory [3], where they provide an elegant means of studying languages over infinite alphabets. This embeds nominal techniques in a broader setting of symmetry aware computation [21].

Gabbay, one of the pioneers of nominal techniques described a variation on the theme: nominal renaming sets [8, 9]. Nominal renaming sets are equipped with a monoid action of arbitrary (possibly non-injective) substitution of names, in contrast to nominal sets, which only involve a group action of permutations.

In this paper, we systematically relate nominal renaming sets to nominal sets. We start by establishing a categorical adjunction (Section 3):

[TABLE]

where ${\mathsf{Pm}\text{-}\mathbf{Nom}}$ is the usual category of nominal sets and ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ the category of nominal renaming sets. The right adjoint $U$ simply forgets the action of non-injective substitutions. The left adjoint $F$ freely extends a nominal set with elements representing the application of such substitutions. For instance, $F$ maps the nominal set $\mathbb{A}^{(*)}$ of all words consisting of distinct atoms to the nominal renaming set $\mathbb{A}^{*}$ consisting of all words over the atoms.

In fact, the latter follows from one of the main results of this paper: $F$ maps the separated product $X\mathop{\ast}Y$ of nominal sets to the Cartesian product of nominal renaming sets. Additionally, under certain conditions, $U$ maps the exponent to the magic wand $X\mathrel{-\kern-3.00003pt{\ast}}Y$, which is the right adjoint of the separated product. The separated product consists of those pairs whose elements have disjoint supports. This is relevant for name abstraction [19], and has also been studied in the setting of presheaf categories, aimed towards separation logic [18].

We apply these connections between nominal sets and renaming sets in the context of automata theory. Nominal automata are expressively equivalent to the more classical register automata [2], and have appealing properties that register automata lack, such as unique minimal automata. However, moving from register automata to nominal automata can lead to an exponential blow-up in the number of states.111Here ‘number of states’ refers to the number of orbits in the state space.

As a motivating example, we consider a language modelling an $n$-bounded FIFO queue. The input alphabet is given by $\Sigma=\{\mathop{\text{\sf Put}}(a)\mid a\in\mathbb{A}\}\cup\{\text{\sf Pop}\}$, and the output alphabet by $O=\mathbb{A}\cup\{\perp\}$ (here, $\perp$ is a null value). The (generalised) language $L_{n}\colon\Sigma^{*}\to O$ maps a sequence of queue operations to the resulting top element when starting from the empty queue, or to $\perp$ if this is undefined. The language $L_{n}$ can be recognised by a nominal (Moore) automaton, but this requires an exponential number of states in $n$, as the automaton distinguishes internally between all possible equalities among elements in the queue [17].

Based on the observation that $L_{n}$ is closed under substitutions, we can come up with a linear automata-theoretic representation. To this end, we define the new notion of separated nominal automaton, where the transition function is only defined for pairs of states and letters with a disjoint support (Section 4). Using the aforementioned categorical framework, we can go back and forth between languages from separated automata and languages which are closed under substitutions. In the FIFO example, the separated automaton obtained from the original nominal automaton has only $n+1$ states, thus dramatically reducing the number of states. We expect that such a reduction is useful in many applications, such as automata learning [17].

2 Monoid actions and nominal sets

In order to capture both the standard notion of nominal sets [19] and sets with more general renaming actions [9], we start by defining monoid actions.

Definition 1**.**

Let $(M,\cdot,1)$ be a monoid. An $M$-set is a set $X$ together with a function ${\cdot}\colon M\times X\to X$ such that $1\cdot x=x$ and $m\cdot(n\cdot x)=(m\cdot n)\cdot x$ for all $m,n\in M$ and $x\in X$. The function ${\cdot}$ is called an $M$-action and $m\cdot x$ is often written by juxtaposition $mx$. A function $f\colon X\to Y$ between two $M$-sets is $M$-equivariant if $m\cdot f(x)=f(m\cdot x)$ for all $m\in M$ and $x\in X$. The class of $M$-sets together with equivariant maps forms a category ${M\text{-}\mathbf{Set}}$.

Let $\mathbb{A}=\{a,b,c,\ldots\}$ be a countable infinite set of atoms. The two main instances of $M$ considered in this paper are the monoid

[TABLE]

of all (finite) substitutions (with composition as multiplication), and the monoid

[TABLE]

of all (finite) permutations. Since $\mathsf{Pm}$ is a submonoid of $\mathsf{Sb}$, any $\mathsf{Sb}$-set is also a $\mathsf{Pm}$-set; and any $\mathsf{Sb}$-equivariant map is also $\mathsf{Pm}$-equivariant. This gives rise to a forgetful functor

[TABLE]

The set $\mathbb{A}$ is an $\mathsf{Sb}$-set by defining $m\cdot a=m(a)$. Given an $M$-set $X$, the set $\mathcal{P}(X)$ of subsets of $X$ is an $M$-set, with the action defined by direct image.

For a $\mathsf{Pm}$-set $X$, the orbit of an element $x$ is the set $\operatorname{orb}(x)=\{g\cdot x\mid g\in\mathsf{Pm}\}$. We say $X$ is orbit-finite if the set $\{\operatorname{orb}(x)\mid x\in X\}$ is finite.

For any monoid $M$, the category ${M\text{-}\mathbf{Set}}$ is symmetric monoidal closed. The product of two $M$-sets is given by the Cartesian product, with the action defined pointwise: $m\cdot(x,y)=(m\cdot x,m\cdot y)$. In ${M\text{-}\mathbf{Set}}$, the exponent $X\to^{M}Y$ is given by the set $\{f\colon M\times X\to Y\mid f\text{ is equivariant}\}$.222If we write a regular arrow $\to$, then we mean a map in the category. Exponent objects will always be denoted by annotated arrows. The action on such an $f\colon M\times X\to Y$ is defined by $(m\cdot f)(n,x)=f(mn,x)$. A good introduction to the construction of the exponent is given by Simmons [25]. If $M$ is a group, a simpler description of the exponent may be given, carried by the set of all functions $f\colon X\to Y$, with the action given by $(g\cdot f)(x)=g\cdot f(g^{-1}\cdot x)$.

2.1 Nominal $M$-sets

The notion of nominal set is usually defined w.r.t. a $\mathsf{Pm}$-action. Here, we use the generalisation to $\mathsf{Sb}$-actions from [9]. Throughout this section, let $M$ denote a submonoid of $\mathsf{Sb}$.

Definition 2**.**

Let $X$ be an $M$-set, and $x\in X$ an element. A set $C\subset\mathbb{A}$ is an ($M$)-support of $x$ if for all $m_{1},m_{2}\in M$ s.t. $m_{1}|_{C}=m_{2}|_{C}$ we have $m_{1}x=m_{2}x$. An $M$-set $X$ is called nominal if every element $x$ has a finite $M$-support.

Nominal $M$-sets and equivariant maps form a full subcategory of ${M\text{-}\mathbf{Set}}$, denoted by ${M\text{-}\mathbf{Nom}}$. The $M$-set $\mathbb{A}$ of atoms is nominal. The powerset $\mathcal{P}(X)$ of a nominal set is not nominal in general; the restriction to finitely supported elements is.

If $M$ is a group, then the notion of support can be simplified by using inverses. To see this, first note that, given elements $g_{1},g_{2}\in M$, $g_{1}|_{C}=g_{2}|_{C}$ can equivalently be written as $g_{1}g_{2}^{-1}|_{C}=\operatorname{id}|_{C}$. Second, the statement $xg_{1}=xg_{2}$ can be expressed as $xg_{1}g_{2}^{-1}=x$. Hence, $C$ is a support iff $g|_{C}=\operatorname{id}_{C}$ implies $gx=x$ for all $g$, which is the standard definition for nominal sets over a group [3, 19]. Surprisingly, a similar characterisation also holds for $\mathsf{Sb}$-sets [9]. Moreover, recall that every $\mathsf{Sb}$-set is also a $\mathsf{Pm}$-set; the associated notions of support coincide on nominal $\mathsf{Sb}$-sets, as shown by the following result. In particular, this means that the forgetful functor (1) restricts to $U\colon{\mathsf{Sb}\text{-}\mathbf{Nom}}\to{\mathsf{Pm}\text{-}\mathbf{Nom}}$.

Lemma 1**.**

[8*, Theorem 4.8]**

Let $X$ be a nominal $\mathsf{Sb}$-set, $x\in X$, and $C\subset\mathbb{A}$. Then $C$ is an $\mathsf{Sb}$-support of $x$ iff it is a $\mathsf{Pm}$-support of $x$.*

Remark 1*.*

It is not true that any $\mathsf{Pm}$-support is an $\mathsf{Sb}$-support. The condition that $X$ is nominal, in the above lemma, is crucial. Let $X=\mathbb{A}+1$ and define the following $\mathsf{Sb}$-action: $m\cdot a=m(a)$ if $m$ is injective, $m\cdot a=\ast$ if $m$ is non-injective, and $m\cdot\ast=\ast$. This is a well-defined $\mathsf{Sb}$-set, but is not nominal. Now consider $U(X)$, this is the $\mathsf{Pm}$-set $\mathbb{A}+1$ with the natural action, which is a nominal $\mathsf{Pm}$-set! In particular, as a $\mathsf{Pm}$-set each element has a finite support, but as a $\mathsf{Sb}$-set the supports are infinite.

This counterexample is similar to the “exploding nominal sets” in [8], but even worse behaved. We like to call them nuclear sets, since an element will collapse when hit by a non-injective map, no matter how far away the non-injectivity occurs.

For $M\in\{\mathsf{Sb},\mathsf{Pm}\}$, any element $x\in X$ of a nominal $M$-set $X$ has a least finite support (w.r.t. set inclusion). We denote the least finite support of an element $x\in X$ by $\mathsf{supp}(x)$. Note that by Lemma 1, the set $\mathsf{supp}(x)$ is independent of whether a nominal $\mathsf{Sb}$-set $X$ is viewed as an $\mathsf{Sb}$-set or a $\mathsf{Pm}$-set. The dimension of $X$ is given by $\dim(X)=\max\{|\mathsf{supp}(x)|\mid x\in X\}$, where $|\mathsf{supp}(x)|$ is the cardinality of $\mathsf{supp}(x)$.

We list some basic properties of nominal $M$-sets, which have known counterparts for the case that $M$ is a group [3], and when $M=\mathsf{Sb}$ [9].

Lemma 2**.**

Let $X$ be an $M$-nominal set. If $C$ supports an element $x\in X$, then $m\cdot C$ supports $m\cdot x$ for all $m\in M$. Moreover, any $g\in\mathsf{Pm}$ preserves least supports: $g\cdot\mathsf{supp}(x)=\mathsf{supp}(gx)$.

The latter equality does not hold in general for a monoid $M$. For instance, the ‘exploding’ nominal renaming sets [9] give counterexamples for $M=\mathsf{Sb}$.

Lemma 3**.**

Given $M$-nominal sets $X,Y$ and a map $f\colon X\to Y$, if $f$ is $M$-equivariant and $C$ supports an element $x\in X$, then $C$ supports $f(x)$.

The category ${M\text{-}\mathbf{Nom}}$ is symmetric monoidal closed, with the product inherited from ${M\text{-}\mathbf{Set}}$, thus simply given by Cartesian product. The exponent is given by the restriction of the exponent $X\to^{M}Y$ in ${M\text{-}\mathbf{Set}}$ to the set of finitely supported functions, denoted by $X\mathrel{\to_{\text{fs}}^{M}}Y$. This is similar to the exponents of nominal sets with 01-substitutions from [20].

Remark 2*.*

In [9] a different presentation of the exponent in ${M\text{-}\mathbf{Nom}}$ is given, based on a certain extension of partial functions. We prefer the previous characterisation, as it is derived in a straightforward way from the exponent in ${M\text{-}\mathbf{Set}}$.

2.2 Separated product

Definition 3**.**

Two elements $x,y\in X$ of a $\mathsf{Pm}$-nominal set are called separated, denoted by $x\mathop{\#}y$, if there are disjoint sets $C_{1},C_{2}\subset\mathbb{A}$ such that $C_{1}$ supports $x$ and $C_{2}$ supports $y$. The separated product of $\mathsf{Pm}$-nominal sets $X$ and $Y$ is defined as

[TABLE]

We extend the separated product to the separated power, defined by $X^{(0)}=1$ and $X^{(n+1)}=X^{(n)}\mathop{\ast}X$, and the set of separated words $X^{(\ast)}=\bigcup_{i}X^{(i)}$. The separated product is an equivariant subset $X\mathop{\ast}Y\subseteq X\times Y$. Consequently, we have equivariant projection maps $X\mathop{\ast}Y\to X$ and $X\mathop{\ast}Y\to Y$.

Example 1*.*

Two finite sets $C,D\subset\mathbb{A}$ are separated precisely when they are disjoint. An important example is the set $\mathbb{A}^{(\ast)}$ of separated words over the atoms: it consists of those words where all letters are distinct.

The separated product gives rise to another symmetric closed monoidal structure on ${\mathsf{Pm}\text{-}\mathbf{Nom}}$, with $1$ as unit, and the exponential object given by magic wand $X\mathrel{-\kern-3.00003pt{\ast}}Y$. An explicit characterisation of $X\mathrel{-\kern-3.00003pt{\ast}}Y$ is not needed in the remainder of this paper, but for a complete presentation we briefly recall the description from [23] (see also [19] and [5]). First, define a $\mathsf{Pm}$-action on the set of partial functions $f\colon X\rightharpoonup Y$ by $(g\cdot f)(x)=g\cdot f(g^{-1}\cdot x)$ if $f(g^{-1}\cdot x)$ is defined. Now, such a partial function $f\colon X\rightharpoonup Y$ is called separating if $f$ is finitely supported, $f(x)$ is defined iff $f\mathop{\#}x$, and $\mathsf{supp}(f)=\bigcup_{x\in\mathrm{dom}(f)}\mathsf{supp}(f(x))\setminus\mathsf{supp}(x)$. Finally, $X\mathrel{-\kern-3.00003pt{\ast}}Y=\{f\colon X\rightharpoonup Y\mid f\text{ is separating}\}$. See [23] for a proof and explanation.

Remark 3*.*

The special case $\mathbb{A}\mathrel{-\kern-3.00003pt{\ast}}Y$ coincides with $[\mathbb{A}]Y$, the set of name abstractions [19]. The latter is generalised to $[X]Y$ in [7]. In [5] it is shown that the coincidence $[X]Y\cong(X\mathrel{-\kern-3.00003pt{\ast}}Y)$ only holds under strong assumptions (including that $X$ is single-orbit).

Remark 4*.*

An analogue of the separated product does not seem to exist for nominal $\mathsf{Sb}$-sets. For instance, consider the set $\mathbb{A}\times\mathbb{A}$. As a $\mathsf{Pm}$-set, it has four equivariant subsets: $\emptyset,\{(a,a)\mid a\in\mathbb{A}\}$, $\mathbb{A}\mathop{\ast}\mathbb{A}$, and $\mathbb{A}\times\mathbb{A}$. However, the set $\mathbb{A}\mathop{\ast}\mathbb{A}$ is not an equivariant subset when considering $\mathbb{A}\times\mathbb{A}$ as an $\mathsf{Sb}$-set.

3 A monoidal construction from $\mathsf{Pm}$-sets to $\mathsf{Sb}$-sets

In this section, we provide a free construction, extending nominal $\mathsf{Pm}$-sets to nominal $\mathsf{Sb}$-sets. We use this as a basis to relate the separated product and exponent (in ${\mathsf{Pm}\text{-}\mathbf{Nom}}$) to the product and exponent in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$. The main results are:

Theorem 1: the forgetful functor $U\colon{\mathsf{Sb}\text{-}\mathbf{Nom}}\to{\mathsf{Pm}\text{-}\mathbf{Nom}}$ has a left adjoint $F$; 2. 2.

Theorem 2: this $F$ is monoidal: it maps separated products to products; 3. 3.

Theorem 3 and Corollary 3: $U$ maps the exponent object in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ to the right adjoint $\mathrel{-\kern-3.00003pt{\ast}}$ of the separated product, if the domain has dimension smaller or equal to $1$.

Together, these results form the categorical infrastructure to relate nominal languages to separated languages and automata in Section 4.

Definition 4**.**

Given a $\mathsf{Pm}$-nominal set $X$, we define a nominal $\mathsf{Sb}$-set $F(X)$ as follows. Define the set

[TABLE]

where $\sim$ is the least equivalence relation containing:

[TABLE]

for all $x\in X$, $m,m^{\prime}\in\mathsf{Sb}$ and $g\in\mathsf{Pm}$. Note that $mg=m\circ g$, i.e., simply the monoid operation of $\mathsf{Sb}$. The equivalence class of a pair $(m,x)$ is denoted by $[m,x]$. We define an $\mathsf{Sb}$-action on $F(X)$ as $n\cdot[m,x]=[nm,x]$.

Well-definedness is proved as part of Proposition 1 below. Informally, an equivalence class $[m,x]\in F(X)$ behaves “as if $m$ acted on $x$”. The first equation (2) ensures compatibility with the $\mathsf{Pm}$-action on $x$, and the second equation (3) ensures that $[m,x]$ only depends the relevant part of $m$.

Example 2*.*

Here are a few examples of the application of $F$. We do not give direct proofs, but the first two will be treated more systematically later in this section (see Corollary 2). For the third, note that $\mathbb{A}\times\mathbb{A}$ consist of two orbits, $\mathbb{A}\mathop{\ast}\mathbb{A}$ and the diagonal $\{(a,a)\mid a\in\mathbb{A}\}$.

• •

$F(\mathbb{A})\cong\mathbb{A}$.

• •

$F(\mathbb{A}^{(*)})\cong\mathbb{A}^{*}$.

• •

$F(\mathbb{A}\times\mathbb{A})\cong\mathbb{A}^{2}+\mathbb{A}$.

The following characterisation of $\sim$ is useful in proofs. (This lemma is proven in the Appendix.)

Lemma 4**.**

We have $(m_{1},x_{1})\sim(m_{2},x_{2})$ iff there is a permutation $g\in\mathsf{Pm}$ such that $gx_{1}=x_{2}$ and $m_{1}|_{C}=m_{2}g|_{C}$, for $C$ some $\mathsf{Pm}$-support of $x_{1}$.

Remark 5*.*

The first relation (2) in Definition 4 comes from the construction of “extension of scalars” in commutative algebra [1]. In that context, one has a ring homomorphism $f\colon A\to B$ and an $A$-module $M$ and wishes to obtain a $B$-module. This is constructed by the tensor product $B\otimes_{A}M$ and it is here that the relation $(b,am)\sim(ba,m)$ is used ($B$ is a right $A$-module via $f$).

Proposition 1**.**

The construction $F$ in Definition 4 extends to a functor

[TABLE]

defined on an equivariant map $f\colon X\to Y$ by $F(f)([m,x])=[m,f(x)]\in F(Y)$.

Proof.

We first prove well-definedness and then the functoriality.

$F(X)$** is an $\mathsf{Sb}$-set.** To this end we check that the $\mathsf{Sb}$-action is well-defined. Let $[m_{1},x_{1}]=[m_{2},x_{2}]\in F(X)$ and let $m\in\mathsf{Sb}$. By Lemma 4, there is some permutation $g$ such that $gx_{1}=x_{2}$ and $m_{1}|_{C}=m_{2}g|_{C}$ for some support $C$ of $x_{1}$. By post-composition with $m$ we get $mm_{1}|_{C}=mm_{2}g|_{C}$, which means (again by the lemma) that $[mm_{1},x_{1}]=[mm_{2},x_{2}]$. Thus $m[m_{1},x_{1}]=m[m_{2},x_{2}]$, which concludes well-definedness.

For associativity and unitality of the $\mathsf{Sb}$-action, we simply note that it is directly defined by left multiplication of $\mathsf{Sb}$ which is associative and unital. This concludes that $F(X)$ is an $\mathsf{Sb}$-set.

$F(X)$** is a nominal $\mathsf{Sb}$ set.** Given an element $[m,x]\in F(X)$ and a $\mathsf{Pm}$-support $C$ of $x$, we will prove that $m\cdot C$ is an $\mathsf{Sb}$-support for $[m,x]$. Suppose that we have $m_{1},m_{2}\in\mathsf{Sb}$ such that $m_{1}|_{m\cdot C}=m_{2}|_{m\cdot C}$. By pre-composition with $m$ we get $m_{1}m|_{C}=m_{2}m|_{C}$ and this leads us to conclude $[m_{1}m,x]=[m_{2}m,x]$. So $m_{1}[m,x]=m_{2}[m,x]$ as required.

Functoriality. Let $f\colon X\to Y$ be a $\mathsf{Pm}$-equivariant map. To see that $F(f)$ is well-defined consider $[m_{1},x_{1}]=[m_{2},x_{2}]$. By Lemma 4, there is a permutation $g$ such that $gx_{1}=x_{2}$ and $m_{1}|_{C}=m_{2}g|_{C}$ for some support $C$ of $x_{1}$. Applying $F(f)$ gives on one hand $[m_{1},f(x_{1})]$ and on the other hand $[m_{2},f(x_{2})]=[m_{2},f(gx_{1})]=[m_{2},gf(x_{1})]=[m_{2}g,f(x_{1})]$ (we used equivariance in the second step). Since $m_{1}|_{C}=m_{2}g|_{C}$ and $f$ preserves supports we have $[m_{2}g,f(x_{1})]=[m_{1},f(x_{1})]$.

For $\mathsf{Sb}$-equivariance we consider both $n\cdot F(f)([m,x])=n[m,f(x)]=[nm,f(x)]$ and $F(f)(n\cdot[m,x])=F(f)([nm,x])=[nm,f(x)]$. This shows that $nF(f)([m,x])=F(f)(n[m,x])$ and concludes that we have a map $F(f)\colon F(X)\to F(Y)$.

The fact that $F$ preserves the identity function and composition follows from the definition directly. ∎

Theorem 1**.**

The functor $F$ is left adjoint to $U$:

[TABLE]

Proof.

We show that, for every nominal set $X$, there is a map $\eta_{X}\colon X\to UF(X)$ with the necessary universal property: for every $\mathsf{Pm}$-equivariant $f\colon X\to U(Y)$ there is a unique $\mathsf{Sb}$-equivariant map $f^{\sharp}\colon FX\to Y$ such that $U(f^{\sharp})\circ\eta_{X}=f$. Define $\eta_{X}$ by $\eta_{X}(x)=[\operatorname{id},x]$. This is equivariant: $g\cdot\eta_{X}(x)=g[\operatorname{id},x]=[g,x]=[\operatorname{id},gx]=\eta_{X}(gx)$. Now, for $f\colon X\rightarrow U(Y)$, define $f^{\sharp}([m,x])=m\cdot f(x)$ for $x\in X$ and $m\in\mathsf{Sb}$. Then $U(f^{\sharp})\circ\eta_{X}(x)=f^{\sharp}([\operatorname{id},x])=\operatorname{id}\cdot f(x)=f(x)$.

To show that $f^{\sharp}$ is well-defined, consider $[m_{1},x_{1}]=[m_{2},x_{2}]$ (we have to prove that $m_{1}\cdot f(x_{1})=m_{2}\cdot f(x_{2})$). By Lemma 4, there is a $g\in\mathsf{Pm}$ such that $gx_{1}=x_{2}$ and $m_{2}g|_{C}=m_{1}|_{C}$ for a $\mathsf{Pm}$-support $C$ of $x_{1}$. Now $C$ is also a $\mathsf{Pm}$-support for $f(x)$ and hence it is an $\mathsf{Sb}$-support of $f(x)$ (Lemma 1). We conclude that $m_{2}\cdot f(x_{2})=m_{2}\cdot f(gx_{1})=m_{2}g\cdot f(x_{1})=m_{1}\cdot f(x_{1})$ (we use $\mathsf{Pm}$-equivariance in the one but last step and $\mathsf{Sb}$-support in the last step). Finally, $\mathsf{Sb}$-equivariance of $f^{\sharp}$ and uniqueness are straightforward calculations (see Appendix). ∎

The counit $\epsilon\colon FU(Y)\to Y$ is defined by $\epsilon([m,x])=m\cdot x$. For the inverse of $-^{\sharp}$, let $g\colon F(X)\to Y$ be an $\mathsf{Sb}$-equivariant map; then $g^{\flat}\colon X\to U(Y)$ is given by $g^{\flat}(x)=g([\operatorname{id},x])$. Note that the unit $\eta$ is a $\mathsf{Pm}$-equivariant map, hence it preserves supports (i.e., any support of $x$ also supports $[\operatorname{id},x]$). This also means that if $C$ is a support of $x$, then $m\cdot C$ is a support of $[m,x]$ (by Lemma 2).

3.1 On (separated) products

The functor $F$ not only preserves coproducts, being a left adjoint, but it also maps the separated product to products:

Theorem 2**.**

The functor $F$ is strong monoidal, from the monoidal category $({\mathsf{Pm}\text{-}\mathbf{Set}},\mathop{\ast},1)$ to $({\mathsf{Sb}\text{-}\mathbf{Set}},\times,1)$. In particular, the map $p$ given by

[TABLE]

is an isomorphism, natural in $X$ and $Y$.

Proof.

We prove that $p$ is an isomorphism. It suffices to show that $p$ is injective and surjective (Lemma 10). Note that $p([m,(x,y)])=([m,x],[m,y])$.

Surjectivity. Let $([m_{1},x],[m_{2},y])$ be an element of $F(X)\times F(Y)$. We take an element $y^{\prime}\in Y$ such that $y^{\prime}\mathop{\#}\mathsf{supp}(x)$ and $y^{\prime}=gy$ for some $g\in\mathsf{Pm}$. Now we have an element $(x,y^{\prime})\in X\mathop{\ast}Y$. By Lemma 2, we have $\mathsf{supp}(y^{\prime})=\mathsf{supp}(y)$. Define the map

[TABLE]

(Observe that $\mathsf{supp}(x)\mathop{\#}\mathsf{supp}(y^{\prime})$, so the cases are not overlapping.) The map $m$ is an element of $\mathsf{Sb}$. Now consider the element $z=[m,(x,y^{\prime})]\in F(X\mathop{\ast}Y)$. Applying $p$ to $z$ gives the element $([m,x],[m,y^{\prime}])$. First, we note that $[m,x]=[m_{1},x]$ by the definition of $m$. Second, we show that $[m,y^{\prime}]=[m_{2},y]$. Observe that $mg|_{\mathsf{supp}(y)}=m_{2}|_{\mathsf{supp}(y)}$ by definition of $m$. Since $\mathsf{supp}(y)$ is a support of $y$, we have $[mg,y]=[m_{2},y]$, and since $[mg,y]=[m,gy]=[m,y^{\prime}]$ we are done. Hence $p([m,(x,y^{\prime})])=([m,x],[m,y^{\prime}])=([m_{1},x],[m_{2},y])$, so $p$ is surjective.

Injectivity. Let $[m_{1},(x_{1},y_{1})]$ and $[m_{2},(x_{2},y_{2})]$ be two elements. Suppose that they are mapped to the same element, i.e., $[m_{1},x_{1}]=[m_{2},x_{2}]$ and $[m_{1},y_{1}]=[m_{2},y_{2}]$. Then there are permutations $g_{x},g_{y}$ such that $x_{2}=g_{x}x_{1}$ and $y_{2}=g_{y}y_{1}$. Moreover, let $C=\mathsf{supp}(x_{1})$ and $D=\mathsf{supp}(y_{1})$; then we have $m_{1}|_{C}=m_{2}g_{x}|_{C}$ and $m_{1}|_{D}=m_{2}g_{y}|_{D}$. In order to show the two original elements are equal, we have to provide a single permutation $g$. Define for, $z\in C\cup D$,

[TABLE]

(Again, $C$ and $D$ are disjoint.) The function $g_{0}$ is injective since the least supports of $x_{2}$ and $y_{2}$ are disjoint. Hence $g_{0}$ defines a local isomorphism from $C\cup D$ to $g_{0}(C\cup D)$. By homogeneity [19], the map $g_{0}$ extends to a permutation $g\in\mathsf{Pm}$ with $g(z)=g_{x}(z)$ for $z\in C$ and $g(z)=g_{y}(z)$ for $z\in D$. In particular we get $(x_{2},y_{2})=g(x_{1},y_{1})$. We also obtain $m_{1}|_{C\cup D}=m_{2}g|_{C\cup D}$. This proves that $[m_{1},(x_{1},y_{1})]=[m_{2},(x_{2},y_{2})]$, and so the map $p$ is injective.

Unit and coherence. To show that $F$ preserves the unit, we note that $[m,1]=[m^{\prime},1]$ for every $m,m^{\prime}\in\mathsf{Sb}$, as the empty set supports $1$ and so $m|_{\emptyset}=m^{\prime}|_{\emptyset}$ vacuously holds. We conclude $F(1)$ is a singleton. ∎

Since $F$ also preserves coproducts (being a left adjoint), we obtain that $F$ maps the set of separated words to the set of all words.

Corollary 1**.**

For any $\mathsf{Pm}$-nominal set $X$, we have $F(X^{(*)})\cong(FX)^{*}$.

As we will show below, the functor $F$ preserves the set $\mathbb{A}$ of atoms. This is an instance of a more general result about preservation of one-dimensional objects.

Proposition 2**.**

The functors $F$ and $U$ are equivalences on $\leq 1$-dimensional objects. Concretely, for $X\in{\mathsf{Pm}\text{-}\mathbf{Nom}}$ and $Y\in{\mathsf{Sb}\text{-}\mathbf{Nom}}$:

If $\dim(X)\leq 1$, then the unit $\eta\colon X\to UF(X)$ is an isomorphism. 2. 2.

If $\dim(Y)\leq 1$, then the co-unit $\epsilon\colon FU(X)\to X$ is an isomorphism.

Before we prove this proposition, we need the following technical property of $\leq 1$-dimensional $\mathsf{Sb}$-sets.

Lemma 5**.**

Let $Y$ be a nominal $\mathsf{Sb}$-set. If an element $y\in Y$ is supported by a singleton set (or even the empty set), then

[TABLE]

Proof.

Let $y\in Y$ be supported by $\{a\}$ and let $m\in\mathsf{Sb}$. Now consider $b=m(a)$ and the bijection $g=(a\,b)$. Now $m|_{\{a\}}=g|_{\{a\}}$, meaning that $my=gy$. So the set $\{my\mid m\in\mathsf{Sb}\}$ is contained in $\{gy\mid g\in\mathsf{Pm}\}$. The inclusion the other way is trivial, which means $\{my\mid m\in\mathsf{Sb}\}=\{gy\mid g\in\mathsf{Pm}\}$. ∎

Proof of Proposition 2.

It is easy to see that $\eta\colon x\mapsto[\operatorname{id},x]$ is injective. Now to see that $\eta$ is surjective, let $[m,x]\in UF(X)$ and consider a support $\{a\}$ of $x$ (this is a singleton or empty since $\dim(X)\leq 1$). Let $b=m(a)$ and consider the swap $g=(a\,b)$. Now $[m,x]=[mg^{-1},gx]$ and note that $\{b\}$ supports $gx$ and $mg^{-1}|_{\{b\}}=\operatorname{id}|_{\{b\}}$. We continue with $[mg^{-1},gx]=[\operatorname{id},gx]$, which concludes that $gx$ is the preimage of $[m,x]$. Hence $\eta$ is an isomorphism.

To see that $\epsilon\colon[m,y]\mapsto my$ is surjective, just consider $m=\operatorname{id}$. To see that $\epsilon$ is injective, let $[m,y],[m^{\prime},y^{\prime}]\in FU(Y)$ be two elements such that $my=m^{\prime}y^{\prime}$. Then by using Lemma 5 we find $g,g^{\prime}\in\mathsf{Pm}$ such that $gy=my=m^{\prime}y^{\prime}=g^{\prime}y^{\prime}$. This means that $y$ and $y^{\prime}$ are in the same orbit (of $U(Y)$) and have the same dimension. Case 1: $\mathsf{supp}(y)=\mathsf{supp}(y^{\prime})=\emptyset$, then $[m,y]=[\operatorname{id},y]=[\operatorname{id},y^{\prime}]=[m^{\prime},y^{\prime}]$. Case 2: $\mathsf{supp}(y)=\{a\}$ and $\mathsf{supp}(y^{\prime})=\{b\}$, then $\mathsf{supp}(gy)=\{g(a)\}$ (Lemma 2). In particular we now now that $m$ and $g$ map $a$ to $c=g(a)$, likewise $m^{\prime}$ and $g^{\prime}$ map $b$ to $c$. Now $[m,y]=[m,g^{-1}g^{\prime}y^{\prime}]=[mg^{-1}g^{\prime},y^{\prime}]=[m^{\prime},y^{\prime}]$, where we used $mg^{-1}g(b)=c=m^{\prime}(b)$ in the last step. This means that $\epsilon$ is injective and hence an isomorphism. ∎

By Proposition 2, we may consider the set $\mathbb{A}$ as both $\mathsf{Sb}$-set and $\mathsf{Pm}$-set (abusing notation). And we get an isomorphism $F(\mathbb{A})\cong\mathbb{A}$ of nominal $\mathsf{Sb}$-sets. To appreciate the above results, we give a concrete characterisation of one-dimensional nominal sets:

Lemma 6**.**

Let $X$ be a nominal $M$-set, for $M\in\{\mathsf{Sb},\mathsf{Pm}\}$. Then $\dim(X)\leq 1$ iff there exist (discrete) sets $Y$ and $I$ such that $X\cong Y+\coprod_{I}\mathbb{A}$.

In particular, the one-dimensional objects include the alphabets used for data words, consisting of a product $S\times\mathbb{A}$ of a discrete set $S$ of action labels and the set of atoms. These alphabets are very common in the study of register automata (see, e.g., [12]).

By the above and Theorem 2, $F$ maps separated powers of $\mathbb{A}$ to powers, and the set of separated words over $\mathbb{A}$ to the $\mathsf{Sb}$-set of words over $\mathbb{A}$.

Corollary 2**.**

We have $F(\mathbb{A}^{(n)})\cong\mathbb{A}^{n}$ and $F(\mathbb{A}^{(*)})\cong\mathbb{A}^{*}$.

3.2 On exponents

We have described how $F$ and $U$ interact with (separated) products. In this section, we establish a relationship between the magic wand ($\mathrel{-\kern-3.00003pt{\ast}}$) and the exponent of nominal $\mathsf{Sb}$-sets ($\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}$).

Definition 5**.**

Let $X\in{\mathsf{Pm}\text{-}\mathbf{Nom}}$ and $Y\in{\mathsf{Sb}\text{-}\mathbf{Nom}}$. We define a $\mathsf{Pm}$-equivariant map $\phi$ as follows:

[TABLE]

is defined by using the composition

[TABLE]

where $p^{-1}$ is from Theorem 2 and $\operatorname{ev}$ is the evaluation map of the exponent $\mathrel{-\kern-3.00003pt{\ast}}$. By Currying and the adjunction, we obtain $\phi$:

$F(X\mathrel{-\kern-3.00003pt{\ast}}U(Y))\times F(X)\to Y$

by Currying

$F(X\mathrel{-\kern-3.00003pt{\ast}}U(Y))\to(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)$

by Theorem 1

$\phi\colon(X\mathrel{-\kern-3.00003pt{\ast}}U(Y))\to U(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)$

With this map we can prove a generalisation of Theorem 1. In particular, the following theorem generalises the one-to-one correspondence between maps $X\to U(Y)$ and maps $F(X)\to Y$. First, it shows that this correspondence is $\mathsf{Pm}$-equivariant. Second, it extends the correspondence to all finitely supported maps and not just the equivariant ones.

Theorem 3**.**

The sets $X\mathrel{-\kern-3.00003pt{\ast}}U(Y)$ and $U(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)$ are naturally isomorphic via $\phi$ as nominal $\mathsf{Pm}$-sets.

Proof.

We define some additional maps in order to construct the inverse of $\phi$. First, from Theorem 1 we get the following isomorphism:

[TABLE]

Second, with this map and Currying, we obtain the following two natural maps:

$U(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)\times UF(X)\xrightarrow{q^{-1}}U((F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)\times F(X))\xrightarrow{U(\operatorname{ev})}U(Y)$

by Currying

$\alpha\colon U(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)\to(UF(X)\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))$

$(UF(X)\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))\times X\xrightarrow{\operatorname{id}{\times}\eta}(UF(X)\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))\times UF(X)\xrightarrow{\operatorname{ev}}U(Y)$

by Currying

$\beta\colon(UF(X)\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))\to(X\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))$

Last, we note that the inclusion $A\mathop{\ast}B\subseteq A\times B$ induces a restriction map $r\colon(B\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}C)\twoheadrightarrow(B\mathrel{-\kern-3.00003pt{\ast}}C)$ (again by Currying). A calculation shows that $r\circ\beta\circ\alpha$ is the inverse of $\phi$ (see Appendix). ∎

Note that this theorem gives an alternative characterisation of the magic wand in terms of the exponent in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$, if the codomain is $U(Y)$. Moreover, for a $1$-dimensional object $X$ in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$, we obtain the following special case of the theorem (using the co-unit isomorphism from Proposition 2):

Corollary 3**.**

Let $X,Y$ be nominal $\mathsf{Sb}$-sets. For $1$-dimensional $X$, the nominal $\mathsf{Pm}$-set $U(X)\mathrel{-\kern-3.00003pt{\ast}}U(Y)$ is naturally isomorphic to $U(X\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)$.

Remark 6*.*

The set $\mathbb{A}\mathrel{-\kern-3.00003pt{\ast}}U(X)$ coincides with the atom abstraction $[\mathbb{A}]UX$ (Remark 3). Hence, as a special case of Corollary 3, we recover [9, Theorem 34], which states a bijective correspondence between $[\mathbb{A}]UX$ and $U(\mathbb{A}\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}X)$.

4 Nominal and separated automata

In this section, we study nominal (Moore) automata, which recognise languages over infinite alphabets. After recalling the basic definitions, we introduce a new variant of automata based on the separating product, which we call separated nominal automata. These automata represent nominal languages which are $\mathsf{Sb}$-equivariant, essentially meaning they are closed under substitution. Our main result is that, if a ‘classical’ nominal automaton (over $\mathsf{Pm}$) represents a language $L$ which is $\mathsf{Sb}$-equivariant, then $L$ can also be represented by a separated nominal automaton. The latter can be exponentially smaller (in number of orbits) than the original automaton, as we show in a concrete example.

Remark 7*.*

We will work with a general output set $O$ instead of just acceptance. The reason for this is that $\mathsf{Sb}$-equivariant functions $L\colon\mathbb{A}\to 2$ are not very interesting: they are defined purely by the length of the input. By using more general output $O$, we may still capture interesting behaviour, e.g., the language in Example 3.

Definition 6**.**

Let $\Sigma,O$ be $\mathsf{Pm}$-sets, called input/output alphabet respectively.

• •

A ($\mathsf{Pm}$)-nominal language is an equivariant map of the form $L\colon\Sigma^{*}\to O$.

• •

A nominal (Moore) automaton $\mathcal{A}=(Q,\delta,o,q_{0})$ consists of a nominal set of states $Q$, an equivariant transition function $\delta\colon Q\times\Sigma\to Q$, an equivariant output function $o\colon Q\rightarrow O$, and an initial state $q_{0}\in Q$ with an empty support.

• •

The language semantics is the map $l\colon Q\times\Sigma^{*}\to O$, defined inductively by

[TABLE]

for all $x\in Q$, $a\in\Sigma$ and $w\in\Sigma^{*}$.

• •

For $l^{\flat}\colon Q\to(\Sigma^{*}\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}O)$ the transpose of $l$, we have that $l^{\flat}(q_{0})\colon\Sigma^{*}\to O$ is equivariant; this is called the language accepted by $\mathcal{A}$.

Note that the language accepted by an automaton can equivalently be characterised by considering paths through the automaton from the initial state.

If the state space $Q$ and the alphabets $\Sigma,O$ are orbit finite, this allows us to run algorithms (reachability, minimization, etc.) on such automata [3], but there is no need to assume this for now. For an automaton $\mathcal{A}=(Q,\delta,o,q_{0})$, we define the set of reachable states as the least set $R(\mathcal{A})\subseteq Q$ such that $q_{0}\in R(\mathcal{A})$ and for all $x\in R(\mathcal{A})$ and $a\in\Sigma$, $\delta(x,a)\in R(\mathcal{A})$.

Example 3*.*

We model a bounded FIFO queue of size $n$ as a nominal Moore automaton, explicitly handling the data in the automaton structure.333We use a reactive version of the queue data structure which is slightly different from the versions in [17, 12]. The input alphabet $\Sigma$ and output alphabet $O$ are as follows:

[TABLE]

The input alphabet encodes two actions: putting a new value on the queue and popping a value. The output is either a value (the front of the queue) or $\perp$ if the queue is empty. A queue of size $n$ is modelled by the automaton $(Q,\delta,o,q_{0})$ defined as follows.

[TABLE]

[TABLE]

The automaton is depicted in Figure 1 for the case $n=3$. The language accepted by this automaton assigns to a word $w$ the first element of the queue after executing the instructions in $w$ from left to right, and $\perp$ if the input is ill-behaved, i.e., Pop is applied to an empty queue or $\mathop{\text{\sf Put}}(a)$ to a full queue.

Definition 7**.**

Let $\Sigma,O$ be $\mathsf{Pm}$-sets. A separated language is an equivariant map of the form $\Sigma^{(*)}\to O$. A separated automaton $\mathcal{A}=(Q,\delta,o,q_{0})$ consists of $Q$, $o$ and $q_{0}$ defined as in a nominal automaton, and an equivariant transition function $\delta\colon Q\mathop{\ast}\Sigma\rightarrow Q$.

The separated language semantics of such an automaton is given by the map $s\colon Q\mathop{\ast}\Sigma^{(*)}\to O$, defined by

[TABLE]

for all $x\in Q$, $a\in\Sigma$ and $w\in\Sigma^{(*)}$ such that $x\mathop{\#}aw$ and $a\mathop{\#}w$.

Let $s^{\flat}\colon Q\to(\Sigma^{(*)}\mathrel{-\kern-3.00003pt{\ast}}O)$ be the transpose of $s$. Then $s^{\flat}(q_{0})\colon\Sigma^{(*)}\to O$ corresponds to a separated language, this is called the separated language accepted by $\mathcal{A}$.

By definition of the separated product, the transition function is only defined on a state $x$ and letter $a\in\Sigma$ if $x\mathop{\#}a$. In Example 4 below, we describe the bounded FIFO as a separated automaton, and describe its accepted language.

First, we show how the language semantics of separated nominal automata extends to a language over all words, provided that both the input alphabet $\Sigma$ and the output alphabet $O$ are $\mathsf{Sb}$-sets.

Definition 8**.**

Let $\Sigma$ and $O$ be nominal $\mathsf{Sb}$-sets. An $\mathsf{Sb}$-equivariant function $L\colon\Sigma^{*}\to O$ is called an $\mathsf{Sb}$-language.

Notice the difference between an $\mathsf{Sb}$-language $L\colon\Sigma^{*}\to O$ and a $\mathsf{Pm}$-language $L^{\prime}\colon(U\Sigma)^{*}\to U(O)$. They are both functions from $\Sigma^{*}$ to $O$, but the latter is only $\mathsf{Pm}$-equivariant, while the former satisfies the stronger property of $\mathsf{Sb}$-equivariance. Languages over separated words, and $\mathsf{Sb}$-languages, are connected as follows.

Proposition 3**.**

Suppose $\Sigma,O$ are both nominal $\mathsf{Sb}$-sets, and suppose $\dim(\Sigma)\leq 1$. There is a one-to-one correspondence

[TABLE]

between separated languages and $\mathsf{Sb}$-nominal languages. From $\overline{S}$ to $S$, this is given by application of the forgetful functor and restricting to the subset of separated words.

For the converse direction, given $w=a_{1}\ldots a_{n}\in\Sigma^{*}$, let $b_{1},\ldots,b_{n}\in\Sigma$ such that $w\mathop{\#}b_{i}$ for all $i$, and $b_{i}\mathop{\#}b_{j}$ for all $i,j$ with $i\neq j$. Define $m\in\mathsf{Sb}$ by

[TABLE]

Then $\overline{S}(a_{1}a_{2}a_{3}\cdots a_{n})=m\cdot S(b_{1}b_{2}b_{3}\cdots b_{n})$.

Proof.

There is the following chain of one-to-one correspondences, from the results of the previous section:

$(U\Sigma)^{(*)}\rightarrow UO$

by Theorem 1

$F(U\Sigma)^{(*)}\rightarrow O$

by Corollary 1

$(FU\Sigma)^{*}\rightarrow O$

by Proposition 2

$\Sigma^{*}\rightarrow O$

∎

Thus, every separated automaton over $U(\Sigma),U(O)$ gives rise to an $\mathsf{Sb}$-language $\overline{S}$, corresponding to the language $S$ accepted by the automaton.

Any nominal automaton $\mathcal{A}$ restricts to a separated automaton, formally described in Definition 9. It turns out that if the $(\mathsf{Pm})$-language accepted by $\mathcal{A}$ is actually an $\mathsf{Sb}$-language, then the restricted automaton already represents this language, as the extension $\overline{S}$ of the associated separated language $S$ (Proposition 4). Hence, in such a case, the restricted separated automaton suffices to describe the language of $\mathcal{A}$.

Definition 9**.**

Let $i\colon Q\mathop{\ast}U(\Sigma)\hookrightarrow Q\times U(\Sigma)$ be the natural inclusion map. A nominal automaton $\mathcal{A}=(Q,\delta,o,q_{0})$ induces a separated automaton $\mathcal{A}_{*}$, by setting $\mathcal{A}_{*}=(Q,\delta\circ i,o,q_{0})$.

Proposition 4**.**

Suppose $\Sigma,O$ are both $\mathsf{Sb}$-sets, and suppose $\dim(\Sigma)\leq 1$. Let $L\colon(U\Sigma)^{*}\to UO$ be the $\mathsf{Pm}$-nominal language accepted by a nominal automaton $\mathcal{A}$, and suppose $L$ is $\mathsf{Sb}$-equivariant. Let $S$ be the separated language accepted by $\mathcal{A}_{*}$. Then $L=U(\overline{S})$.

Proof.

It follows from the one-to-one correspondence in Proposition 3: on the bottom there are two languages ($L$ and $U(\overline{S})$), while there is only the restriction of $L$ on the top. We conclude that $L=U(\overline{S})$. ∎

As we will see in Example 4, separated automata allow us to represent $\mathsf{Sb}$-languages in a much smaller way than nominal automata. Given a nominal automaton $\mathcal{A}$, a smaller separated automaton can be obtained by computing the reachable part of the restriction $\mathcal{A}_{*}$. The reachable part is defined similarly (but only where $\delta$ is defined) and denoted by $R(\mathcal{A}_{*})$ as well.

Lemma 7**.**

For any nominal automaton $\mathcal{A}$, we have $R(\mathcal{A}_{*})\subseteq R(\mathcal{A})$.

The converse inclusion of the above proposition does certainly not hold, as shown by the following example.

Example 4*.*

Let $\mathcal{A}$ be the automaton modelling a bounded FIFO queue (for some $n$), from Example 3. The $\mathsf{Pm}$-nominal language $L$ accepted by $\mathcal{A}$ is $\mathsf{Sb}$-equivariant: it is closed under application of arbitrary substitutions.

The separated automaton $\mathcal{A}_{*}$ is given simply by restricting the transition function to $Q\mathop{\ast}\Sigma$, i.e., a $\mathop{\text{\sf Put}}(a)$-transition from a state $w\in Q$ exists only if $a$ does not occur in $w$. The separated language $S$ accepted by this new automaton is the restriction of the nominal language of $\mathcal{A}$ to separated words. By Proposition 4, we have $L=U(\overline{S})$. Hence, the separated automaton $\mathcal{A}_{*}$ represents $L$, essentially by closing the associated separated language $S$ under all substitutions.

The reachable part of $\mathcal{A}_{*}$ is given by

[TABLE]

Clearly, restricting $\mathcal{A}_{*}$ to the reachable part does not affect the accepted language. However, while the orginal state space $Q$ has exponentially many orbits in $n$, $R_{\mathcal{A}_{*}}$ has only $n+1$ orbits! Thus, taking the reachable part of $R_{\mathcal{A}_{*}}$ yields a separated automaton which represents the FIFO language $L$ in a much smaller way than the original automaton.

4.1 Separated automata: coalgebraic perspective

Nominal automata and separated automata can be presented as coalgebras on the category of $\mathsf{Pm}$-nominal sets. In this section we revisit the above results from this perspective, and generalise from (equivariant) languages to finitely supported languages. In particular, we retrieve the extension from separated languages to $\mathsf{Sb}$-languages, by establishing $\mathsf{Sb}$-languages as a final separated automaton. The latter result follows by instantiating a well-known technique for lifting adjunctions to categories of coalgebras, using the results of Section 3. In the remainder of this section we assume familiarity with the theory of coalgebras, see, e.g., [13, 22].

Definition 10**.**

Let $M$ be a submonoid of $\mathsf{Sb}$, and let $\Sigma$, $O$ be nominal $M$-sets, referred to as the input and output alphabet respectively. We define the functor $B_{M}\colon{M\text{-}\mathbf{Nom}}\to{M\text{-}\mathbf{Nom}}$ by $B_{M}(X)=O\times(\Sigma\mathrel{\to_{\text{fs}}^{M}}X)$. An ($M$)-nominal (Moore) automaton is a $B_{M}$-coalgebra.

A $B_{M}$-coalgebra can be presented as a nominal set $Q$ together with the pairing

[TABLE]

of an equivariant output function $o\colon Q\to O$, and (the transpose of) an equivariant transition function $\delta\colon Q\times\Sigma\to Q$. In case $M=\mathsf{Pm}$, this coincides with the automata of Definition 6, omitting initial states. The language semantics is generalised accordingly, as follows. Given such a $B_{M}$-coalgebra $(Q,\langle o,\delta^{\flat}\rangle)$, the language semantics $l\colon Q\times\Sigma^{*}\to O$ is given by

[TABLE]

for all $x\in S$, $a\in\Sigma$ and $w\in\Sigma^{*}$.

Proposition 5**.**

Let $M$ be a submonoid of $\mathsf{Sb}$, let $\Sigma$, $O$ be nominal $M$-sets. The nominal $M$-set $\Sigma^{*}\mathrel{\to_{\text{fs}}^{M}}O$ extends to a final $B_{M}$-coalgebra $(\Sigma^{*}\mathrel{\to_{\text{fs}}^{M}}O,\zeta)$, such that the unique homomorphism from a given $B_{M}$-coalgebra is the transpose $l^{\flat}$ of the language semantics (4).

A separated automaton (Definition 7, without initial states) corresponds to a coalgebra for the functor $B_{*}\colon{\mathsf{Pm}\text{-}\mathbf{Nom}}\to{\mathsf{Pm}\text{-}\mathbf{Nom}}$ given by $B_{*}(X)=O\times(\Sigma\mathrel{-\kern-3.00003pt{\ast}}X)$. The separated language semantics arises by finality.

Proposition 6**.**

The set $\Sigma^{(\ast)}\mathrel{-\kern-3.00003pt{\ast}}O$ is the carrier of a final $B_{*}$-coalgebra, such that the unique coalgebra homomorphism from a given $B_{*}$-coalgebra $(Q,\langle o,\delta\rangle)$ is the transpose $s^{\flat}\!$ of the separated language semantics $s\colon Q\mathop{\ast}\Sigma^{(\ast)}\to O$ (Definition 7).

Next, we provide an alternative description of the final $B_{*}$-coalgebra which assigns $\mathsf{Sb}$-nominal languages to states of separated nominal automata. The essence is to obtain a final $B_{*}$-coalgebra from the final $B_{\mathsf{Sb}}$-coalgebra. In order to prove this, we use a technique to lift adjunctions to categories of coalgebras. This technique occurs regularly in the coalgebraic study of automata [14, 16, 15].

Theorem 4**.**

Let $\Sigma$ be a $\mathsf{Pm}$-set, and $O$ an $\mathsf{Sb}$-set. Define $B_{*}$ and $B_{\mathsf{Sb}}$ accordingly, as $B_{*}(X)=UO\times(\Sigma\mathrel{-\kern-3.00003pt{\ast}}X)$ and $B_{\mathsf{Sb}}(X)=O\times(F\Sigma\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}X)$. There is an adjunction $\overline{F}\dashv\overline{U}$ in:

[TABLE]

where $\overline{F}$ and $\overline{U}$ coincide with $F$ and $U$ respectively on carriers.

Proof.

There is a natural isomorphism $\lambda\colon B_{*}U\Rightarrow UB_{\mathsf{Sb}}$ given by

[TABLE]

where $\phi$ is the isomorphism from Theorem 3 and the isomorphism on the right comes from $U$ being a right adjoint. The result now follows from Theorem 2.14 in [11]. In particular, $\overline{U}(X,\gamma)=(UX,\lambda^{-1}\circ U(\gamma))$. ∎

Since right adjoints preserve limits, and final objects in particular, we obtain the following, giving semantics of separated automata through finality.

Corollary 4**.**

Let $((F\Sigma)^{*}\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}O,\zeta)$ be the final $B_{\mathsf{Sb}}$-coalgebra (Proposition 5). Then the $B_{*}$-coalgebra $\overline{U}(\Sigma^{*}\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}O,\zeta)$ is final and carried by the set $(F\Sigma)^{*}\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}O$ of $\mathsf{Sb}$-nominal languages.

5 Related and future work

Fiore and Turi described a similar adjunction between certain presheaf categories [6]. However, Staton describes in his thesis that the usage of presheaves allows for many degenerate models and one should look at sheaves instead [26]. The category of sheaves is equivalent to the category of nominal sets. Staton transfers the adjunction of Fiore and Turi to the sheaf categories. We conjecture that the adjunction presented in this paper is equivalent, but defined in more elementary means. The monoidal property of $F$, which is crucial for our application in automata, has not been discussed before.

An interesting line of research is the generalisation to other symmetries by Bojańczyk et al. [3]. In particular, the total order symmetry is relevant, since it allows one to compare elements on their order, as often used in data words. In this case the symmetries are given by the group of all monotone bijections. Many results of nominal sets generalise to this symmetry. For monotone substitutions, however, the situation seems more subtle. For example, we note that a substitution which maps two values to the same value actually maps all the values in between to that value. Whether the adjunction from Theorem 1 generalises to other symmetries is left as future work.

This research was motivated by learning nominal automata. If we know a nominal automaton recognises an $\mathsf{Sb}$-language, then we are better off learning a separated automaton directly. From the $\mathsf{Sb}$-semantics of separated automata, it follows that we have a Myhill-Nerode theorem, which means that learning is feasible. We expect that this can be useful, since we can achieve an exponential reduction this way.

Bojańczyk et al. prove that nominal automata are equivalent to register automata in terms of expressiveness [3]. However, when translating from register automata with $n$ states to nominal automata, we may get exponentially many orbits. This happens for instance in the FIFO automaton (Example 3). We have shown that the exponential blow-up is avoidable by using separated automata, for this example and in general for $\mathsf{Sb}$-equivariant languages. Such languages come from register automata which manipulate data but where do control flow does not depend on comparisons. This typically occurs in data structures.

An important open problem is whether the latter requirement can be relaxed, by adding separated transitions only locally in a nominal automaton. A possible step in this direction is to consider the monad $T=UF$ on ${\mathsf{Pm}\text{-}\mathbf{Nom}}$ and incorporate it in the automaton model. We believe that this is the hypothesised “substitution monad” from [17]. The monad is monoidal (sending separated products to Cartesian products) and if $X$ is an orbit-finite nominal set, then so is $T(X)$. This means that we can consider nominal $T$-automata and we can perhaps determinise them using coalgebraic methods [24].

Acknowledgements

We would like to thank Gerco van Heerdt and Tom Hirschowitz for their useful comments.

Appendix A Omitted Proofs

Lemma 8**.**

(Lemma 1) Let $X$ be a nominal $\mathsf{Sb}$-set and $x\in X$. Then a set $C$ supports $x$ w.r.t. the $\mathsf{Sb}$-action if and only if $C$ supports $x$ w.r.t. the (induced) $\mathsf{Pm}$-action.

Proof.

(Slightly different proof from the one in [8].) First note that one direction is easy: an $\mathsf{Sb}$-support is also a $\mathsf{Pm}$-support.

For the other direction, let $C$ be a $\mathsf{Pm}$-support of $x\in X$. Now let $C^{\prime}$ be a $\mathsf{Sb}$-support of $x$ (note that $X$ is a nominal $\mathsf{Sb}$-set). Assume $m,m^{\prime}$ such that $m|_{C}=m^{\prime}|_{C}$ and take a $g$ such that $g|_{C}=\operatorname{id}|_{C}$ and $g(c^{\prime})\in\ker(m,m^{\prime})$ for all $c^{\prime}\in C^{\prime}\setminus C$. This is possible, since $C^{\prime}\setminus C$ is a finite set, and there are only finitely many values where $m$ and $m^{\prime}$ disagree ($\mathsf{Sb}$ consists of finite substitutions). Now $mg|_{C^{\prime}}=m^{\prime}g|_{C^{\prime}}$, so $mgx=m^{\prime}gx$ (remember that $C^{\prime}$ is an $\mathsf{Sb}$-support). Using that $C$ is a $\mathsf{Pm}$-support we know that $gx=x$ and so $mgx=m^{\prime}gx\implies mx=m^{\prime}x$. This concludes that $C$ is a $\mathsf{Sb}$-support. ∎

Lemma 9**.**

(Lemma 4) We have $(m_{1},x_{1})\sim(m_{2},x_{2})$ iff there is a $g\in\mathsf{Pm}$ such that $gx_{1}=x_{2}$ and $m_{1}|_{C}=m_{2}g|_{C}$, for $C$ some $\mathsf{Pm}$-support of $x_{1}$.

Proof.

Let us define $(m_{1},x_{1})\sim^{\prime}(m_{2},x_{2})$ if there exists a permutation $g\in\mathsf{Pm}$ such that $gx_{1}=x_{2}$ and $m_{1}|_{C}=m_{2}g|_{C}$, for $C$ some $\mathsf{Pm}$-support of $x_{1}$. We need to prove ${\sim}={\sim^{\prime}}$.

(${\sim^{\prime}}\subseteq{\sim}$) Let $(m_{1},x_{1})\sim^{\prime}(m_{2},x_{2})$, then there is a $g$ with the required properties. Now check $(m_{2},x_{2})=(m_{2},gx_{1})\sim(m_{2}g,x_{1})\sim(m_{1},x_{1})$.

(${\sim}\subseteq{\sim^{\prime}}$) For this direction, we show that $\sim^{\prime}$ is an equivalence relation which contains relations (2) and (3). Proving reflexivity and symmetry is trivial. For transitivity, assume $(m_{1},x_{1})\sim^{\prime}(m_{2},x_{2})$ and $(m_{2},x_{2})\sim^{\prime}(m_{3},x_{3})$. There are $g,h$ with $gx_{1}=x_{2}$ and $hx_{2}=x_{3}$. Note that $hgx_{1}=x_{3}$. Moreover, we have $m_{1}|_{\mathsf{supp}(x_{1})}=m_{2}g|_{\mathsf{supp}(x_{1})}$ and $m_{2}|_{\mathsf{supp}(x_{2})}=m_{3}h|_{\mathsf{supp}(x_{2})}$. Observe that $\mathsf{supp}(x_{2})=g\mathsf{supp}(x_{1})$ so that $m_{2}|_{g\mathsf{supp}(x_{1})}=m_{3}h|_{g\mathsf{supp}(x_{1})}$. Now it follows that $m_{1}|_{\mathsf{supp}(x_{1})}=m_{2}g|_{\mathsf{supp}(x_{1})}=m_{2}hg|_{\mathsf{supp}(x_{1})}$. This proves $(m_{1},x_{1})\sim^{\prime}(m_{3},x_{3})$ as required. To see that relation 2 is included, we take the $g$ from the relation and check the requirements. To see that relation 3 is included, we simply take $g=\operatorname{id}$ and the requirement on supports follow by assumption. ∎

Theorem 5**.**

(Theorem 1) The functor $F$ is left adjoint to $U$:

[TABLE]

Proof.

(Remainder of proof: equivariance and uniqueness) For the $\mathsf{Sb}$-equivariance, we compute $n\cdot f^{\sharp}([m,x])=nm\cdot f(x)=f^{\sharp}([nm,x])=f^{\sharp}(n[m,x])$.

Finally, for uniqueness, suppose $h\colon FX\rightarrow Y$ is such that $U(h)\circ\eta_{X}=f$, i.e., $h([\operatorname{id},x])=f(x)$. Then $h([m,x])=h(m[\operatorname{id},x])=m\cdot h([\operatorname{id},x])=m\cdot f(x)=m\cdot f^{\sharp}([\operatorname{id},x])=f^{\sharp}(m\cdot[\operatorname{id},x])=f^{\sharp}([m,x])$ as desired. ∎

Lemma 10**.**

If a map in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ is both injective and surjective, then it is an isomorphism of nominal $\mathsf{Sb}$-sets.

Proof.

Let $f\colon X\to Y$ be an injective, surjective map between nominal $\mathsf{Sb}$-sets. Since $f$ is surjective, it is epic, and since it is injective, it is monic. Every map which is epic and monic is an isomorphism in ${\mathsf{Sb}\text{-}\mathbf{Set}}$, because it is a topos. Since ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ is a full subcategory of ${\mathsf{Sb}\text{-}\mathbf{Set}}$, we conclude that $f$ is an isomorphism of nominal $\mathsf{Sb}$-sets. (Alternatively, we can use the fact that ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ is a topos [9].) ∎

Theorem 6**.**

(Theorem 3) The sets $X\mathrel{-\kern-3.00003pt{\ast}}U(Y)$ and $U(F(X)\mathrel{\to_{\text{fs}}}Y)$ are naturally isomorphic via $\phi$ as nominal $\mathsf{Pm}$-sets.

Proof.

(Remainder of the proof: calculations of composition) We prove that $r\circ\beta\circ\alpha$ is the inverse of $\phi$.444We use $r_{X,U(Y)}\colon(X\mathrel{\to_{\text{fs}}^{\mathsf{Pm}}}U(Y))\twoheadrightarrow(X\mathrel{-\kern-3.00003pt{\ast}}U(Y))$ here. The easiest way to see this is to evaluate $(r\circ\beta\circ\alpha\circ\phi)^{\sharp}$ on a separated pair $(\psi,x)$ and see that this equals $\operatorname{id}^{\sharp}(\psi,x)$. (The $\sharp$ denotes (un)currying or transposition.) Most steps involve spelling out the definitions. We comment only on the interesting steps.

Let $(\psi,x)\in(X\mathrel{-\kern-3.00003pt{\ast}}U(Y))\mathop{\ast}X$ and calculate:

[TABLE]

So $(r\circ\beta\circ\alpha\circ\phi)^{\sharp}=\operatorname{ev}=\operatorname{id}^{\sharp}$. Hence $r\circ\beta\circ\alpha\circ\phi=\operatorname{id}$. There are few steps which require attention. Ad 1: Recall that the exponent in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ consists of two-variable functions and that $\operatorname{ev}(\psi,y)=\psi(\operatorname{id},y)$. Ad 2: Currying in ${\mathsf{Sb}\text{-}\mathbf{Nom}}$ is defined by $g_{\flat}c(s,a)=g(s\cdot c,a)$. Ad 3: Note that $\psi\mathop{\#}x$, and so to compute $p^{-1}$ we do not have to rename things to be fresh.

Similarly, we prove that the composition $\phi\circ r\circ\beta\circ\alpha=\operatorname{id}$, by considering its (twice) transpose. Let $(\psi,x)\in FU(F(X)\mathrel{\to_{\text{fs}}^{\mathsf{Sb}}}Y)\times F(X)$ and note that $\psi=[m,\psi_{0}],x=[n,x_{0}]$. Now calculate:

[TABLE]

We conclude that $(\phi\circ r\circ\beta\circ\alpha)^{\sharp\sharp}={\operatorname{ev}}\circ\epsilon\times\operatorname{id}=\operatorname{id}^{\sharp\sharp}$ and so $\phi\circ r\circ\beta\circ\alpha=\operatorname{id}$. Ad 1 (twice): To apply $p^{-1}$, we choose a fresh $x_{0}^{\prime}$ and define $m^{\prime}$ such that $[m,\psi_{0}]=[m^{\prime},\psi_{0}]$ and $[n,x_{0}]=[m^{\prime},x_{0}^{\prime}]$. Ad 2: Note that $x_{0}\mathop{\#}\psi_{0}$ (and so $x_{0}\mathop{\#}\beta(\alpha(\psi_{0}))$), so we are allowed to restrict with $r$. Ad 3: Here we use that $\psi_{0}$ is a (two-variable) $\mathsf{Sb}$-equivariant map.

This concludes that $r\circ\beta\circ\alpha=\phi^{-1}$. ∎