diff --git a/content/separated-nominal-automata.tex b/content/separated-nominal-automata.tex index 8e03bcf..8330b58 100644 --- a/content/separated-nominal-automata.tex +++ b/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. -However, the second is non-trivial and uses the following technical property of $\leq 1$-dimensional $\sb$-sets. +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. @@ -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].