Separated nom aut.

content/separated-nominal-automata.tex

@@ -142,7 +142,7 @@ 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$.
+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
 
@@ -172,14 +172,14 @@ 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 exploding nominal sets of \citet[Gabbay07], but even worse behaved.
+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)$.
+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],
@@ -192,7 +192,7 @@ Moreover, any $g \in \perm$ preserves least supports: $g \cdot \supp(x) = \supp(
 \stoplemma
 
 The latter equality does not hold in general for a monoid $M$.
-For instance, the \quote{exploding} nominal renaming sets by \citet[GabbayH08] give counterexamples for $M = \sb$.
+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)$.
@@ -230,7 +230,7 @@ An important example is the set $\atoms^{(\ast)}$ of separated words over the at
 \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 paper, but for a complete presentation we briefly recall the description from \citet[Clouston13] (see also the book of \citenp[Pitts13]).
+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}\}$.
@@ -257,7 +257,7 @@ However, the set $\atoms \sepprod \atoms$ is not an equivariant subset when cons
 
 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$.
-More precisely, the main results are:
+The main results are:
 \startitemize[after]
 \item
 the forgetful functor $U \colon \sbnom \to \permnom$ has a left adjoint $F$ (\in{Theorem}[thm:adjunction]);
@@ -305,8 +305,9 @@ defined on an equivariant map $f \colon X \to Y$ by $F(f)([m, x]) = [m, f(x)] \i
 \stopproposition
 
 \startproofnoqed
+We first prove well-definedness and then the functoriality.
 \startdescription{$F(X)$ is an $\sb$-set.}
-We first check whether the $\sb$-action is well-defined.
+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$.
@@ -318,7 +319,7 @@ 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 $\sb$-nominal set.}
+\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}$.
@@ -469,8 +470,7 @@ Concretely, for $X \in \permnom$ and $Y \in \sbnom$:
 \stopitemize
 \stoplemma
 
-The first item follows easily by showing that $\eta$ is surjective.
+Before we prove this lemma, we need the following technical property of $\leq 1$-dimensional $\sb$-sets.
-However, the second is non-trivial and uses the following technical property of $\leq 1$-dimensional $\sb$-sets.
 
 \startlemma[reference=lem:1dim-sbnom]
 Let $Y$ be a nominal $\sb$-set.
@@ -479,14 +479,44 @@ If an element $y \in Y$ is supported by a singleton set (or even the empty set),
 \{ 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
-By \in{Lemma}[lem:1dim-iso], considering the set $\atoms$ as both $\sb$-set and $\perm$-set (abusing notation), we get an isomorphism $F(\atoms) \cong \atoms$ of nominal $\sb$-sets.
+
-Note that one-dimensional objects include the alphabets used for \emph{data words} \cite{IsbernerHS14}, consisting of a product $S \times \atoms$ of a discrete set $S$ of action labels and the set of atoms.
+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]
@@ -518,7 +548,7 @@ By Currying and the adjunction we arrive at $\phi$:
 \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) {$(X \wandto U(Y)) \to U(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) {};
 
@@ -568,8 +598,8 @@ Second, with this map and Currying, we obtain the following two natural maps:
 \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$.
-\footnote{We use $r_{X, U(Y)} \colon (X \permto U(Y)) \to (X \wandto U(Y))$ here.}
 \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)$.
@@ -625,12 +655,12 @@ this is called the \emph{language accepted by $\mathcal{A}$}.
 \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 \cite[BojanczykKL14], but there is no need to assume this for now.
+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[MSSKS17, IsbernerHS14].}
+\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 \},
@@ -794,6 +824,11 @@ 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}_*$.
@@ -803,7 +838,7 @@ The reachable part is defined similarly (but only where $\delta$ is defined) and
 For any nominal automaton $\mathcal{A}$, we have
 $R(\mathcal{A}_*) \subseteq R(\mathcal{A})$.
 \stopproposition
-The converse of the above proposition does certainly not hold, as shown by the following example.
+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].