Laatste hoofdstuk (nog niet helemaal gechecked)
This commit is contained in:
Joshua Moerman
parent
b7eb986943
commit
2f3d61eabe
6 changed files with 1085 additions and 5 deletions
207
biblio.bib
207
biblio.bib
|
|
@ -2286,3 +2286,210 @@
|
||||||
comment = {More recent: On Test Derivation from Partial Specifications, 2000.
|
comment = {More recent: On Test Derivation from Partial Specifications, 2000.
|
||||||
{\&} Testing from partial deterministic FSM specifications, 2005.}
|
{\&} Testing from partial deterministic FSM specifications, 2005.}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@inproceedings{BojanczykKLT13,
|
||||||
|
author = {Miko{\l}aj Boja{\'{n}}czyk and
|
||||||
|
Bartek Klin and
|
||||||
|
Slawomir Lasota and
|
||||||
|
Szymon Toru{\'{n}}czyk},
|
||||||
|
title = {Turing Machines with Atoms},
|
||||||
|
booktitle = {28th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
|
||||||
|
2013, New Orleans, LA, USA, June 25-28, 2013},
|
||||||
|
pages = {183--192},
|
||||||
|
year = {2013},
|
||||||
|
url = {https://doi.org/10.1109/LICS.2013.24},
|
||||||
|
doi = {10.1109/LICS.2013.24},
|
||||||
|
timestamp = {Thu, 25 May 2017 00:42:40 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/lics/BojanczykKLT13},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{GabbayP99,
|
||||||
|
author = {Murdoch Gabbay and
|
||||||
|
Andrew M. Pitts},
|
||||||
|
title = {A New Approach to Abstract Syntax Involving Binders},
|
||||||
|
booktitle = {14th Annual {IEEE} Symposium on Logic in Computer Science, Trento,
|
||||||
|
Italy, July 2-5, 1999},
|
||||||
|
pages = {214--224},
|
||||||
|
year = {1999},
|
||||||
|
url = {https://doi.org/10.1109/LICS.1999.782617},
|
||||||
|
doi = {10.1109/LICS.1999.782617},
|
||||||
|
timestamp = {Thu, 25 May 2017 00:42:40 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/lics/GabbayP99},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@techreport{Gabbay07,
|
||||||
|
author = {Murdoch James Gabbay},
|
||||||
|
title = {Nominal Renaming Sets},
|
||||||
|
note = {Heriot-Watt University},
|
||||||
|
year = {2007},
|
||||||
|
url = {https://www.gabbay.org/paper.html#nomrs-tr}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{GabbayH08,
|
||||||
|
author = {Murdoch James Gabbay and
|
||||||
|
Martin Hofmann},
|
||||||
|
title = {Nominal Renaming Sets},
|
||||||
|
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
|
||||||
|
International Conference, {LPAR} 2008. Proceedings},
|
||||||
|
pages = {158--173},
|
||||||
|
year = {2008},
|
||||||
|
url = {https://doi.org/10.1007/978-3-540-89439-1\_11},
|
||||||
|
doi = {10.1007/978-3-540-89439-1\_11},
|
||||||
|
timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/lpar/GabbayH08},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{OHearn03,
|
||||||
|
author = {Peter W. O'Hearn},
|
||||||
|
title = {On bunched typing},
|
||||||
|
journal = {J. Funct. Program.},
|
||||||
|
volume = {13},
|
||||||
|
number = {4},
|
||||||
|
pages = {747--796},
|
||||||
|
year = {2003},
|
||||||
|
url = {https://doi.org/10.1017/S0956796802004495},
|
||||||
|
doi = {10.1017/S0956796802004495},
|
||||||
|
timestamp = {Sat, 27 May 2017 14:24:34 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/journals/jfp/OHearn03},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{HermidaJ98,
|
||||||
|
author = {Claudio Hermida and
|
||||||
|
Bart Jacobs},
|
||||||
|
title = {Structural Induction and Coinduction in a Fibrational Setting},
|
||||||
|
journal = {Inf. Comput.},
|
||||||
|
volume = {145},
|
||||||
|
number = {2},
|
||||||
|
pages = {107--152},
|
||||||
|
year = {1998},
|
||||||
|
url = {https://doi.org/10.1006/inco.1998.2725},
|
||||||
|
doi = {10.1006/inco.1998.2725},
|
||||||
|
timestamp = {Thu, 18 May 2017 09:54:19 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/journals/iandc/HermidaJ98},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@book{jacobs-coalg,
|
||||||
|
author = {Bart Jacobs},
|
||||||
|
title = {Introduction to Coalgebra: Towards Mathematics of States and Observation},
|
||||||
|
series = {Cambridge Tracts in Theoretical Computer Science},
|
||||||
|
volume = {59},
|
||||||
|
publisher = {Cambridge University Press},
|
||||||
|
year = {2016},
|
||||||
|
url = {https://doi.org/10.1017/CBO9781316823187},
|
||||||
|
doi = {10.1017/CBO9781316823187},
|
||||||
|
isbn = {9781316823187},
|
||||||
|
timestamp = {Tue, 16 May 2017 14:01:42 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/books/cu/J2016},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{Rutten00,
|
||||||
|
author = {Jan J. M. M. Rutten},
|
||||||
|
title = {Universal coalgebra: a theory of systems},
|
||||||
|
journal = {Theor. Comput. Sci.},
|
||||||
|
volume = {249},
|
||||||
|
number = {1},
|
||||||
|
pages = {3--80},
|
||||||
|
year = {2000},
|
||||||
|
url = {https://doi.org/10.1016/S0304-3975(00)00056-6},
|
||||||
|
doi = {10.1016/S0304-3975(00)00056-6},
|
||||||
|
timestamp = {Sun, 28 May 2017 13:20:01 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/journals/tcs/Rutten00},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{JSS14,
|
||||||
|
author = {B. Jacobs and
|
||||||
|
A. Silva and
|
||||||
|
A. Sokolova},
|
||||||
|
title = {Trace semantics via determinization},
|
||||||
|
journal = {J. Comput. Syst. Sci.},
|
||||||
|
volume = {81},
|
||||||
|
number = {5},
|
||||||
|
pages = {859--879},
|
||||||
|
year = {2015}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{KlinR16,
|
||||||
|
author = {Bartek Klin and
|
||||||
|
Jurriaan Rot},
|
||||||
|
title = {Coalgebraic trace semantics via forgetful logics},
|
||||||
|
journal = {Logical Methods in Computer Science},
|
||||||
|
volume = {12},
|
||||||
|
number = {4},
|
||||||
|
year = {2016},
|
||||||
|
url = {https://doi.org/10.2168/LMCS-12(4:10)2016},
|
||||||
|
doi = {10.2168/LMCS-12(4:10)2016},
|
||||||
|
timestamp = {Mon, 13 Aug 2018 16:48:39 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/journals/corr/KlinR16},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{KerstanKW14,
|
||||||
|
author = {Henning Kerstan and
|
||||||
|
Barbara K{\"{o}}nig and
|
||||||
|
Bram Westerbaan},
|
||||||
|
title = {Lifting Adjunctions to Coalgebras to (Re)Discover Automata Constructions},
|
||||||
|
booktitle = {Coalgebraic Methods in Computer Science - 12th {IFIP} {WG} 1.3 International
|
||||||
|
Workshop, {CMCS} 2014, Colocated with {ETAPS} 2014, Grenoble, France,
|
||||||
|
April 5-6, 2014, Revised Selected Papers},
|
||||||
|
pages = {168--188},
|
||||||
|
year = {2014},
|
||||||
|
url = {https://doi.org/10.1007/978-3-662-44124-4\_10},
|
||||||
|
doi = {10.1007/978-3-662-44124-4\_10},
|
||||||
|
timestamp = {Fri, 26 May 2017 00:50:45 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/cmcs/KerstanKW14},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@phdthesis{Staton07,
|
||||||
|
author = {Staton, Sam},
|
||||||
|
title = {{Name-passing process calculi: operational models and
|
||||||
|
structural operational semantics}},
|
||||||
|
year = 2007,
|
||||||
|
month = jun,
|
||||||
|
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-688.pdf},
|
||||||
|
institution = {University of Cambridge, Computer Laboratory},
|
||||||
|
number = {UCAM-CL-TR-688}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{SilvaBBR13,
|
||||||
|
author = {Alexandra Silva and
|
||||||
|
Filippo Bonchi and
|
||||||
|
Marcello M. Bonsangue and
|
||||||
|
Jan J. M. M. Rutten},
|
||||||
|
title = {Generalizing determinization from automata to coalgebras},
|
||||||
|
journal = {Logical Methods in Computer Science},
|
||||||
|
volume = {9},
|
||||||
|
number = {1},
|
||||||
|
year = {2013},
|
||||||
|
url = {https://doi.org/10.2168/LMCS-9(1:9)2013},
|
||||||
|
doi = {10.2168/LMCS-9(1:9)2013},
|
||||||
|
timestamp = {Mon, 13 Aug 2018 16:47:28 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1302-1046},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{FioreT01,
|
||||||
|
author = {Marcelo P. Fiore and
|
||||||
|
Daniele Turi},
|
||||||
|
title = {Semantics of Name and Value Passing},
|
||||||
|
booktitle = {16th Annual {IEEE} Symposium on Logic in Computer Science, Boston,
|
||||||
|
Massachusetts, USA, June 16-19, 2001, Proceedings},
|
||||||
|
pages = {93--104},
|
||||||
|
publisher = {{IEEE} Computer Society},
|
||||||
|
year = {2001},
|
||||||
|
url = {https://doi.org/10.1109/LICS.2001.932486},
|
||||||
|
doi = {10.1109/LICS.2001.932486},
|
||||||
|
timestamp = {Thu, 25 May 2017 00:42:40 +0200},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/lics/FioreT01},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
|
|
||||||
|
|
@ -35,7 +35,7 @@
|
||||||
\startpart[title={Nominal Techniques}]
|
\startpart[title={Nominal Techniques}]
|
||||||
\component content/learning-nominal-automata
|
\component content/learning-nominal-automata
|
||||||
\component content/ordered-nominal-sets
|
\component content/ordered-nominal-sets
|
||||||
\chapter{Succinct Nominal Automata?}
|
\component content/separated-nominal-automata
|
||||||
\stoppart
|
\stoppart
|
||||||
\stopbodymatter
|
\stopbodymatter
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -372,7 +372,7 @@ The following chapters are split into two parts.
|
||||||
\in{Part}[part:testing] contains material about testing techniques, while \in{Part}[part:nominal] is about nominal techniques.
|
\in{Part}[part:testing] contains material about testing techniques, while \in{Part}[part:nominal] is about nominal techniques.
|
||||||
Each chapter could be read in isolation.
|
Each chapter could be read in isolation.
|
||||||
However, the chapters do get more technical and mathematical -- especially in \in{Part}[part:nominal].
|
However, the chapters do get more technical and mathematical -- especially in \in{Part}[part:nominal].
|
||||||
\todo{Should I be more clear about my contribution?}
|
\todo{Should I be more concrete about my contribution?}
|
||||||
|
|
||||||
\startdescription[title={\in{Chapter}[chap:test-methods]: FSM-based test methods.}]
|
\startdescription[title={\in{Chapter}[chap:test-methods]: FSM-based test methods.}]
|
||||||
This chapter introduces test generation methods which can be used for learning.
|
This chapter introduces test generation methods which can be used for learning.
|
||||||
|
|
@ -472,7 +472,7 @@ These machines can be decomposed by projecting on each output,
|
||||||
resulting in smaller components that can be learned with fewer queries.
|
resulting in smaller components that can be learned with fewer queries.
|
||||||
We give experimental evidence that this is a useful technique which can reduce the number of queries substantially.
|
We give experimental evidence that this is a useful technique which can reduce the number of queries substantially.
|
||||||
This is all motivated by the idea that compositional methods are widely used throughout engineering and that we should use this in model learning.
|
This is all motivated by the idea that compositional methods are widely used throughout engineering and that we should use this in model learning.
|
||||||
This was presented by Vaandrager at ICGI:
|
This was presented by Frits Vaandrager at ICGI:
|
||||||
|
|
||||||
\cite[entry][Moerman18].
|
\cite[entry][Moerman18].
|
||||||
\stopdescription
|
\stopdescription
|
||||||
|
|
|
||||||
838
content/separated-nominal-automata.tex
Normal file
838
content/separated-nominal-automata.tex
Normal file
|
|
@ -0,0 +1,838 @@
|
||||||
|
\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
|
||||||
|
|
||||||
|
|
||||||
|
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 \citep[BojanczykKL14],
|
||||||
|
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[BojanczykKL14, 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 \citet[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
|
||||||
|
|
||||||
|
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 \quote{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 paper, 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$.
|
||||||
|
More precisely, 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].
|
||||||
|
\todo{Reconsider moving some proofs from the appendix to the main text}.
|
||||||
|
|
||||||
|
\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
|
||||||
|
|
||||||
|
\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 $(\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
|
||||||
|
\startproof
|
||||||
|
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.
|
||||||
|
\stopdescription
|
||||||
|
\stopproof
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
To appreciate the above result, 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.
|
||||||
|
|
||||||
|
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 transposing (first by Currying, then by the adjunction) the following composition
|
||||||
|
\startformula
|
||||||
|
F(X \wandto U(Y)) \times F(X) \xrightarrow{p^{-1}} F((X \wandto U(Y)) \sepprod X) \xrightarrow{F(\ev)} FU(Y) \xrightarrow{\epsilon} Y
|
||||||
|
\stopformula
|
||||||
|
where $p^{-1}$ is from \in{Theorem}[thm:monoidal] and $\ev$ is the evaluation map of the exponent $\wandto$.
|
||||||
|
\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
|
||||||
|
|
||||||
|
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 \cite[BojanczykKL14], 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].}
|
||||||
|
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[->]
|
||||||
|
(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:
|
||||||
|
\todo{Chain of one-to-one correspondences}.
|
||||||
|
\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 $\mathcal{A}_* = (Q, \delta \circ i, o, q_0)$.
|
||||||
|
\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
|
||||||
|
|
||||||
|
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 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
|
||||||
|
|
@ -18,8 +18,9 @@
|
||||||
|
|
||||||
% The dblp database ignores Pauls nice a-breve and s-comma
|
% The dblp database ignores Pauls nice a-breve and s-comma
|
||||||
\btxremapauthor [Paul Fiterau{-}Brostean] [Paul Fiterău-Broștean]
|
\btxremapauthor [Paul Fiterau{-}Brostean] [Paul Fiterău-Broștean]
|
||||||
\btxremapauthor [Michal Szynwelski] [Micha\l{} Szynwelski]
|
% These two don't work well...
|
||||||
\btxremapauthor [Slawomir Lasota] [S\l{}awomir Lasota]
|
%\btxremapauthor [Michal Szynwelski] [Micha\l{} Szynwelski]
|
||||||
|
%\btxremapauthor [Slawomir Lasota] [S\l{}awomir Lasota]
|
||||||
\btxremapauthor [Eryk Kopczynski] [Eryk Kopczy\'nski]
|
\btxremapauthor [Eryk Kopczynski] [Eryk Kopczy\'nski]
|
||||||
\btxremapauthor [Adenilso da Silva Simão] [Adenilso Simão]
|
\btxremapauthor [Adenilso da Silva Simão] [Adenilso Simão]
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -70,4 +70,38 @@
|
||||||
% language extension
|
% language extension
|
||||||
\define\Lext{{\cdot}}
|
\define\Lext{{\cdot}}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
\define\Put{\kw{Put}}
|
||||||
|
\define\Pop{\kw{Pop}}
|
||||||
|
\define\Null{\kw{Null}}
|
||||||
|
|
||||||
|
\define\perm{\text{\ss Pm}}
|
||||||
|
\define\sb{\text{\ss Sb}}
|
||||||
|
|
||||||
|
\define\MSet{{M\text{-}{Set}}}
|
||||||
|
\define\MNom{{M\text{-}{Nom}}}
|
||||||
|
\define\permset{{\perm\text{-}{Set}}}
|
||||||
|
\define\permnom{{\perm\text{-}{Nom}}}
|
||||||
|
\define\sbset{{\sb\text{-}{Set}}}
|
||||||
|
\define\sbnom{{\sb\text{-}{Nom}}}
|
||||||
|
|
||||||
|
\define\sepprod{\mathbin{\,\ast\,}}
|
||||||
|
\define\wandtob{{{-}\!\!{-}\!\!\ast}}
|
||||||
|
\define\wandto{\mathrel{\wandtob}}
|
||||||
|
\define\separated{\mathrel{\#}}
|
||||||
|
|
||||||
|
\define\pow{\mathcal{P}}
|
||||||
|
|
||||||
|
\define\fsto{\mathrel{{\to}_{\text{\rm fs}}}}
|
||||||
|
\define\sbto{\mathrel{{\to}_{\text{\rm fs}}^{\sb}}}
|
||||||
|
\define\permto{\mathrel{{\to}_{\text{\rm fs}}^{\perm}}}
|
||||||
|
\define\mto{\mathrel{{\to}_{\text{\rm fs}}^{M}}}
|
||||||
|
|
||||||
|
\define\sa{B_*}
|
||||||
|
|
||||||
|
\define\dom{dom}
|
||||||
|
\define\ev{ev}
|
||||||
|
\define\bot{{\perp}}
|
||||||
|
|
||||||
\stopenvironment
|
\stopenvironment
|
||||||
|
|
|
||||||
Reference in a new issue