\project thesis
\startcomponent separated-nominal-automata

\startchapter
  [title={Separated Nominal Automata},
   reference=chap:separated-nominal-automata]

\midaligned{~
\author[width=0.5\hsize]{Joshua Moerman \\ Radboud University}
\author[width=0.5\hsize]{Jurriaan Rot \\ Radboud University}
}

\startabstract
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 \emph{nominal renaming sets}, which involve arbitrary substitutions rather than permutations, through a categorical adjunction.
In particular, the separated product of nominal sets is related to the Cartesian product of nominal renaming sets.
Based on these results, we define the new notion of \emph{separated nominal automata}.
These efficiently recognise nominal languages, provided these languages are renaming sets.
In such cases, moving from the existing notion of nominal automata to separated automata can lead to an exponential reduction of the state space.
\stopabstract

\vfill\noindent
This chapter is based on the following submission:

\noindent\cite[entry][MoermanR19]
\page

\noindent
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 by \citet[GabbayP99], they
have been widely used for implementing and reasoning over syntax with binders (see the book of \citenp[Pitts13]).
Further, nominal techniques have been related to computability theory \citep[BojanczykKLT13] and automata theory \citep[BojanczykKL14],
where they provide an elegant means of studying languages over infinite alphabets.
This embeds nominal techniques in a broader setting of \emph{symmetry aware computation} \citep[Pitts16].

Gabbay, one of the pioneers of nominal techniques described a variation on the theme: \emph{nominal renaming sets} \citep[Gabbay07, GabbayH08].
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, the motivation for using nominal renaming sets comes from automata theory over infinite alphabets.
Certain languages form nominal renaming sets, which means that they are closed under all possible substitutions on atoms.
In order to obtain efficient automata-theoretic representations of such languages, we systematically relate nominal renaming sets to nominal sets.

We start by establishing a categorical adjunction in \in{Section}[sec:adjunction]:
\placefigure[force, none]{}{
\hbox{\starttikzpicture[bend angle=15]
\node              (0) {$\permnom$};
\node [right of=0] (p) {$\perp$};
\node [right of=p] (1) {$\sbnom$};
\path[->]
(0) edge [bend left] node [above] {$F$} (1)
(1) edge [bend left] node [below] {$U$} (0);
\stoptikzpicture}}
where $\permnom$ is the usual category of nominal sets and $\sbnom$ 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 $\atoms^{(*)}$ of all words consisting of distinct atoms to the nominal renaming set $\atoms^*$ consisting of all words over the atoms.

In fact, the latter follows from one of the main results of this paper:
$F$ maps the \emph{separated product} $X \sepprod Y$ of nominal sets to the Cartesian product of nominal renaming sets.
Additionally, under certain conditions, $U$ maps the exponent to the \emph{magic wand} $X \wandto 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 \citep[Pitts13], and has also been studied in the setting of presheaf categories, aimed towards separation logic \citep[OHearn03].

We apply these connections between nominal sets and renaming sets in the context of automata theory.
Nominal automata are an elegant model for recognising languages over infinite alphabets.
They are expressively equivalent to the more classical register automata (\citenp[Bojanczyk18], Theorem 6.5),
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.
\footnote{Here \quote{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 = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \}$, and the output alphabet by $O = \atoms \cup \{ \Null \}$.
The 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 $\Null$ if this is undefined.
The language $L_n$ can be recognised by a nominal 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.

Based on the observation that $L_n$ is a nominal renaming set, we can come up with a \emph{linear} automata-theoretic representation.
To this end, we define the new notion of \emph{separated nominal automaton}, where the transition function is only defined for pairs of states and letters with a disjoint support (\in{Section}[sec:automata]).
Using the aforementioned categorical framework, we find that such separated automata recognise languages which are nominal renaming sets.
Separated nominal automata can be much smaller than classical nominal automata recognising the same language.
In particular, in the FIFO example, the reachable part of the separated automaton obtained from the original nominal automaton has $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 (\in{Chapter}[chap:learning-nominal-automata]).

In summary, the main contributions of this paper are the adjunction between nominal sets and nominal renaming sets, the relation between separated product and the Cartesian product of renaming sets, and the application to automata theory.
We conclude with a coalgebraic account of separated automata in \in{Section}[sec:sep-aut].
In particular, we justify the semantics of separated automata by showing how it arises through a final coalgebra, obtained by lifting the adjunction to categories of coalgebras.
The last section is orthogonal to the other results, and background knowledge of coalgebra is needed only there.


\startsection
  [title={Monoid actions and nominal sets}]

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

\startdefinition
Let $(M, \cdot, 1)$ be a monoid.
An \emph{$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 \emph{$M$-action} and $m \cdot x$ is often written by juxtaposition $m x$.
A function $f \colon X \to Y$ between two $M$-sets is \emph{$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 $\MSet$.
\stopdefinition

Let $\atoms = \{a, b, c, \ldots\}$ be a countable infinite set of \emph{atoms}.
The two main instances of $M$ considered in this paper are the monoid
\startformula
\sb = \{ m \colon \atoms \to \atoms \mid m(a) \neq a \text{ for finitely many }a \}
\stopformula
of all (finite) substitutions (with composition as multiplication), and the monoid
\startformula
\perm = \{ g \in \sb \mid g \text{ is a bijection} \}
\stopformula
of all (finite) permutations.
Since $\perm$ is a submonoid of $\sb$, any $\sb$-set is also a $\perm$-set; and any $\sb$-equivariant map is also $\perm$-equivariant.
This gives rise to a forgetful functor
\startformula
U \colon \sbset \to \permset .
\stopformula

The set $\atoms$ is an $\sb$-set by defining $m \cdot a = m(a)$.
Given an $M$-set $X$, the set $\pow(X)$ of subsets of $X$ is an $M$-set, with the action defined by direct image.

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

For any monoid $M$, the category $\MSet$ 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 $\MSet$, the exponent $X \to^{M} Y$ is given by the set
$\{f \colon M \times X \to Y \mid f \text{ is equivariant}\}$.
\footnote{If 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 \citet[Simmons].
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)$.


\startsubsection
  [title={Nominal $M$-sets}]

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

\startdefinition
Let $X$ be an $M$-set, and $x \in X$ an element.
A set $C \subset \atoms$ is an \emph{($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 \emph{nominal} if every element $x$ has a finite $M$-support.
\stopdefinition

Nominal $M$-sets and equivariant maps form a full subcategory of $\MSet$, denoted by $\MNom$.
The $M$-set $\atoms$ of atoms is nominal.
The powerset $\pow(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 = \id|_C$.
Second, the statement $x g_1 = x g_2$ can be expressed as $x g_1 g_2^{-1} = x$.
Hence, $C$ is a support iff $g|_C = \id_C$ implies $gx = x$ for all $g$, which is the standard definition for nominal sets over a group \citep[Pitts13].
Surprisingly, \citet[GabbayH08] show a similar characterisation also holds for $\sb$-sets.
Moreover, recall that every $\sb$-set is also a $\perm$-set; the associated notions of support coincide on nominal $\sb$-sets, as shown by the following result.
In particular, this means that the forgetful functor restricts to $U \colon \sbnom \to \permnom$.

\startlemma[reference=lem:GM-support]
(Theorem 4.8 from \citenp[Gabbay07])
Let $X$ be a nominal $\sb$-set, $x \in X$, and $C \subset \atoms$.
Then $C$ is an $\sb$-support of $x$ iff it is a $\perm$-support of $x$.
\stoplemma

\startremark
It is not true that any $\perm$-support is an $\sb$-support.
The condition that $X$ is nominal, in the above lemma, is crucial.
Let $X = \atoms + 1$ and define the following $\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 $\sb$-set, but is \emph{not nominal}.
Now consider $U(X)$, this is the $\perm$-set $\atoms + 1$ with the natural action, which is a \emph{nominal} $\perm$-set!
In particular, as a $\perm$-set each element has a finite support, but as a $\sb$-set the supports are infinite.

This counterexample is similar to the \quotation{exploding nominal sets} of \citet[Gabbay07], but even worse behaved.
We like to call them \emph{nuclear sets}, since an element will collapse when hit by a non-injective map, no matter how far away the non-injectivity occurs.
\stopremark

For $M \in \{\sb, \perm\}$, 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 $\supp(x)$.
Note that by \in{Lemma}[lem:GM-support], the set $\supp(x)$ is independent of whether a nominal $\sb$-set $X$ is viewed as an $\sb$-set or a $\perm$-set.
The \emph{dimension} of $X$ is given by $\dim(X) = \max \{|\supp(x)| \,\mid\, x \in X \}$, where $|\supp(x)|$ is the cardinality of $\supp(x)$.

We list some basic properties of nominal $M$-sets, which have
known counterparts for the case that $M$ is a group \citep[BojanczykKL14],
and when $M=\sb$ \citep[GabbayH08].

\startlemma[reference=lem:transfer-support]
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 \perm$ preserves least supports: $g \cdot \supp(x) = \supp(g x)$.
\stoplemma

The latter equality does not hold in general for a monoid $M$.
For instance, the exploding nominal renaming sets by \citet[GabbayH08] give counterexamples for $M = \sb$.

\startlemma
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)$.
\stoplemma

The category $\MNom$ is symmetric monoidal closed, with the product inherited from $\MSet$, thus simply given by Cartesian product.
The exponent is given by the restriction of the exponent $X \to^{M} Y$ in $\MSet$ to the set of finitely supported functions, denoted by $X \mto Y$.
This is similar to the exponents of nominal sets with 01-substitutions from \citet[Pitts14].

\startremark
\citet[GabbayH08] give a different presentation of the exponent in $\MNom$, 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 $\MSet$.
\stopremark


\stopsubsection
\startsubsection
  [title={Separated product}]

\startdefinition
Two elements $x, y \in X$ of a $\perm$-nominal set are called \emph{separated}, denoted by $x \separated y$, if there are disjoint sets $C_1, C_2 \subset \atoms$ such that $C_1$ supports $x$ and $C_2$ supports $y$.
The \emph{separated product} of $\perm$-nominal sets $X$ and $Y$ is defined as
\startformula
X \sepprod Y = \{ (x, y) \mid x \separated y \}.
\stopformula
\stopdefinition

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

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

The separated product gives rise to another symmetric closed monoidal structure on $\permnom$, with $1$ as unit, and the exponential object given by \emph{magic wand} $X \wandto Y$.
An explicit characterisation of $X \wandto Y$ is not needed in the remainder of this chapter, but for a complete presentation we briefly recall the description from \citet[Clouston13] (see also the book of \citenp[Pitts13]).
First, define a $\perm$-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 \emph{separating} if $f$ is finitely supported, $f(x)$ is defined iff $f \separated x$, and $\supp(f) = \bigcup_{x \in \dom(f)} \supp(f(x)) \setminus \supp(x)$.
Finally, $X \wandto Y = \{f \colon X \rightharpoonup Y \mid f \text{ is separating}\}$.
See \citet[Clouston13] for a proof and explanation.

\startremark[reference=rem:atom-abstr]
The special case $\atoms \wandto Y$ coincides with $[\atoms]Y$, the set of \emph{name abstractions} \citep[Pitts13].
The latter is generalised to $[X]Y$ by \citet[Clouston13], but it is shown there that the coincidence $[X]Y \cong (X \wandto Y)$ only holds under strong assumptions (including that $X$ is single-orbit).
\stopremark

\startremark
An analogue of the separated product does not seem to exist for nominal $\sb$-sets.
For instance, consider the set $\atoms \times \atoms$.
As a $\perm$-set, it has four equivariant subsets: $\emptyset, \Delta(\atoms) = \{(a,a) \mid a \in \atoms\}$, $\atoms \sepprod \atoms$, and $\atoms \times \atoms$.
However, the set $\atoms \sepprod \atoms$ is not an equivariant subset when considering $\atoms \times \atoms$ as an $\sb$-set.
\stopremark


\stopsubsection
\stopsection
\startsection
  [title={A monoidal construction from $\perm$-sets to $\sb$-sets},
   reference=sec:adjunction]

In this section, we provide a free construction, extending nominal $\perm$-sets to nominal $\sb$-sets.
We use this as a basis to relate the separated product and exponent (in $\permnom$) to the product and exponent in $\sbnom$.
The main results are:
\startitemize[after]
\item
the forgetful functor $U \colon \sbnom \to \permnom$ has a left adjoint $F$ (\in{Theorem}[thm:adjunction]);
\item
this $F$ is monoidal: it maps separated products to products (\in{Theorem}[thm:monoidal]);
\item
$U$ maps the exponent object in $\sbnom$ to the right adjoint $\wandto$ of the separated product, if the domain has dimension $\leq 1$ (\in{Theorem}[thm:exponent-separated], \in{Corollary}[cor:exponent-iso]).
\stopitemize

Together, these results form the categorical infrastructure to relate nominal languages to separated languages and automata in \in{Section}[sec:automata].

\startdefinition[reference=def:left-adjoint]
Given a $\perm$-nominal set $X$, we define a nominal $\sb$-set $F(X)$ as follows.
Define the set
\startformula
F(X) = \{ (m, x) \mid m \in \sb, x \in X \} / _\sim,
\stopformula
where $\sim$ is the least equivalence relation containing:
\startformula\startalign
\NC (m, g x) \NC \sim (m g, x), \NR
\NC (m, x)   \NC \sim (m', x) \quad \text{ if } m|_C = m'|_C \text{ for a }\perm\text{-support } C \text{ of } x, \NR
\stopalign\stopformula
for all $x \in X$, $m, m' \in \sb$ and $g \in \perm$.
The equivalence class of a pair $(m,x)$ is denoted by $[m,x]$.
We define an $\sb$-action on $F(X)$ as $n \cdot [m, x] = [n m , x]$.
\stopdefinition
Well-definedness is proved as part of \in{Proposition}[prop:functor] below.
Informally, an equivalence class $[m,x] \in F(X)$ behaves \quotation{as if $m$ acted on $x$}.
The first equation of $\sim$ ensures compatibility with the $\perm$-action on $x$, and the second equation ensures that $[m,x]$ only depends the relevant part of $m$.
The following characterisation of $\sim$ is useful in proofs.
\startlemma[reference=lm:sim]
We have $(m_1, x_1) \sim (m_2, x_2)$ iff there is a permutation $g \in \perm$ such that $g x_1 = x_2$ and $m_1|_C = m_2 g|_C$, for $C$ some $\perm$-support of $x_1$.
\stoplemma

\startremark
The first relation of $\sim$ in \in{Definition}[def:left-adjoint] comes from the construction of \quotation{extension of scalars} in commutative algebra (see \citenp[AtiyahM69]).
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$).
\stopremark

\startproposition[reference=prop:functor]
The construction $F$ in \in{Definition}[def:left-adjoint] extends to a functor
\startformula F \colon \permnom \to \sbnom , \stopformula
defined on an equivariant map $f \colon X \to Y$ by $F(f)([m, x]) = [m, f(x)] \in F(Y)$.
\stopproposition

\startproofnoqed
We first prove well-definedness and then the functoriality.
\startdescription{$F(X)$ is an $\sb$-set.}
To this end we check that the $\sb$-action is well-defined.
Let $[m_1, x_1] = [m_2, x_2] \in F(X)$ and let $m \in \sb$.
By \in{Lemma}[lm:sim], there is some permutation $g$ such that  $g x_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 $m m_1|_C = m m_2 g|_C$, which means (again by the lemma)
that $[m m_1, x_1] = [m m_2, x_2]$.
Thus $m [m_1, x_1] = m [m_2, x_2]$, which concludes well-definedness.

For associativity and unitality of the $\sb$-action, we simply note that it is
directly defined by left multiplication of $\sb$ which is associative and unital.
This concludes that $F(X)$ is an $\sb$-set.
\stopdescription
\startdescription{$F(X)$ is an nominal $\sb$ set.}
Given an element $[m, x] \in F(X)$ and a $\perm$-support $C$ of $x$, we will prove that $m \cdot C$ 
is an $\sb$-support for $[m, x]$.
Suppose that we have $m_1, m_2 \in \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.
\stopdescription
\startdescription{Functoriality.}
Let $f \colon X \to Y$ be a $\perm$-equivariant map.
To see that $F(f)$ is well-defined consider $[m_1, x_1] = [m_2, x_2]$.
By \in{Lemma}[lm:sim], there is a permutation $g$ such that  $g x_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(g x_1)] = [m_2, g f(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 $\sb$-equivariance we consider both $n \cdot F(f)([m, x]) = n [m, f(x)] = [n m, f(x)]$ and $F(f)(n \cdot [m, x]) = F(f)([nm, x]) = [nm, f(x)]$.
This shows that $n F(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.
\QED
\stopdescription
\stopproofnoqed

\starttheorem[reference=thm:adjunction]
The functor $F$ is left adjoint to $U$:
\placefigure[force, none]{}{
\hbox{\starttikzpicture[bend angle=15]
\node              (0) {$\permnom$};
\node [right of=0] (p) {$\perp$};
\node [right of=p] (1) {$\sbnom$};
\path[->]
(0) edge [bend left] node [above] {$F$} (1)
(1) edge [bend left] node [below] {$U$} (0);
\stoptikzpicture}}
\stoptheorem
\startproof
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 $\perm$-equivariant $f \colon X \to U(Y)$ there is a unique $\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) = [\id,x]$.
This is equivariant: $g \cdot \eta_X(x) = g [\id,x] = [g,x] = [\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 \sb$.
Then $U(f^\sharp) \circ \eta_X(x) = f^\sharp([\id, x]) = \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 \in{Lemma}[lm:sim], there is a $g \in \perm$ such that $g x_1 = x_2$ and $m_2 g |_C = m_1|_C$ for a $\perm$-support $C$ of $x_1$.
Now $C$ is also a $\perm$-support for $f(x)$ and hence it is an $\sb$-support of $f(x)$ (\in{Lemma}[lem:GM-support]).
We conclude that $m_2 \cdot f(x_2) = m_2 \cdot f(g x_1) = m_2 g \cdot f(x_1)  = m_1 \cdot f(x_1)$ (we use $\perm$-equivariance in the one but last step and $\sb$-support in the last step).
Finally, $\sb$-equivariance of $f^\sharp$ and uniqueness are straightforward calculations.
\stopproof

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 $\sb$-equivariant map;
then $g^{\flat} \colon X \to U(Y)$ is given by $g^{\flat}(x) = g([\id, x])$.
Note that the unit $\eta$ is a $\perm$-equivariant map, hence it preserves supports (i.e., any support of $x$ also supports $[\id, x]$).
This also means that if $C$ is a support of $x$, then $m \cdot C$ is a support of $[m, x]$ (by \in{Lemma}[lem:transfer-support]).


\startsubsection
  [title={On (separated) products}]

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

\starttheorem[reference=thm:monoidal]
The functor $F$ is strong monoidal, from the monoidal category\break $(\permset, \sepprod, 1)$ to $(\sbset, \times, 1)$.
In particular, the map $p$ given by
\startformula
p = \langle F(\pi_1), F(\pi_2) \rangle \colon F(X \sepprod Y) \to F(X) \times F(Y)
\stopformula
is an isomorphism, natural in $X$ and $Y$.
\stoptheorem
\startproofnoqed
We prove that $p$ is an isomorphism.
It suffices to show that $p$ is injective and surjective.
Note that $p([m, (x, y)]) = ([m, x], [m, y])$.

\startdescription[title={Surjectivity.}]
Let $([m_1, x], [m_2, y])$ be an element of $F(X) \times F(Y)$.
We take an element $y' \in Y$ such that $y' \separated \supp(x)$ and $y' = gy$ for some $g \in \perm$.
Now we have an element $(x, y') \in X \sepprod Y$.
By \in{Lemma}[lem:transfer-support], we have $\supp(y') = \supp(y)$.
Define the map
\startformula
m(x) =
\startmathcases
   \NC m_1(x)         \NC if $x \in \supp(x)$  \NR
   \NC m_2(g^{-1}(x)) \NC if $x \in \supp(y')$ \NR
   \NC x              \NC otherwise.           \NR
\stopmathcases
\stopformula
(Observe that $\supp(x) \separated \supp(y')$, so the cases are not overlapping.)
The map $m$ is an element of $\sb$.
Now consider the element $z = [m, (x, y')] \in F(X \sepprod Y)$.
Applying $p$ to $z$ gives the element $([m, x], [m, y'])$.
First, we note that $[m, x] = [m_1, x]$ by the definition of $m$.
Second, we show that $[m, y'] = [m_2, y]$. 
Observe that $m g|_{\supp(y)} = m_2|_{\supp(y)}$ by definition of $m$. 
Since $\supp(y)$ is a support of $y$, we have $[mg, y] = [m_2, y]$,
and since $[mg, y] = [m, g y] = [m, y']$ we are done.
Hence $p([m, (x, y')]) = ([m, x], [m, y']) = ([m_1, x], [m_2, y])$, so $p$ is surjective.
\stopdescription

\startdescription[title={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=\supp(x_1)$ and $D=\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$,
\startformula
g_0(z) =
\startmathcases
   \NC g_x(z)  \NC if $z \in C$  \NR
   \NC g_y(z)  \NC if $z \in D$. \NR
\stopmathcases
\stopformula
(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 \citep[Pitts13], the map $g_0$ extends to a permutation $g \in \perm$ 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.
\stopdescription

\startdescription[title={Unit and coherence.}]
To show that $F$ preserves the unit, we note that $[m, 1] = [m', 1]$ for every $m, m' \in \sb$, as the empty set supports $1$ and so $m|_{\emptyset} = m'|_{\emptyset}$ vacuously holds.
We conclude $F(1)$ is a singleton.
By the definition $p([m, (x, y)])=([m, x], [m, y])$, one can check the coherence axioms elementary.
\QED
\stopdescription
\stopproofnoqed

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.
\startcorollary[reference=cor:sep-words]
For any $\perm$-nominal set $X$, we have $F(X^{(*)}) \cong (FX)^*$.
\stopcorollary

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

\startlemma[reference=lem:1dim-iso]
The functors $F$ and $U$ are equivalences on $\leq 1$-dimensional objects.
Concretely, for $X \in \permnom$ and $Y \in \sbnom$:
\startitemize
\item If $\dim(X) \leq 1$, then the unit $\eta \colon X \to UF(X)$ is an isomorphism.
\item If $\dim(Y) \leq 1$, then the co-unit $\epsilon \colon FU(X) \to X$ is an isomorphism.
\stopitemize
\stoplemma

Before we prove this lemma, we need the following technical property of $\leq 1$-dimensional $\sb$-sets.

\startlemma[reference=lem:1dim-sbnom]
Let $Y$ be a nominal $\sb$-set.
If an element $y \in Y$ is supported by a singleton set (or even the empty set), then
\startformula
\{ m y \mid m \in \sb \} = \{ g y \mid g \in \perm \} .
\stopformula
\stoplemma
\startproof
Let $y \in Y$ be supported by $\{ a \}$ and let $m \in \sb$.
Now consider $b = m(a)$ and the bijection $g = \swap{a}{b}$.
Now $m|_{\{a\}} = g|_{\{a\}}$, meaning that $m y = g y$.
So the set $\{ m y \mid m \in \sb \}$ is contained in $\{ g y \mid g \in \perm \}$.
The inclusion the other way is trivial, which means $\{ m y \mid m \in \sb \} = \{ g y \mid g \in \perm \}$.
\stopproof
\start
{\it Proof of Lemma \ref[default][lem:1dim-iso].}
It is easy to see that $\eta \colon x \mapsto [\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 = \swap{a}{b}$.
Now $[m, x] = [m g^{-1}, g x]$ and note that $\{ b \}$ supports $g x$ and $m g^{-1}|_{\{b\}} = \id|_{\{b\}}$.
We continue with $[m g^{-1}, g x] = [\id, g x]$, which concludes that $g x$ is the preimage of $[m, x]$.
Hence $\eta$ is an isomorphism.

To see that $\epsilon \colon [m, y] \mapsto m y$ is surjective, just consider $m = \id$.
To see that $\epsilon$ is injective, let $[m, y], [m', y'] \in FU(Y)$ be two elements such that $m y = m' y'$.
Then by using \in{Lemma}[lem:1dim-sbnom] we find $g, g' \in \perm$ such that $g y = m y = m' y' = g' y'$.
This means that $y$ and $y'$ are in the same orbit (of $U(Y)$) and have the same dimension.
Case 1: $\supp(y) = \supp(y') = \emptyset$, then $[m, y] = [\id, y] = [\id, y'] = [m', y']$.
Case 2: $\supp(y) = \{ a \}$ and $\supp(y') = \{ b \}$, then $\supp(g y) = \{ g(a) \}$ (\in{Lemma}[lem:transfer-support]).
In particular we now now that $m$ and $g$ map $a$ to $c = g(a)$, likewise $m'$ and $g'$ map $b$ to $c$.
Now $[m, y] = [m, g^{-1} g' y'] = [m g^{-1} g', y'] = [m', y']$, where we used $m g^{-1} g (b) = c = m'(b)$ in the last step.
This means that $\epsilon$ is injective and hence an isomorphism.
\QED\blank[big]\noindentation
\stop

By \in{Lemma}[lem:1dim-iso], we may consider the set $\atoms$ as both $\sb$-set and $\perm$-set (abusing notation).
And we get an isomorphism $F(\atoms) \cong \atoms$ of nominal $\sb$-sets.
To appreciate the above results, we give a concrete characterisation of one-dimensional nominal sets:
\startlemma[reference=lm:char-dim-one]
Let $X$ be a nominal $M$-set, for $M \in \{\sb,\perm\}$.
Then $\dim(X) \leq 1$ iff there exist (discrete) sets $Y$ and $I$ such that $X \cong Y + \coprod_{I} \atoms$.
\stoplemma

In particular, the one-dimensional objects include the alphabets used for \emph{data words}, consisting of a product $S \times \atoms$ 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., \citenp[IsbernerHS14]).

By the above and \in{Theorem}[thm:monoidal], $F$ maps separated powers of $\atoms$ to powers, and the set of separated words over $\atoms$ to the $\sb$-set of words over $\atoms$.
\startcorollary[reference=prop:An-iso]
We have $F(\atoms^{(n)}) \cong \atoms^n$ and $F(\atoms^{(*)}) \cong \atoms^{*}$.
\stopcorollary


\stopsubsection
\startsubsection
  [title={On exponents}]

We have described how $F$ and $U$ interact with (separated) products.
In this section, we establish a relationship between the magic wand ($\wandto$) and the exponent of nominal $\sb$-sets ($\sbto$).

\startdefinition
Let $X \in \permnom$ and $Y \in \sbnom$.
We define a $\perm$-equivariant map $\phi$ as follows:
\startformula
\phi \colon (X \wandto U(Y)) \to U(F(X) \sbto Y)
\stopformula
is defined by using the composition
\startformula
F(X \wandto U(Y)) \times F(X) \tot{p^{-1}} F((X \wandto U(Y)) \sepprod X) \tot{F(\ev)} FU(Y) \tot{\epsilon} Y,
\stopformula
where $p^{-1}$ is from \in{Theorem}[thm:monoidal] and $\ev$ is the evaluation map of the exponent $\wandto$.
By Currying and the adjunction we arrive at $\phi$:

\placefigure[force,none]{}{
\hbox{\starttikzpicture[node distance=16pt]
\node              (1) {$F(X \wandto U(Y)) \times F(X) \to Y$};
\node [below of=1] (2) {$F(X \wandto U(Y)) \to (F(X) \sbto Y)$};
\node [below of=2] (3) {$\phi \colon (X \wandto U(Y)) \to U(F(X) \sbto Y)$};
\node [fit=(1) (2), inner sep=1pt] (12) {};
\node [fit=(2) (3), inner sep=1pt] (23) {};

\node [anchor=west] at (12.east) {by Currying};
\node [anchor=west] at (23.east) {by \in{Theorem}[thm:adjunction]};

\draw (12.west) -- (12.east);
\draw (23.west) -- (23.east);
\stoptikzpicture}}
\stopdefinition

With this map we can prove a generalisation of \in{Theorem}[thm:adjunction].
In particular, the following lemma 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 $\perm$-equivariant.
Second, it extends the correspondence to all finitely supported maps and not just the equivariant ones.

\starttheorem[reference=thm:exponent-separated]
The sets $X \wandto U(Y)$ and $U(F(X) \sbto Y)$ are naturally isomorphic via $\phi$ as nominal $\perm$-sets.
\stoptheorem
\startproof
We define some additional maps in order to construct the inverse of $\phi$.
First, from \in{Theorem}[thm:adjunction] we get the following isomorphism:
\startformula
q \colon U(X \times Y) \tot{=} U(X) \times U(Y)
\stopformula
Second, with this map and Currying, we obtain the following two natural maps:

\placefigure[force,none]{}{
\hbox{\starttikzpicture[node distance=16pt]
\node              (1) {$U(F(X) \sbto Y) \times UF(X) \tot{q^{-1}} U((F(X) \sbto Y) \times F(X)) \tot{U(\ev)} U(Y)$};
\node [below of=1] (2) {$\alpha \colon U(F(X) \sbto Y) \to (UF(X) \permto U(Y))$};
\node [fit=(1) (2), inner sep=1pt] (12) {};

\node [anchor=west] at (12.east) {by Currying};

\draw (12.west) -- (12.east);
\stoptikzpicture}}

\placefigure[force,none]{}{
\hbox{\starttikzpicture[node distance=16pt]
\node              (1) {$(UF(X) \permto U(Y)) \times X \tot{\id {\times} \eta} (UF(X) \permto U(Y)) \times UF(X) \tot{\ev} U(Y)$};
\node [below of=1] (2) {$\beta \colon (UF(X) \permto U(Y)) \to (X \permto U(Y))$};
\node [fit=(1) (2), inner sep=1pt] (12) {};

\node [anchor=west] at (12.east) {by Currying};

\draw (12.west) -- (12.east);
\stoptikzpicture}}

Last, we note that the inclusion $A \sepprod B \subseteq A \times B$ induces a \emph{restriction} map $r \colon (B \permto C) \to (B \wandto C)$ (again by Currying).
A calculation shows that $r \circ \beta \circ \alpha$ is the inverse of $\phi$.
\stopproof

Note that this theorem gives an alternative characterisation of the magic wand in terms of the exponent in $\sbnom$, if the codomain is $U(Y)$.
Moreover, for a $1$-dimensional object $X$ in $\sbnom$, we obtain the following special case of the theorem (using the co-unit isomorphism from \in{Lemma}[lem:1dim-iso]):

\startcorollary[reference=cor:exponent-iso]
Let $X, Y$ be nominal $\sb$-sets.
For $1$-dimensional $X$, the nominal $\perm$-set $U(X) \wandto U(Y)$ is naturally isomorphic to $U(X \sbto Y)$.
\stopcorollary

\startremark
The set $\atoms \wandto U(X)$ coincides with the atom abstraction $[\atoms] UX$ (\in{Remark}[rem:atom-abstr]).
Hence, as a special case of \in{Corollary}[cor:exponent-iso], we recover Theorem 34 of \citet[GabbayH08],
which states a bijective correspondence between $[\atoms] UX$ and $U(\atoms \sbto X)$.
\stopremark


\stopsubsection
\stopsection
\startsection
  [title={Nominal and separated automata},
   reference=sec:automata]

In this section, we study nominal 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 \emph{separated nominal automata}.
These automata represent nominal languages which are $\sb$-equivariant, essentially meaning they are closed under substitution.
Our main result is that, if a \quote{classical} nominal automaton (over $\perm$) represents a language $L$ which is $\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.

\startdefinition[reference=def:nominal-aut]
Let $\Sigma, O$ be $\perm$-sets, called input/output alphabet respectively.
\startitemize
\item
A \emph{($\perm$)-nominal language} is an equivariant map of the form $L \colon \Sigma^* \to O$.
\item 
A \emph{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.

\item 
The \emph{language semantics} is the map $l \colon Q \times \Sigma^* \rightarrow O$, 
defined inductively by
\startformula
	l(x, \varepsilon) = o(x)\,, \qquad l(x, aw) = l(\delta(x,a),w)
\stopformula
for all $x \in Q$, $a \in \Sigma$ and $w \in \Sigma^*$.

\item For $l^\flat \colon Q \rightarrow (\Sigma^* \permto O)$ the transpose of $l$, 
we have that $l^\flat(q_0) \colon \Sigma^* \rightarrow O$ is equivariant;
this is called the \emph{language accepted by $\mathcal{A}$}.
\stopitemize
\stopdefinition
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, 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 \emph{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})$. 

\startexample[reference=ex:fifo]
We model a bounded FIFO queue of size $n$ as a nominal Moore automaton, explicitly handling the data in the automaton structure.
\footnote{We use a reactive version of the queue data structure which is slightly different from the versions of \citet[MoermanS0KS17, IsbernerHS14].}
The input alphabet $\Sigma$ and output alphabet $O$ are as follows:
\startformula
\Sigma = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \},
 \qquad O = \atoms \cup \{ \Null \}.
\stopformula

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 $\Null$ if the queue is empty.
A queue of size $n$ is modelled by the automaton $(Q, \delta, o, q_0)$ defined as follows.
\startformula
Q = \atoms^{\leq n} \cup \{ \perp \},
\qquad q_0 = \epsilon,
\qquad o(a_1 \ldots a_k) =
     \startmathcases
         \NC a_1   \NC if $k \geq 1$ \NR
         \NC \Null \NC otherwise     \NR
     \stopmathcases
\stopformula
\startformula
\delta(a_1 \ldots a_k, \Put(b)) =
     \startmathcases[numberdistance=0pt]
         \NC a_1 \ldots a_k b \NC if $k < n$ \NR
         \NC \perp            \NC otherwise  \NR
     \stopmathcases
\quad
\delta(a_1 \ldots a_k, \Pop) =
     \startmathcases[numberdistance=0pt]
         \NC a_2 \ldots a_k \NC if $k > 0$ \NR
         \NC \perp          \NC otherwise  \NR
     \stopmathcases
\stopformula
\startformula
\delta(\bot, x) = \bot
\stopformula
The automaton is depicted in \in{Figure}[fig:fifo] 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 $\Null$ if the input is ill-behaved, i.e., $\Pop$ is applied to an empty queue or $\Put(a)$ to a full queue.

\startplacefigure
  [title={The FIFO automaton from \in{Example}[ex:fifo] with $n = 3$.
          The right-most state consists of \emph{five} orbits as we can take $a, b, c$ distinct, all the same, or two of them equal in three different ways.
          Consequently, the complete state space has ten orbits.
          The output of each state is denoted in the lower part.},
   list={The FIFI automaton with $n=3$.},
   reference=fig:fifo]
\hbox{\starttikzpicture[node distance=3.33cm, bend angle=10, initial text=]
  \node[state with output, initial] (0) {$\epsilon$ \nodepart{lower} $o = {\perp}$};
  \node[state with output, right of=0] (1) {$a$     \nodepart{lower} $o = a$};
  \node[state with output, right of=1] (2) {$a b$   \nodepart{lower} $o = a$};
  \node[state with output, right of=2] (3) {$a b c$ \nodepart{lower} $o = a$};
  \node[state with output, below=.5cm of 0] (s) {$\perp$ \nodepart{lower} $o = {\perp}$};
  
  \path[trans]
  (0) edge [bend right] node [below] {$\Put(a)$} (1)
  (0) edge              node [left]  {$\Pop$} (s)
  (1) edge [bend right] node [above] {$\Pop$} (0)
  (1) edge [bend right] node [below] {$\Put(b)$} (2)
  (2) edge [bend right] node [above, align=center] {$\Pop$ \\ goes to $b$} (1)
  (2) edge [bend right] node [below] {$\Put(c)$} (3)
  (3) edge [bend right] node [above, align=center] {$\Pop$ \\ goes to $b c$} (2)
  (3) edge [bend left=17] node [below right] {$\Put(d)$} (s)
  (s) edge [loop below] node {$\Sigma$} (s);
\stoptikzpicture}
\stopplacefigure
\stopexample


\startdefinition[reference=def:sep-aut]
Let $\Sigma, O$ be $\perm$-sets.
A \emph{separated language} is an equivariant map of the form $\Sigma^{(*)} \to O$.
A \emph{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 \sepprod \Sigma \rightarrow Q$.

The \emph{separated language semantics} of such an automaton is given by the map $s \colon Q \sepprod \Sigma^{(*)} \rightarrow O$, 
defined by
\startformula
	s(x, \epsilon) = o(x), \qquad s(x, aw) = s(\delta(x,a),w)
\stopformula
for all $x \in Q$, $a \in \Sigma$ and $w \in \Sigma^{(*)}$ such that $x \separated aw$ and $a \separated w$.

Let $s^\flat \colon Q \to (\Sigma^{(*)} \wandto O)$ be the transpose of $s$.
Then $s^\flat(q_0) \colon \Sigma^{(*)} \to O$ corresponds to a separated language,
this is called the \emph{separated language accepted by $\mathcal{A}$}.
\stopdefinition

By definition of the separated product, the transition function is only defined
on a state $x$ and letter $a \in \Sigma$ if $x \separated a$. 
In \in{Example}[ex:sep-aut-fifo] 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 \emph{all} words, provided that both the input alphabet $\Sigma$ and the output alphabet $O$ are $\sb$-sets.
\startdefinition
	Let $\Sigma$ and $O$ be nominal $\sb$-sets.
	An $\sb$-equivariant function $L \colon \Sigma^* \to O$ is called an \emph{$\sb$-language}.
\stopdefinition
Notice the difference between an $\sb$-language $L \colon \Sigma^* \to O$ 
and a $\perm$-language $L' \colon (U \Sigma)^* \rightarrow U(O)$. They are both functions from
$\Sigma^{*}$ to $O$, but the latter is only $\perm$-equivariant,
while the former satisfies the stronger property of $\sb$-equivariance.
Languages over separated words, and $\sb$-languages, are connected as follows.

\starttheorem[reference=thm:extension]
Suppose $\Sigma, O$ are both nominal $\sb$-sets, and suppose $\dim(\Sigma) \leq 1$.
There is a one-to-one correspondence
\startformula
\frac{S \colon (U\Sigma)^{(*)} \rightarrow UO \quad\text{ $\perm$-equivariant}}
{\overline{S} \colon \Sigma^* \rightarrow O \quad \text{ $\sb$-equivariant}}
\stopformula
between separated languages and $\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 \separated b_i$ for all $i$, and $b_i \separated b_j$ for all $i,j$ with $i \neq j$.
Define $m \in \sb$ by
\startformula
m(a) =
\startmathcases
\NC a_i \NC if $a = b_i$ for some $i$ \NR
\NC a   \NC otherwise
\stopmathcases
\stopformula
Then $\overline{S}(a_1a_2a_3\cdots a_n) = m \cdot S(b_1 b_2 b_3 \cdots b_n)$.
\stoptheorem
\startproof
There is the following chain of one-to-one correspondences, from the results of the previous section:
\placefigure[force,none]{}{
\hbox{\starttikzpicture[node distance=16pt]
\node              (1) {$(U\Sigma)^{(*)} \rightarrow UO$};
\node [below of=1] (2) {$F(U\Sigma)^{(*)} \rightarrow O$};
\node [below of=2] (3) {$(FU\Sigma)^* \rightarrow O$};
\node [below of=3] (4) {$\Sigma^* \rightarrow O$};
\node [fit=(1) (2), inner sep=1pt] (12) {};
\node [fit=(2) (3), inner sep=1pt] (23) {};
\node [fit=(3) (4), inner sep=1pt] (34) {};

\node [anchor=west] at (12.east) {by {\in{Theorem}[thm:adjunction]} };
\node [anchor=west] at (23.east) {by {\in{Corollary}[cor:sep-words]} };
\node [anchor=west] at (34.east) {by {\in{Lemma}[lem:1dim-iso]} };

\draw (12.west) -- (12.east);
\draw (23.west) -- (23.east);
\draw (34.west) -- (34.east);
\stoptikzpicture}}
\stopproof

Thus, every separated automaton over $U(\Sigma), U(O)$ gives rise to an $\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 \in{Definition}[def:restr-aut].
It turns out that if the $(\perm)$-language accepted by $\mathcal{A}$ is actually an $\sb$-language, then the restricted automaton already represents this language, as the extension $\overline{S}$ of the associated separated language $S$ (\in{Theorem}[thm:separated-sb-lang]).
Hence, in such a case, the restricted separated automaton suffices to describe the language of $\mathcal{A}$.

\startdefinition[reference=def:restr-aut]
Let $i \colon Q \sepprod U(\Sigma) \to 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
\startformula
\mathcal{A}_* = (Q, \delta \circ i, o, q_0).
\stopformula
\stopdefinition

\starttheorem[reference=thm:separated-sb-lang]
Suppose $\Sigma, O$ are both $\sb$-sets, and suppose $\dim(\Sigma) \leq 1$.
Let $L \colon (U\Sigma)^* \to UO$ be the $\perm$-nominal language accepted by a nominal automaton $\mathcal{A}$, and suppose $L$ is $\sb$-equivariant.
Let $S$ be the separated language accepted by $\mathcal{A}_*$.
Then
$L = U(\overline{S})$.
\stoptheorem
\startproof
If follows from the one-to-one correspondence in \in{Theorem}[thm:extension]:
one the bottom there are two language ($L$ and $U(\overline{S})$), while there is only the restriction of $L$ on the top.
We conclude that $L = U(\overline{S})$.
\stopproof

As we will see in \in{Example}[ex:sep-aut-fifo], separated automata allow us to represent $\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.

\startproposition
For any nominal automaton $\mathcal{A}$, we have
$R(\mathcal{A}_*) \subseteq R(\mathcal{A})$.
\stopproposition
The converse inclusion of the above proposition does certainly not hold, as shown by the following example.

\startexample[reference=ex:sep-aut-fifo]
Let $\mathcal{A}$ be the automaton modelling a bounded FIFO queue (for some $n$), from \in{Example}[ex:fifo].
The $\perm$-nominal language $L$ accepted by $\mathcal{A}$ is $\sb$-equivariant: it is closed under application of arbitrary substitutions.

The separated automaton $\mathcal{A}_*$ is given simply be restricting the transition function to $Q \sepprod \Sigma$, i.e., a $\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 \in{Theorem}[thm:separated-sb-lang], 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 \emph{reachable} part of $\mathcal{A}_*$ is given by
\startformula
R_{\mathcal{A}_*} =  \atoms^{(\leq n)} \cup \{ \perp \}.
\stopformula
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.
\stopexample


\startsubsection
  [title={Separated automata: coalgebraic perspective},
   reference=sec:sep-aut]

Nominal automata and separated automata can be presented as \emph{coalgebras} on the category of $\perm$-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 $\sb$-languages, by establishing $\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 \in{Section}[sec:adjunction].
In the remainder of this section we assume familiarity with the theory
of coalgebras, see, e.g., \citet[jacobs-coalg, Rutten00].

\startdefinition[reference=def:nominal-aut-coalg]
Let $M$ be a submonoid of $\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 \MNom \to \MNom$ by $B_M(X) = O \times (\Sigma \mto X)$.
An \emph{($M$)-nominal (Moore) automaton} is a $B_M$-coalgebra.
\stopdefinition

A $B_M$-coalgebra can be presented as a nominal set $Q$ together with the pairing
\startformula
\langle o, \delta^\flat \rangle \colon Q \to O \times (\Sigma \mto Q)
\stopformula
of an equivariant \emph{output} function $o \colon Q \to O$,
and (the transpose of) an equivariant \emph{transition} function $\delta \colon Q \times \Sigma \to Q$.
In case $M = \perm$, this coincides with the automata of \in{Definition}[def:nominal-aut], omitting initial states.
The language semantics is generalised accordingly, as follows.
Given such a $B_M$-coalgebra $(Q, \langle o, \delta^\flat \rangle)$, the \emph{language semantics} $l \colon Q \times \Sigma^* \to O$ is given by
\startformula
l(x, \varepsilon) = o(x)\,, \qquad l(x, aw) = l(\delta(x,a),w)
\stopformula
for all $x \in S$, $a \in \Sigma$ and $w \in \Sigma^*$.

\starttheorem[reference=thm:final-nom-aut]
Let $M$ be a submonoid of $\sb$, let $\Sigma$, $O$ be nominal $M$-sets.
The nominal $M$-set $\Sigma^* \mto O$ extends to a final $B_M$-coalgebra $(\Sigma^* \mto O, \zeta)$, such that the unique homomorphism from a given $B_M$-coalgebra is the transpose $l^\flat$ of the language semantics.
\stoptheorem

A \emph{separated automaton} (\in{Definition}[def:sep-aut], without initial states)
corresponds to a coalgebra for the functor $\sa \colon \permnom \to \permnom$ given by $\sa(X) = O \times (\Sigma \wandto X)$.
The separated language semantics arises by finality.
\starttheorem[reference=thm:final-sep]
The set $\Sigma^{(\ast)} \wandto O$ is the carrier of a final $\sa$-coalgebra,
such that the unique coalgebra homomorphism from a given $\sa$-coalgebra $(Q,\langle o, \delta \rangle)$ is the transpose $s^\flat\!$ of the separated language semantics $s \colon Q \sepprod \Sigma^{(\ast)} \rightarrow O$
(\in{Definition}[def:sep-aut]).
\stoptheorem

Next, we provide an alternative final $\sa$-coalgebra which assigns $\sb$-nominal languages to states of separated nominal automata.
The essence is to obtain a final $\sa$-coalgebra from the final $B_{\sb}$-coalgebra.
In order to prove this, we use a technique to lift adjunctions to categories of coalgebras.
This technique occurs more often in the coalgebraic study
of automata \citep[JSS14, KlinR16, KerstanKW14].

\starttheorem[reference=thm:adjunction-lift]
Let $\Sigma$ be a $\perm$-set, and $O$ an $\sb$-set.
Define $\sa$ and $B_{\sb}$ accordingly, as $\sa(X) = UO \times (\Sigma \wandto X)$
and $B_{\sb}(X) = O \times (F\Sigma \sbto X)$.

There is an adjunction $\overline{F} \dashv \overline{U}$ in:
\placefigure[force, none]{}{
\hbox{\starttikzpicture[bend angle=15]
\node              (0) {$\text{\ss CoAlg}(\sa)$};
\node [right of=0] (p) {$\perp$};
\node [right of=p] (1) {$\text{\ss CoAlg}(B_{Sb})$};
\path[->]
(0) edge [bend left] node [above] {$\overline{F}$} (1)
(1) edge [bend left] node [below] {$\overline{U}$} (0);
\stoptikzpicture}}
where $\overline{F}$ and $\overline{U}$ coincide with $F$ and $U$ respectively on carriers.
\stoptheorem
\startproof
There is a natural isomorphism
$ \lambda \colon \sa U \to U B_{\sb} $
given by
\startformula
\lambda \colon UO \times (\Sigma \wandto UX) \xrightarrow{\id \times \phi} UO \times U(F \Sigma \sbto X) \xrightarrow{\cong} U(O \times (F \Sigma \sbto X)),
\stopformula
where $\phi$ is the isomorphism from \in{Theorem}[thm:exponent-separated] and the isomorphism on the right comes from $U$ being a right adjoint.
The result now follows from Theorem 2.14 of \citet[HermidaJ98].
In particular, $\overline{U}(X, \gamma) = (UX, \lambda^{-1} \circ U(\gamma))$.
\stopproof

Since right adjoints preserve limits, and final objects in particular, we obtain the following.
This gives an $\sb$-semantics of separated automata through finality.

\startcorollary[reference=cor:final-coalgs]
Let $((F \Sigma)^* \sbto O, \zeta)$  be the final $B_{\sb}$-coalgebra (\in{Theorem}[thm:final-nom-aut]).
The $\sa$-coalgebra $\overline{U}(\Sigma^* \sbto O, \zeta)$ is final and carried
by the set $ (F \Sigma)^* \sbto O $ of $\sb$-nominal languages. 
\stopcorollary


\stopsubsection
\stopsection
\startsection
  [title={Related and future work}]

\citet[FioreT01] described a similar adjunction between certain presheaf categories.
However, \citet[Staton07] describes in his thesis that the usage of presheaves allows for many degenerate models and one should look at sheaves instead.
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 \citet[BojanczykKL14].
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 \emph{all} the values in between to that value.
Whether the adjunction from \in{Theorem}[thm:adjunction] 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 $\sb$-language, then we are better off learning a separated automaton directly.
From the $\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\'{n}czyk et al. prove that nominal automata are equivalent to register automata in terms of expressiveness \citep[BojanczykKL14].
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 (\in{Example}[ex:fifo]).
We have shown that the exponential blow-up is avoidable by using separated automata, for this example and in general for $\sb$-equivariant languages.
An 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 $\permnom$ and incorporate it in the automaton model.
We believe that this is the hypothesised \quotation{substitution monad} from \in{Chapter}[chap:learning-nominal-automata].
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 \citep[SilvaBBR13].

%Super-separated automata $X \to O \sepprod (\Sigma \wandto X)$.
%\todo{}


\stopsection
\startsubject[title={Acknowledgements}]

We would like to thank Gerco van Heerdt for his useful comments.


\stopsubject
\referencesifcomponent
\stopchapter
\stopcomponent