From 4a7c1865b201a32769ed1f7e6bf428af713eb0fd Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 1 Oct 2018 11:12:57 +0200 Subject: [PATCH] Added the ordered nominal sets chapter --- content.tex | 2 +- content/ordered-nominal-sets.tex | 923 +++++++++++++++++++++++++++++++ environment.tex | 3 +- environment/notation.tex | 9 +- 4 files changed, 934 insertions(+), 3 deletions(-) create mode 100644 content/ordered-nominal-sets.tex diff --git a/content.tex b/content.tex index 68d2707..bef6bdb 100644 --- a/content.tex +++ b/content.tex @@ -15,7 +15,7 @@ \component content/applying-automata-learning \component content/minimal-separating-sequences \component content/learning-nominal-automata -\chapter{Ordered Nominal Sets} +\component content/ordered-nominal-sets \chapter{Succinct Nominal Automata?} \title{References} diff --git a/content/ordered-nominal-sets.tex b/content/ordered-nominal-sets.tex new file mode 100644 index 0000000..53aa7aa --- /dev/null +++ b/content/ordered-nominal-sets.tex @@ -0,0 +1,923 @@ +\project thesis +\startcomponent ordered-nominal-sets + +\startchapter + [title={Fast Computations on Ordered Nominal Sets}, + reference=chap:ordered-nominal-sets] + +\todo{Auteurs en moet ik ook support noemen van de andere auteurs? Keywords?} + +\startabstract +We show how to compute efficiently with nominal sets over the total order symmetry, by developing a direct representation of such nominal sets and basic constructions thereon. +In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis. +The approach is implemented as the library \ONS{} (Ordered Nominal Sets). + +Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets. +We evaluate \ONS{} in two applications: +minimisation of automata and active automata learning. +In both cases, \ONS{} is competitive compared to existing implementations and outperforms them for certain classes of inputs. +\stopabstract + + +\startsection + [title={Introduction}] + +Automata over infinite alphabets are natural models for programs with unbounded data domains. +Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[bojanczyk2014automata, DAntoniV17, DBLP:journals/corr/abs-1209-0680, KaminskiF94, MontanariP97, Segoufin06] and references therein). +Typical infinite alphabets include sequence numbers, timestamps, and identifiers. +This means one can model data flow in such automata beside the basic control flow provided by ordinary automata. +Recently, it has been shown in a series of papers that such models are amenable to learning \citep[AartsFKV15, BolligHLM13, CasselHJS16, DrewsD17, moerman2017learning, Vaandrager17] with the verification of (closed source) TCP implementations by \citet[Fiterau-Brostean16] as a prominent example. + +A foundational approach to infinite alphabets is provided by the notion of \emph{nominal set}, originally introduced in computer science as an elegant formalism for name binding \citep[GabbayP02, pitts2016nominal]. +Nominal sets have been used in a variety of applications in semantics, computation, and concurrency theory (see \citenp[pitts2013nominal] for an overview). +\citet[bojanczyk2014automata] introduce \emph{nominal automata}, which allow one to model languages over infinite alphabets with different symmetries. +Their results are parametric in the structure of the data values. +Important examples of data domains are ordered data values (e.g., timestamps) and data values that can only be compared for equality (e.g., identifiers). +In both data domains, nominal automata and register automata are equally expressive \citep[bojanczyk2014automata]. + +Important for applications of nominal sets and automata are implementations. +A couple of tools exist to compute with nominal sets. +Notably, \NLambda{} \citep[EPTCS207.3] and \LOIS{} \citep[kopczynski1716, kopczynski2017] provide a general purpose programming language to manipulate infinite sets. +\footnote{Other implementations of nominal techniques that are less directly related to our setting (Mihda, Fresh OCaml, and Nominal Isabelle) are discussed in \in{Section}[sec:related].} +Both tools are based on SMT solvers and use logical formulas to represent the infinite sets. +These implementations are very flexible, and the SMT solver does most of the heavy lifting, which makes the implementations themselves relatively straightforward. +Unfortunately, this comes at a cost as SMT solving is in general {\sc Pspace}-hard. +Since the formulas used to describe sets tend to grow as more calculations are done, running times can become unpredictable. + +In the current paper, we use a direct representation, based on symmetries and orbits, to represent nominal sets. +We focus on the \emph{total order symmetry}, where data values are rational numbers and can be compared for their order. +Nominal automata over the total order symmetry are more expressive than automata over the equality symmetry (i.e., traditional register automata of \citenp[KaminskiF94]). +A key insight is that the representation of nominal sets from \citet[bojanczyk2014automata] becomes rather simple in the total order symmetry; each orbit is presented solely by a natural number, intuitively representing the number of variables or registers. + +Our main contributions include the following. +\startitemize +\item +We develop the \emph{representation theory} of nominal sets over the total order symmetry. +We give concrete representations of nominal sets, their products, and equivariant maps. +\item +We provide \emph{time complexity bounds} for operations on nominal sets such as intersections and membership. +Using those results we give the time complexity of Moore's minimisation algorithm (generalised to nominal automata) and prove that it is polynomial in the number of orbits. +\item +Using the representation theory, we are able to \emph{implement nominal sets in a C++ library} \ONS{}. +The library includes all the results from the representation theory (sets, products, and maps). +\item +We \emph{evaluate the performance} of \ONS{} and compare it to \NLambda{} and \LOIS{}, using two algorithms on nominal automata: +minimisation \citep[BojanczykL12] and automata learning \citep[moerman2017learning]. +We use randomly generated automata as well as concrete, logically structured models such as FIFO queues. +For random automata, our methods are drastically faster than the other tools. +On the other hand, \LOIS{} and \NLambda{} are faster in minimising the structured automata as they exploit their logical structure. +In automata learning, the logical structure is not available a-priori, and \ONS{} is faster in most cases. +\stopitemize + +The structure of the paper is as follows. +\in{Section}[sec:nomsets] contains background on nominal sets and their representation. +\in{Section}[sec:total-order] describes the concrete representation of nominal sets, equivariant maps and products in the total order symmetry. +\in{Section}[sec:impl] describes the implementation \ONS{} with complexity results, and \in{Section}[sec:appl] the evaluation of \ONS{} on algorithms for nominal automata. +Related work is discussed in \in{Section}[sec:related], and future work in \in{Section}[sec:fw]. + + +\stopsection +\startsection + [title={Nominal sets}, + reference=sec:nomsets] + +Nominal sets are infinite sets that carry certain symmetries, allowing a finite representation in many interesting cases. +We recall their formalisation in terms of group actions, following \citet[bojanczyk2014automata, pitts2013nominal], to which we refer for an extensive introduction. + + +\startsubsubsection + [title={Group actions.}] + +Let $G$ be a group and $X$ be a set. +A \emph{(right) $G$-action} is a function ${\cdot} \colon X \times G \to X$ satisfying $x \cdot 1 = x$ and $(x \cdot g) \cdot h = x \cdot (g h)$ for all $x \in X$ and $g, h \in G$. +A set $X$ with a $G$-action is called a \emph{$G$-set} and we often write $xg$ instead of $x \cdot g$. +The \emph{orbit} of an element $x \in X$ is the set $\{xg \mid g \in G\}$. +A $G$-set is always a disjoint union of its orbits (in other words, the orbits partition the set). +We say that $X$ is \emph{orbit-finite} if it has finitely many orbits, and we denote the number of orbits by $N(X)$. + +A map $f \colon X \to Y$ between $G$-sets is called \emph{equivariant} if it preserves the group action, i.e., for all $x\in X$ and $g \in G$ we have $f(x)g = f(xg)$. +If an equivariant map $f$ is bijective, then $f$ is an \emph{isomorphism} and we write $X \cong Y$. +A subset $Y\subseteq X$ is equivariant if the corresponding inclusion map is equivariant. +The \emph{product} of two $G$-sets $X$ and $Y$ is given by the Cartesian +product $X \times Y$ with the pointwise group action on it, i.e., $(x,y)g = (xg,yg)$. +Union and intersection of $X$ and $Y$ are well-defined if the two +actions agree on their common elements. + + +\stopsubsubsection +\startsubsubsection + [title={Nominal sets.}] + +A \emph{data symmetry} is a pair $(\mathcal{D},G)$ where $\mathcal{D}$ is a set and $G$ is a subgroup of $\Sym(\mathcal{D})$, the group of bijections on $\mathcal{D}$. +Note that the group $G$ naturally acts on $\mathcal{D}$ by defining $x g = g(x)$. +In the most studied instance, called the \emph{equality symmetry}, $\mathcal{D}$ is a countably infinite set and $G = \Sym(\mathcal{D})$. +In this paper, we will mostly focus on the \emph{total order symmetry} given by $\mathcal{D} = \Q$ and $G = \{\pi \mid \pi \in \Sym(\Q), \pi \text{ is monotone}\}$. + +Let $(\mathcal{D}, G)$ be a data symmetry and $X$ be a $G$-set. +A set of data values $S\subseteq \mathcal{D}$ is called a \emph{support} of an element $x \in X$ if for all $g\in G$ with $\forall s \in S: sg = s$ we have $xg = x$. +A $G$-set $X$ is called \emph{nominal} if every element $x\in X$ has a finite support. + +\startexample +We list several examples for the total order symmetry. +The set $\Q^2$ is nominal as each element $(q_1, q_2) \in \Q^2$ has the finite set $\{q_1, q_2\}$ as its support. +The set has the following three orbits: $\{(q_1, q_2) \mid q_1 < q_2\}$, $\{(q_1, q_2) \mid q_1 > q_2\}$ and $\{(q_1, q_2) \mid q_1 = q_2\}$. + +For a set $X$, the set of all subsets of size $n \in \N$ is denoted by $\mathcal{P}_n(X) = \{Y \subseteq X \mid \#Y = n\}$. +The set $\mathcal{P}_n(\Q)$ is a single-orbit nominal set for each $n$, with the action defined by direct image: $Y g = \{ yg \mid y \in Y \}$. +The group of monotone bijections also acts by direct image on the full power set $\mathcal{P}(\Q)$, but this is \emph{not} a nominal set. +For instance, the set $\mathbb{Z} \in \mathcal{P}(\Q)$ of integers has no finite support. +\stopexample + + +If $S \subseteq \mathcal{D}$ is a support of an element $x \in X$, then any set $S' \subseteq \mathcal{D}$ such that $S \subseteq S'$ is also a support of $x$. +A set $S \subseteq \mathcal{D}$ is a \emph{least support} of $x \in X$ if it is a support of $x$ and $S \subseteq S'$ for any support $S'$ of $x$. +The existence of least supports is crucial for representing orbits. +Unfortunately, even when elements have a finite support, in general they do not always have a least support. +A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set +has a least support. Both the equality and the total order symmetry admit least supports. +(See \citep[bojanczyk2014automata] for other (counter)examples of data symmetries admitting least supports.) +Having least supports is useful for a finite representation. + +Given a nominal set $X$, the size of the least support of an element $x \in X$ is denoted by $\dim(x)$, the \emph{dimension} of $x$. +We note that all elements in the orbit of $x$ have the same dimension. +For an orbit-finite nominal set $X$, we define $\dim(X) = \max \{ \dim(x) \mid x \in X \}$. +For a single-orbit set $O$, observe that $\dim(O) = \dim(x)$ where $x$ is any element $x \in O$. + + +\stopsubsubsection +\startsubsection + [title={Representing nominal orbits}, + reference=subsec:nomorbit] + +We represent nominal sets as collections of single orbits. +The finite representation of single orbits is based on the theory of \citet[bojanczyk2014automata], which uses the technical notions of \emph{restriction} and \emph{extension}. +We only briefly report their definitions here. +However, the reader can safely move to the concrete representation theory in \in{Section}[sec:total-order] with only a superficial understanding of \in{Theorem}[representation_tuple] below. + +The \emph{restriction} of an element $\pi \in G$ to a subset $C \subseteq \mathcal{D}$, written as $\pi|_C$, is the restriction of the function $\pi \colon \mathcal{D} \to \mathcal{D}$ to the domain $C$. +The restriction of a group $G$ to a subset $C \subseteq \mathcal{D}$ is defined as $G|_C = \{\pi|_C \mid \pi \in G,\, C \pi = C\}$. +The \emph{extension} of a subgroup $S \le G|_C$ is defined as $\ext_G(S) = \{\pi \in G \mid \pi|_C \in S\}$. +For $C \subseteq \mathcal{D}$ and $S\le G|_C$, define $[C,S]^{ec} = \{\{sg \mid s \in \ext_G(S)\}\mid g\in G\}$, i.e., the set of right cosets of $\ext_G(S)$ in $G$. +Then $[C,S]^{ec}$ is a single-orbit nominal set. + +Using the above, we can formulate the representation theory from \citet[bojanczyk2014automata] that we will use in the current paper. +This gives a finite description for all single-orbit nominal sets $X$, namely a finite set $C$ together with some of its symmetries. + +\starttheorem[reference=representation_tuple] +Let $X$ be a single-orbit nominal set for a data symmetry $(\mathcal{D}, G)$ that admits least supports and let $C \subseteq \mathcal{D}$ be the least support of some element $x \in X$. +Then there exists a subgroup $S \le G|_C$ such that $X \cong [C,S]^{ec}$. +\stoptheorem + +The proof by \citet[bojanczyk2014automata] uses a bit of category theory: +it establishes an equivalence of categories between single-orbit sets and the pairs $(C, S)$. +We will not use the language of category theory much in order to keep the paper self-contained. + + +\stopsubsection +\stopsection +\startsection + [title={Representation in the total order symmetry}, + reference=sec:total-order] + +This section develops a concrete representation of nominal sets over the total order symmetry, as well as their equivariant maps and products. +It is based on the abstract representation theory from \in{Section}[subsec:nomorbit]. +From now on, by \emph{nominal set} we always refer to a nominal set over the total order symmetry. +Hence, our data domain is $\Q$ and we take $G$ to be the group of monotone bijections. + + +\startsubsection + [title={Orbits and nominal sets}, + reference=sec:orbits-and-nominal-set] + +From the representation in \in{Section}[subsec:nomorbit], we find that any single-orbit set $X$ can be represented as a tuple $(C,S)$. +Our first observation is that the finite group of \quote{local symmetries}, $S$, in this representation is always trivial, i.e., $S = I$, where $I = \{1\}$ is the trivial group. +This follows from the following lemma and $S \le G|_C$. + +\startlemma[reference=group_trivial] +For every finite subset $C \subset \Q$, we have $G|_C = I$. +\stoplemma + +Immediately, we see that $(C, S) = (C, I)$, and hence that the orbit is fully represented by the set $C$. +A further consequence of \in{Lemma}[group_trivial] is that each \emph{element} of an orbit can be uniquely identified by its least support. +This leads us to the following characterisation of $[C,I]^{ec}$. +\startlemma[reference=orbitrep] +Given a finite subset $C \subset \Q$, we have $[C,I]^{ec} \cong \mathcal{P}_{\#C}(\Q)$. +\stoplemma + +By \in{Theorem}[representation_tuple] and the above lemmas, we can represent an orbit by a single integer $n$, the size of the least support of its elements. +This naturally extends to (orbit-finite) nominal sets with multiple orbits by using a multiset of natural numbers, representing the size of the least support of each of the orbits. +These multisets are formalised here as functions $f \colon \N \to \N$. + +\startdefinition[reference=def:present-nom] +Given a function $f \colon \N \to \N$, we define a nominal set $[f]^{o}$ by +\startformula +\[f\]^{o} = \bigcup_{\startsubstack n \in \N \NR 1 \le i \le f(n) \stopsubstack} \{i\} \times \mathcal{P}_n(\Q). +\stopformula +\stopdefinition + +\startproposition[reference=thm:pres-nom] +For every orbit-finite nominal set $X$, there is a function $f \colon \N \to \N$ such that $X \cong [f]^{o}$ and the set $\{n \mid f(n) \neq 0\}$ is finite. +Furthermore, the mapping between $X$ and $f$ is one-to-one up to isomorphism of $X$ when restricting to $f \colon \N \to \N$ for which the set $\{n\mid f(n) \ne 0\}$ is finite. +\stopproposition +The presentation in terms of a function $f \colon \N \to \N$ enforces that there are only finitely many orbits of any given dimension. +The first part of the above proposition generalises to arbitrary nominal sets by replacing the codomain of $f$ by the class of all sets and adapting \in{Definition}[def:present-nom] accordingly. +However, the resulting correspondence will no longer be one-to-one. + +As a brief example, let us consider the set $\Q \times \Q$. +The elements $(a, b)$ split in three orbits, one for $a < b$, one for $a = b$ and one for $a > b$. +These have dimension 2, 1 and 2 respectively, so the set $\Q \times \Q$ is represented by the multiset $\{1, 2, 2\}$. + + +\stopsubsection +\startsubsection + [title={Equivariant maps}, + reference=sec:eq-maps] + +We show how to represent equivariant maps, using two basic properties. +Let $f \colon X \to Y$ be an equivariant map. +The first property is that the direct image of an orbit (in $X$) is again an orbit (in $Y$), +that is to say, $f$ is defined \quote{orbit-wise}. +Second, equivariant maps cannot introduce new elements in the support (but they can drop them). +More precisely: + +\startlemma[reference=lem:eqiorbit] +Let $f \colon X \to Y$ be an equivariant map, and $O\subseteq X$ a single orbit. +The direct image $f(O) = \{f(x) \mid x \in O\}$ is a single-orbit nominal set. +\stoplemma + +\startlemma[reference=eqimap_contained] +Let $f \colon X \to Y$ be an equivariant map between two nominal sets $X$ and $Y$. +Let $x\in X$ and let $C$ be a support of $x$. +Then $C$ supports $f(x)$. +\stoplemma + +Hence, equivariant maps are fully determined by associating two pieces of information for each orbit in the domain: +the orbit on which it is mapped and a string denoting which elements of the least support of the input are preserved. +These ingredients are formalised in the first part of the following definition. +The second part describes how these ingredients define an equivariant function. +\in{Proposition}[eqimap_rep] then states that every equivariant function can be described in this way. + +\startdefinition[reference=def:eqmap] +Let $H = \{(I_1, F_1, O_1), \ldots, (I_n, F_n, O_n)\}$ be a finite set of tuples where the $I_i$'s are disjoint single-orbit nominal sets, the $O_i$'s are single-orbit nominal sets with $\dim(O_i) \leq \dim(I_i)$, and the $F_i$'s are bit strings of length $\dim(I_i)$ with exactly $\dim(O_i)$ ones. + +Given a set $H$ as above, we define $f_H \colon \bigcup I_i \to \bigcup O_i$ as the unique equivariant function such that, given $x \in I_i$ with least support $C$, $f_H(x)$ is the unique element of $O_i$ with support $\{C(j) \mid F_i(j) = 1\}$, where $F_i(j)$ is the $j$-th bit of $F_i$ and $C(j)$ is the $j$-th smallest element of $C$. +\stopdefinition + +\startproposition[reference=eqimap_rep] +For every equivariant map $f \colon X \to Y$ between orbit-finite nominal sets $X$ and $Y$ there is a set $H$ as in \in{Definition}[def:eqmap] such that $f = f_H$. +\stopproposition + +Consider the example function $\min \colon \mathcal{P}_3(\Q) \to \Q$ which returns the smallest element of a 3-element set. +Note that both $\mathcal{P}_3(\Q)$ and $\Q$ are single orbits. +Since for the orbit $\mathcal{P}_3(\Q)$ we only keep the smallest element of the support, we can thus represent the function $\min$ with $\{(\mathcal{P}_3(\Q), 100, \Q)\}$. + + +\stopsubsection +\startsubsection + [title={Products}, + reference=subsec:products] + +The product $X \times Y$ of two nominal sets is again a nominal set and hence, it can be represented itself in terms of the dimension of each of its orbits as shown in \in{Section}[sec:orbits-and-nominal-set]. +However, this approach has some disadvantages. + +\startexample[reference=ex:product] +We start by showing that the orbit structure of products can be non-trivial. +Consider the product of $X = \Q$ and the set $Y = \{(a,b) \in \Q^2 \mid a < b\}$. +This product consists of \emph{five} orbits, more than one might naively expect from the fact that both sets are single-orbit: +\startformula\startalign[width=broad] +\NC \{(a,(b,c)) \mid a,b,c \in \Q, a < b < c\}, \NC \quad \{(a,(a,b)) \mid a,b \in \Q, a < b\}, \NR +\NC \{(b,(a,c)) \mid a,b,c \in \Q, a < b < c\}, \NC \quad \{(b,(a,b)) \mid a,b \in \Q, a < b\}, \NR +\NC \{(c,(a,b)) \mid a,b,c \in \Q, a < b < c\}. \NC \NR +\stopalign\stopformula +\stopexample + +We find that this product is represented by the multiset $\{2,2,3,3,3\}$. +Unfortunately, this is not sufficient to accurately describe the product as it abstracts away from the relation between its elements with those in $X$ and $Y$. +In particular, it is not possible to reconstruct the projection maps from such a representation. + +The essence of our representation of products is that each orbit $O$ in the product $X \times Y$ is described entirely by the dimension of $O$ together with the two (equivariant) projections $\pi_1 \colon O \to X$ and $\pi_2 \colon O \to Y$. +This combination of the orbit and the two projection maps can already be represented using \in{Propositions}[thm:pres-nom] and \in{}[eqimap_rep]. +However, as we will see, a combined representation for this has several advantages. +For discussing such a representation, let us first introduce what it means for tuples of a set and two functions to be isomorphic: + +\startdefinition +Given nominal sets $X, Y, Z_1$ and $Z_2$, and equivariant functions $l_1 \colon Z_1 \to X$, $r_1 \colon Z_1 \to Y$, $l_2 \colon Z_2 \to X$ and $r_2 \colon Z_2 \to Y$, we define $(Z_1, l_1, r_1) \cong (Z_2, l_2, r_2)$ if there exists an isomorphism $h \colon Z_1 \to Z_2$ such that $l_1 = l_2 \circ h$ and $r_1 = r_2 \circ h$. +\stopdefinition + +Our goal is to have a representation that, for each orbit $O$, produces a tuple $(A, f_1, f_2)$ isomorphic to the tuple $(O, \pi_1, \pi_2)$. +The next lemma gives a characterisation that can be used to simplify such a representation. + +\startlemma[reference=lm:supp-product] +Let $X$ and $Y$ be nominal sets and $(x, y) \in X \times Y$. +If $C$, $C_x$, and $C_y$ are the least supports of $(x, y)$, $x$, and $y$ respectively, then $C = C_x \cup C_y$. +\stoplemma + +With \in{Proposition}[eqimap_rep] we represent the maps $\pi_1$ and $\pi_2$ by tuples $(O, F_1, O_1)$ and $(O, F_2, O_2)$ respectively. +Using \in{Lemma}[lm:supp-product] and the definitions of $F_1$ and $F_2$, we see that at least one of $F_1(i)$ and $F_2(i)$ equals $1$ for each $i$. + +We can thus combine the strings $F_1$ and $F_2$ into a single string $P \in \{L, R, B\}^{*}$ as follows. +We set $P(i) = L$ when only $F_1(i)$ is $1$, $P(i) = R$ when only $F_2(i)$ is $1$, and $P(i) = B$ when both are $1$. +The string $P$ fully describes the strings $F_1$ and $F_2$. +This process for constructing the string $P$ gives it two useful properties. +The number of $L$s and $B$s in the string gives the size dimension of $O_1$. +Similarly, the number of $R$s and $B$s in the string gives the dimension of $O_2$. +We will call strings with that property \emph{valid}. +In conclusion, to describe a single orbit of the product $X \times Y$, a valid string $P$ together with the images of $\pi_1$ and $\pi_2$ is sufficient. + +\startdefinition[reference=def:orbstringdef] +Let $P \in \{L,R,B\}^{*}$, and $O_1 \subseteq X$, $O_2 \subseteq Y$ be single-orbit sets. Given a tuple $(P, O_1, O_2)$, where the string $P$ is valid, define +\startformula +\[(P,O_1,O_2)\]^t = (\mathcal{P}_{|P|}(\Q), f_{H_1}, f_{H_2}), +\stopformula +where $H_i = \{(\mathcal{P}_{|P|}(\Q), F_i, O_i)\}$ +and the string $F_1$ is defined as the string $P$ with $L$s and $B$s replaced by $1$s and $R$s by $0$s. +The string $F_2$ is similarly defined with the roles of $L$ and $R$ swapped. +\stopdefinition + +\startproposition[reference=orbstring] +There exists a one-to-one correspondence between the orbits $O \subseteq X \times Y$, and tuples $(P, O_1, O_2)$ satisfying $O_1 \subseteq X$, $O_2 \subseteq Y$, and where $P$ is a valid string, such that $[(P,O_1,O_2)]^{t} \cong (O, \pi_1|_O, \pi_2|_O)$. +\stopproposition + +From the above proposition it follows that we can generate the product $X \times Y$ simply by enumerating all valid strings $P$ for all pairs of orbits $(O_1, O_2)$ of $X$ and $Y$. +Given this, we can calculate the multiset representation of a product from the multiset representations of both factors. + +\starttheorem[reference=thm:prod-combinatorics] +For $X \cong [f]^{o}$ and $Y \cong [g]^{o}$ we have $X \times Y \cong [h]^{o}$, where +\startformula +h(n) = \sum_{\startsubstack 0 \le i, j \le n \NR i+j \ge n \stopsubstack} f(i) g(j) {{n}\choose{j}}{{j}\choose{n-i}}. +\stopformula +\todo{choose-notatie klopt niet} +\stoptheorem + +\startexample +To illustrate some aspects of the above representation, let us use it to calculate the product of \in{Example}[ex:product]. +First, we observe that both $\Q$ and $S = \{(a,b) \in \Q^2 \mid a < b\}$ consist of a single orbit. +Hence any orbit of the product corresponds to a triple $(P, \Q, S)$, where the string $P$ satisfies $|P|_L+|P|_B = \dim(\Q) = 1$ and $|P|_R+|P|_B = \dim(S) = 2$. +We can now find the orbits of the product $\Q \times S$ by enumerating all strings satisfying these equations. +This yields: +\startitemize +\item LRR, corresponding to the orbit $\{(a,(b,c)) \mid a,b,c \in \Q, a < b < c\}$, +\item RLR, corresponding to the orbit $\{(b,(a,c)) \mid a,b,c \in \Q, a < b < c\}$, +\item RRL, corresponding to the orbit $\{(c,(a,b)) \mid a,b,c \in \Q, a < b < c\}$, +\item RB, corresponding to the orbit $\{(b,(a,b)) \mid a,b \in \Q, a < b\}$, and +\item BR, corresponding to the orbit $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$. +\stopitemize +Each product string fully describes the corresponding orbit. +To illustrate, consider the string BR. +The corresponding bit strings for the projection functions are $F_1 = 10$ and $F_2 = 11$. +From the lengths of the string we conclude that the dimension of the orbit is $2$. +The string $F_1$ further tells us that the left element of the tuple consists only of the smallest element of the support. +The string $F_2$ indicates that the right element of the tuple is constructed from both elements of the support. +Combining this, we find that the orbit is $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$. +\stopexample + + +\stopsubsection +\startsubsection + [title={Summary}] + +We summarise our concrete representation in the following table. +\in{Propositions}[thm:pres-nom], \in{}[eqimap_rep] and \in{}[orbstring] correspond to the three rows in the table. + +\todo{Table} +% \starttabular}{l|p{5.7cm} +% \emph{Object} & \emph{Representation} \\ +% \hline +% Single orbit $O$ & Natural number $n = \dim(O)$ \\ +% Nominal set $X = \bigcup_i O_i$ & Multiset of these numbers \\ +% \hline +% Map from single orbit $f \colon O \to Y$ & The orbit $f(O)$ and a bit string $F$ \\ +% Equivariant map $f \colon X \to Y$ & Set of tuples $(O, F, f(O))$, one for each orbit \\ +% \hline +% Orbit in a product $O \subseteq X \times Y$ & The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports \\ +% Product $X \times Y$ & Set of tuples $(P, O_X, O_Y)$, one for each orbit \\ +% \stoptabular + +Notice that in the case of maps and products, the orbits are inductively represented using the concrete representation. +As a base case we can represent single orbits by their dimension. + + +\stopsubsection +\stopsection +\startsection + [title={Implementation and Complexity of ONS}, + reference=sec:impl] + +The ideas outlined above have been implemented in the \cpp{} library \ONS{} +\footnote{\ONS{} can be found at \todo{https://github.com/davidv1992/ONS}.} +The library can represent orbit-finite nominal sets and their products, (disjoint) unions, and maps. +A full description of the possibilities is given in the documentation included with \ONS{}. + +As an example, the following program computes the product from \in{Example}[ex:product]. +Initially, the program creates the nominal set $A$, containing the entirety of $\Q$. +Then it creates a nominal set $B$, such that it consists of the orbit containing the element $(1,2) \in \Q \times \Q$. +For this, the library determines to which orbit of the product $\Q \times \Q$ the element $(1,2)$ belongs, and then stores a description of the orbit as described in \in{Section}[sec:total-order]. +Note that this means that it internally never needs to store the element used to create the orbit. +The function \kw{nomset_product} then uses the enumeration of product strings mentioned in \in{Section}[subsec:products] to calculate the product of $A$ and $B$. +Finally, it prints a representative element for each of the orbits in the product. +These elements are constructed based on the description of the orbits stored, filled in to make their support equal to sets of the form $\{1, 2, \ldots, n\}$. + +\todo{Linenumbering} + +\starttyping +nomset A = nomset_rationals(); +nomset> B({rational(1),rational(2)}); + +auto AtimesB = nomset_product(A, B); // compute the product +for (auto orbit : AtimesB) + cout << orbit.getElement() << " "; +\stoptyping + +\noindent +Running this gives the following output +(where {\tt /1} signifies the denominator): + +\starttyping +(1/1,(2/1,3/1)) (1/1,(1/1,2/1)) (2/1,(1/1,3/1)) +(2/1,(1/1,2/1)) (3/1,(1/1,2/1)) +\stoptyping + +Internally, \kw{orbit} is implemented following the theory presented in \in{Section}[sec:total-order], storing the dimension of the orbit it represents. +It also contains sufficient information to reconstruct elements given their least support, such as the product string for orbits resulting from a product. +The class \kw{nomset} then uses a standard set data structure to store the collection of orbits contained in the nominal set it represents. + +In a similar way, \kw{eqimap} stores equivariant maps by associating each orbit in the domain with the image orbit and the string representing which of the least support to keep. +This is stored using a map data structure. +For both nominal sets and equivariant maps, the underlying data structure is currently implemented using trees. + + +\startsubsection + [title={Complexity of operations}] + +Using the concrete representation of nominal sets, we can determine the complexity of common operations. +To simplify such an analysis, we will make the following assumptions: +\startitemize +\item The comparison of two orbits takes $O(1)$. +\item Constructing an orbit from an element takes $O(1)$. +\item Checking whether an element is in an orbit takes $O(1)$. +\stopitemize +These assumptions are justified as each of these operations takes time proportional to the size of the representation of an individual orbit, which in practice is small and approximately constant. +For instance, the orbit $\mathcal{P}_n(\Q)$ is represented by just the integer $n$ and its type. + +\starttheorem[reference=thmcomplexity] +If nominal sets are implemented with a tree-based set structure (as in \ONS{}), the complexity of the following set operations is as follows. +Recall that $\Nsize(X)$ denotes the number of orbits of $X$. +We use $p$ and $f$ to denote functions implemented in whatever way the user wants, which we assume to take $O(1)$ time. +The software assumes these are equivariant, but this is not verified. + +\todo{Table} +% \startcenter +% \starttabular}{r|l +% Operation & Complexity\\ +% \hline +% Test $x \in X$ & $O(\log \Nsize(X))$\\ +% Test $X\subseteq Y$ & $O(\min(\Nsize(X)+\Nsize(Y), \Nsize(X)\log \Nsize(Y)))$\\ +% Calculate $X \cup Y$ & $O(\Nsize(X)+\Nsize(Y))$\\ +% Calculate $X \cap Y$ & $O(\Nsize(X)+\Nsize(Y))$\\ +% Calculate $\{x \in X \mid p(x)\}$ & $O(\Nsize(X))$\\ +% Calculate $\{f(x) \mid x \in X\}$ & $O(\Nsize(X)\log \Nsize(X))$\\ +% Calculate $X\times Y$ & $O(\Nsize(X\times Y)) \,\subseteq\, O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$\\ +% \stoptabular +% \stopcenter +\stoptheorem + +\startproof +Since most parts are proven similarly, we only include proofs for the first and last item. + +\emph{Membership.} +To decide $x \in X$, we first construct the orbit containing $x$, which is done in constant time. +Then we use a logarithmic lookup to decide whether this orbit is in our set data structure. +Hence, membership checking is $O(\log(\Nsize(X)))$. + +\emph{Products.} +Calculating the product of two nominal sets is the most complicated construction. +For each pair of orbits in the original sets $X$ and $Y$, all product orbits need to be generated. +Each product orbit itself is constructed in constant time. +By generating these orbits in-order, the resulting set takes $O(\Nsize(X \times Y))$ time to construct. + +We can also give an explicit upper bound for the number of orbits in terms of the input. +Recall that orbits in a product are represented by strings of length at most $\dim(X)+\dim(Y)$. +(If the string is shorter, we pad it with one of the symbols.) +Since there are three symbols ($L, R$ and $B$), the product of $X$ and $Y$ will have at most $3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y)$ orbits. +It follows that taking products has time complexity of $O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$. +\stopproof + + +\stopsubsection +\stopsection +\startsection + [title={Results and evaluation in automata theory}, + reference=sec:appl] + +In this section we consider applications of nominal sets to automata theory. +As mentioned in the introduction, nominal sets are used to formalise languages over infinite alphabets. +These languages naturally arise as the semantics of register automata. +The definition of register automata is not as simple as that of ordinary finite automata. +Consequently, transferring results from automata theory to this setting often requires non-trivial proofs. +Nominal automata, instead, are defined as ordinary automata by replacing finite sets with orbit-finite nominal sets. +The theory of nominal automata is developed by \citet[bojanczyk2014automata] and it is shown that many, but not all, algorithms from automata theory transfer to nominal automata. + +As an example we consider the following language on rational numbers: +\startformula +\Lint = \{ a_1 b_1 \cdots a_n b_n \mid a_i, b_i \in \Q, a_i < a_{i+1} < b_{i+1} < b_i \text{ for all } i \}. +\stopformula +We call this language the \emph{interval language} as a word $w \in \Q^{\ast}$ is in the language when it denotes a sequence of nested intervals. +This language contains arbitrarily long words. +For this language it is crucial to work with an infinite alphabet as for each finite set $C \subset \Q$, the restriction $\Lint \cap C^{\ast}$ is just a finite language. +Note that the language is equivariant: $w \in \Lint \iff wg \in \Lint$ for any monotone bijection $g$, because nested intervals are preserved by monotone maps. +\footnote{The $G$-action on words is defined point-wise: $(w_1 \ldots w_n) g = (w_1 g) \ldots (w_n g)$.} +Indeed, $\Lint$ is a nominal set, although it is not orbit-finite. + +Informally, the language $\Lint$ can be accepted by the automaton depicted in \in{Figure}[fig:lint-minimal]. +Here we allow the automaton to store rational numbers and compare them to new symbols. +For example, the transition from $q_2$ to $q_3$ is taken if any value $c$ between $a$ and $b$ is read and then the currently stored value $a$ is replaced by $c$. +For any other value read at state $q_2$ the automaton transitions to the sink state $q_4$. +Such a transition structure is made precise by the notion of nominal automata. + +\startplacefigure + [title={Example automaton that accepts the language $\Lint$.}, + reference=fig:lint-minimal] +\todo{Plaatje} +% \starttikzpicture +% \node (S 0) at (0,0) [state, minimum size=1.5cm] {$q_0$}; +% \node (S 1) at (3,0) [state, minimum size=1.5cm] {$q_1(a)$}; +% \node (S 2) at (7,0) [state, minimum size=1.5cm, accepting] {$q_2(a,b)$}; +% \node (S 3) at (11,0) [state, minimum size=1.5cm] {$q_3(a,b)$}; +% \node (S 4) at (7,-2.5) [state, minimum size=1.5cm] {$q_4$}; +% \node (S 5) at (11,-2.5) [state,minimum size=1.5cm,draw=none] {}; + +% \path +% (S 0) edge node[above] {$a$} (S 1) +% (S 1) edge node[above] {$b > a$} (S 2) +% (S 1) edge[bend right] node[below left] {$b \le a$} (S 4) +% (S 2) edge[bend left=10] node[above,align=center] {$a 60$m \\ +% rand$_{15,1}$ (x10) & $15$ & n/a & $0.04$s & \color{black!70} n/a & $1$m $27$s & $10$m $20$s \\ +% rand$_{15,2}$ (x10) & $15$ & n/a & $0.11$s & \color{black!70} n/a & $55$m $46$s & $> 60$m \\ +% rand$_{15,3}$ (x10) & $15$ & n/a & $0.46$s & \color{black!70} n/a & $> 60$m & $> 60$m \\ +% \hline +% FIFO($2$) & $13$ & $6$ & $0.01$s & \color{black!70} $0.01$s & $1.37$s & $0.24$s \\ +% FIFO($3$) & $65$ & $19$ & $0.38$s & \color{black!70} $0.09$s & $11.59$s & $2.4$s \\ +% FIFO($4$) & $440$ & $94$ & $39.11$s & \color{black!70} $1.60$s & $1$m $16$s & $14.95$s \\ +% FIFO($5$) & $3686$ & $635$ & $> 60$m & \color{black!70} $39.78$s & $6$m $42$s & $1$m $11$s \\ +% \hline +% $ww(2)$ & $8$ & $8$ & $0.00$s & \color{black!70} $0.00$s & $0.14$s & $0.03$s \\ +% $ww(3)$ & $24$ & $24$ & $0.19$s & \color{black!70} $0.02$s & $0.88$s & $0.16$s \\ +% $ww(4)$ & $112$ & $112$ & $26.44$s & \color{black!70} $0.25$s & $3.41$s & $0.61$s \\ +% $ww(5)$ & $728$ & $728$ & $> 60$m & \color{black!70} $6.37$s & $10.54$s & $1.80$s \\ +% \hline +% $\Lmax$ & $5$ & $3$ & $0.00$s & \color{black!70} $0.00$s & $2.06$s & $0.03$s \\ +% $\Lint$ & $5$ & $5$ & $0.00$s & \color{black!70} $0.00$s & $1.55$s & $0.03$s +% \stoptabular +% \caption{Running times for \in{Algorithm}[alg:moore] implemented in the three libraries. +% $N(S)$ is the size of the input and $N(S^\text{min})$ the size of the minimal automaton. +% For \ONS{}, the time used to generate the automaton is reported separately (in grey).} +% \label{minimize_results} +% \stoptable + +The results for structured automata show a clear effect of the extra structure. +Both \NLambda{} and \LOIS{} remain capable of minimising the automata in reasonable amounts of time for larger sizes. +In contrast, \ONS{} benefits little from the extra structure. +Despite this, it remains viable: even for the larger cases it falls behind significantly only for the largest FIFO automaton and the two largest $ww$ automata. + + +\stopsubsubsection +\stopsubsection +\startsubsection + [title={Learning nominal automata}] + +Another application that we implemented in \ONS{} is \emph{automata learning}. +The aim of automata learning is to infer an unknown regular language $\lang$. +We use the framework of active learning as set up by \citet[Angluin87] +where a learning algorithm can query an oracle to gather information about $\lang$. +Formally, the oracle can answer two types of queries: +\startitemize +\item \emph{membership queries}, where a query consists of a word $w \in A^{*}$ and the oracle replies whether $w \in \lang$, and +\item \emph{equivalence queries}, where a query consists of an automaton $\mathcal{H}$ and the oracle replies positively if $\lang(\mathcal{H}) = \lang$ or provides a counterexample if $\lang(\mathcal{H}) \neq \lang$. +\stopitemize +With these queries, the \LStar{} algorithm can learn regular languages efficiently \citep[Angluin87]. +In particular, it learns the unique minimal automaton for $\lang$ using only finitely many queries. +The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages \citep[moerman2017learning]. +In particular, it learns a nominal DFA (over an infinite alphabet) using only finitely many queries. +We implement \nLStar{} in the presented library and compare it to its previous implementation in \NLambda{}. +The algorithm is not polynomial, unlike the minimisation algorithm described above. +However, the authors conjecture that there is a polynomial algorithm. +\footnote{See \todo{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.} +For the correctness, termination, and comparison with other learning algorithms see \citep[moerman2017learning]. + + +\startsubsubsection + [title={Implementations.}] + +Both implementations in \NLambda{} and \ONS{} are direct implementations of the pseudocode for \nLStar{} with no further optimisations. +The authors of \LOIS{} implemented \nLStar{} in their library as well. +\footnote{Can be found on \todo{github.com/eryxcc/lois/blob/master/tests/learning.cpp}.} +They reported similar performance as the implementation in \NLambda{} (private communication). +Hence we focus our comparison on \NLambda{} and \ONS{}. +We use the variant of \nLStar{} where counterexamples are added as columns instead of prefixes. + +The implementation in \NLambda{} has the benefit that it can work with different symmetries. +Indeed, the structured examples, FIFO and $ww$, are equivariant w.r.t. the equality symmetry as well as the total order symmetry. +For that reason, we run the \NLambda{} implementation using both the equality symmetry and the total order symmetry on those languages. +For the languages $\Lmax$, $\Lint$ and the random automata, we can only use the total order symmetry. + +To run the \nLStar{} algorithm, we implement an external oracle for the membership queries. +This is akin to the application of learning black box systems \citep[Vaandrager17]. +For equivalence queries, we constructed counterexamples by hand. +All implementations receive the same counterexamples. +We measure CPU time instead of real time, so that we do not account for the external oracle. + + +\stopsubsubsection +\startsubsubsection + [title={Results.}] + +The results (\in{Table}[learning_results]) for random automata show an advantage for \ONS{}. +Additionally, we report the number of membership queries, +which can vary for each implementation as some steps in the algorithm depend on the internal ordering of set data structures. + +In contrast to the case of minimisation, +the results suggest that \NLambda{} cannot exploit the logical structure of FIFO$(n)$, $\Lmax$ and $\Lint$ as it is not provided a priori. +For $ww(2)$ we inspected the output on \NLambda{} and saw that it learned some logical structure (e.g., it outputs $\{ (a, b) \mid a \neq b \}$ as a single object instead of two orbits $\{ (a, b) \mid a < b \}$ and $\{ (a, b) \mid b < a \}$). +This may explain why \NLambda{} is still competitive. +For languages which are equivariant for the equality symmetry, the \NLambda{} implementation using the equality symmetry can learn with much fewer queries. +This is expected as the automata themselves have fewer orbits. +It is interesting to see that these languages can be learned more efficiently by choosing the right symmetry. + +\todo{Table} +% \starttable +% \centering +% \starttabular}{l l l|r r|r r|r r +% & & & \multicolumn{2}{l|}{\ONS{}} & \multicolumn{2}{l|}{\NLambda{}$^{\mathit{ord}}$} & \multicolumn{2}{l}{\NLambda{}$^{\mathit{eq}}$} \\ +% Model & $\Nsize(S)$ & $\dim(S)$ & time & MQs & time & MQs & time& MQs \\ +% \hline +% rand$_{5,1}$ & $4$ & $1$ & $2$m $7$s & $2321$ & $39$m $51$s & $1243$ & & \\ +% rand$_{5,1}$ & $5$ & $1$ & $0.12$s & $404$ & $40$m $34$s & $435$ & & \\ +% rand$_{5,1}$ & $3$ & $0$ & $0.86$s & $499$ & $30$m $19$s & $422$ & & \\ +% rand$_{5,1}$ & $5$ & $1$ & $> 60$m & n/a & $> 60$m & n/a & & \\ +% rand$_{5,1}$ & $4$ & $1$ & $0.08$s & $387$ & $34$m $57$s & $387$ & & \\ +% \hline +% FIFO$(1)$ & $3$ & $1$ & $0.04$s & $119$ & $3.17$s & $119$ & $1.76$s & $51$ \\ +% FIFO$(2)$ & $6$ & $2$ & $1.73$s & $2655$ & $6$m $32$s & $3818$ & $40.00$s & $434$ \\ +% FIFO$(3)$ & $19$ & $3$ & $46$m $34$s & $298400$ & $> 60$m & n/a & $34$m $7$s & $8151$ \\ +% \hline +% $ww(1)$ & $4$ & $1$ & $0.42$s & $134$ & $2.49$s & $77$ & $1.47$s & $30$ \\ +% $ww(2)$ & $8$ & $2$ & $4$m $26$s & $3671$ & $3$m $48$s & $2140$ & $30.58$s & $237$ \\ +% $ww(3)$ & $24$ & $3$ & $> 60$m & n/a & $> 60$m & n/a & $> 60$m & n/a \\ +% \hline +% $\Lmax$ & $3$ & $1$ & $0.01$s & $54$ & $3.58$s & $54$ & & \\ +% $\Lint$ & $5$ & $2$ & $0.59$s & $478$ & $1$m $23$s & $478$ & & +% \stoptabular +% \caption{Running times and number of membership queries for the \nLStar{} algorithm. For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.} +% \label{learning_results} +% \stoptable + + +\stopsubsubsection +\stopsubsection +\stopsection +\startsection + [title={Related work}, + reference=sec:related] + +As stated in the introduction, \NLambda{} by \citet[EPTCS207.3] and \LOIS{} by \citet[kopczynski1716] use first-order formulas to represent nominal sets and use SMT solvers to manipulate them. +This makes both libraries very flexible and they indeed implement the equality symmetry as well as the total order symmetry. +As their representation is not unique, the efficiency depends on how the logical formulas are constructed. +As such, they do not provide complexity results. +In contrast, our direct representation allows for complexity results (\in{Section}[sec:impl]) and leads to different performance characteristics (\in{Section}[sec:appl]). + +A second big difference is that both \NLambda{} and \LOIS{} implement a \quotation{programming paradigm} instead of just a library. +This means that they overload natural programming constructs in their host languages (\haskell{} and \cpp{} respectively). +For programmers this means they can think of infinite sets without having to know about nominal sets. + +It is worth mentioning that an older (unreleased) version of \NLambda{} implemented nominal sets with orbits instead of SMT solvers \citep[towardsnominal]. +However, instead of characterising orbits (e.g., by its dimension), they represent orbits by a representative element. +The authors of \NLambda{} have reported that the current version is faster \citep[EPTCS207.3]. + +The theoretical foundation of our work is the main representation theorem in \citep[bojanczyk2014automata]. +We improve on that by instantiating it to the total order symmetry and distil a concrete representation of nominal sets. +As far as we know, we provide the first implementation of the representation theory in \citep[bojanczyk2014automata]. + +Another tool using nominal sets is Mihda \citep[ferrari2005]. +Here, only the equality symmetry is implemented. +This tool implements a translation from $\pi$-calculus to history-dependent automata (HD-automata) with the aim of minimisation and checking bisimilarity. +The implementation in OCaml is based on \emph{named sets}, which are finite representations for nominal sets. +The theory of named sets is well-studied and has been used to model various behavioural models with local names. +For those results, the categorical equivalences between named sets, nominal sets and a certain (pre)sheaf category have been exploited \citep[CianciaKM10, CianciaM10]. +The total order symmetry is not mentioned in their work. +We do, however, believe that similar equivalences between categories can be stated. +Interestingly, the product of named sets is similar to our representation of products of nominal sets: pairs of elements together with data which denotes the relation between data values. + +Fresh OCaml by \citet[shinwell2005fresh] and Nominal Isabelle by \citet[urban2005nominal] are +both specialised in name-binding and $\alpha$-conversion used in proof systems. +They only use the equality symmetry and do not provide a library for manipulating nominal sets. +Hence they are not suited for our applications. + +On the theoretical side, there are many complexity results for register automata \citep[DBLP:journals/corr/abs-1209-0680, DBLP:conf/lics/MurawskiRT15]. +In particular, we note that problems such as emptiness and equivalence are NP-hard depending on the type of register automaton. +This does not easily compare to our complexity results for minimisation. +One difference is that we use the total order symmetry, where the local symmetries are always trivial (\in{Lemma}[group_trivial]). +As a consequence, all the complexity required to deal with groups vanishes. +Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry. +Another difference is that register automata allow for duplicate values in the registers. +In nominal automata, such configurations will be encoded in different orbits. +An interesting open problem is whether equivalence of unique-valued register automata is in {\sc Ptime} \citep[DBLP:conf/lics/MurawskiRT15]. + +Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DAntoniV17, maler2017generic]. +These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries. +Symbolic automata are finite state (as opposed to infinite state nominal automata) and do not allow for storing values. +However, they do allow for general predicates over an infinite alphabet, including comparison to constants. + + +\stopsection +\startsection + [title={Conclusion and Future Work}, + reference=sec:fw] + +We presented a concrete finite representation for nominal sets over the total order symmetry. +This allowed us to implement a library, \ONS{}, and provide complexity bounds for common operations. +The experimental comparison of \ONS{} against existing solutions for automata minimisation and +learning show that our implementation is much faster in many instances. +As such, we believe \ONS{} is a promising implementation of nominal techniques. + +A natural direction for future work is to consider other symmetries, such as the equality symmetry. +Here, we may take inspiration from existing tools such as Mihda (see \in{Section}[sec:related]). +Another interesting question is whether it is possible to translate a nominal automaton over the total order symmetry which accepts an equality language to an automaton over the equality symmetry. +This would allow one to efficiently move between symmetries. +Finally, our techniques can potentially be applied to timed automata by exploiting the intriguing connection between the nominal automata that we consider and timed automata \citep[BojanczykL12]. + + +\stopsection +\startsubject + [title={Acknowledgement}] + +We would like to thank Szymon Toru\'{n}czyk and Eryk Kopczy\'{n}ski for their prompt help when using the \LOIS{} library. +For general comments and suggestions we would like to thank Ugo Montanari and Niels van der Weide. +At last, we want to thank the anonymous reviewers for their comments. + +\stopsubject +\referencesifcomponent +\stopchapter +\stopcomponent \ No newline at end of file diff --git a/environment.tex b/environment.tex index 9b2404e..2c23f94 100644 --- a/environment.tex +++ b/environment.tex @@ -22,9 +22,10 @@ \defineenumeration[definition][text=Definition] \defineenumeration[example][text=Example] \defineenumeration[lemma][text=Lemma] +\defineenumeration[proposition][text=Proposition] \defineenumeration[theorem][text=Theorem] \defineenumeration[corollary][text=Corollary] -\setupenumeration[definition,example,lemma,theorem,corollary][alternative=serried,width=fit,right=.] +\setupenumeration[definition,example,lemma,proposition,theorem,corollary][alternative=serried,width=fit,right=.] \definestartstop[proof][before={{\it Proof. }}, after={\hfill$\square$}] diff --git a/environment/notation.tex b/environment/notation.tex index 6d37e77..f5cd1cf 100644 --- a/environment/notation.tex +++ b/environment/notation.tex @@ -29,8 +29,8 @@ \define\NLambda{{\sc Nλ}} \define\LOIS{{\sc Lois}} -% Libraries \define\cpp{{C++}} +\define\haskell{{Haskell}} % Maths \define\N{\naturalnumbers} @@ -49,6 +49,13 @@ \define[1]\lder{{#1}^{-1}} \define[2]\restr{{#1}|_{#2}} +\define\ext{ext} +\define\Nsize{N} +\define\Sym{Sym} + +\define\Lint{\mathcal{L}_{\text{int}}} +\define\Lmax{\mathcal{L}_{\text{max}}} + % language extension \define\Lext{{\cdot}}