diff --git a/biblio.bib b/biblio.bib index cd5d275..ef19237 100644 --- a/biblio.bib +++ b/biblio.bib @@ -889,7 +889,7 @@ author = {Gian Luigi Ferrari and Ugo Montanari and Emilio Tuosto}, - title = {Coalgebraic minimization of HD-automata for the Pi-calculus using + title = {Coalgebraic minimization of {HD}-automata for the $\pi$-calculus using polymorphic types}, journal = {Theor. Comput. Sci.}, volume = {331}, diff --git a/content/ordered-nominal-sets.tex b/content/ordered-nominal-sets.tex index 12c9cea..80e8dad 100644 --- a/content/ordered-nominal-sets.tex +++ b/content/ordered-nominal-sets.tex @@ -379,19 +379,19 @@ Combining this, we find that the orbit is $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$ 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 +\placetable[here][tab:overview]{Overview of representation.} +\starttabulate[|l|p|] +\NC \emph{Object} \NC \emph{Representation} \NC\NR +\HL %---------------------------------------- +\NC Single orbit $O$ \NC Natural number $n = \dim(O)$ \NC\NR +\NC Nominal set $X = \bigcup_i O_i$ \NC Multiset of these numbers \NC\NR +\HL %---------------------------------------- +\NC Map from single orbit $f \colon O \to Y$ \NC The orbit $f(O)$ and a bit string $F$ \NC\NR +\NC Equivariant map $f \colon X \to Y$ \NC Set of tuples $(O, F, f(O))$, one for each orbit \NC\NR +\HL %---------------------------------------- +\NC Orbit in a product $O \subseteq X \times Y$ \NC The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports \NC\NR +\NC Product $X \times Y$ \NC Set of tuples $(P, O_X, O_Y)$, one for each orbit \NC\NR +\stoptabulate 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. @@ -404,7 +404,7 @@ As a base case we can represent single orbits by their dimension. 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}.} +\footnote{\ONS{} can be found at \href{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{}. @@ -463,20 +463,18 @@ 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 +\placetable[here][tab:complexity]{Time complexity of operations on nominal sets.} +\starttabulate[|r|l|] +\NC \emph{Operation} \VL \emph{Complexity} \NC\NR +\HL +\NC Test $x \in X$ \VL $O(\log \Nsize(X))$ \NC\NR +\NC Test $X\subseteq Y$ \VL $O(\min(\Nsize(X)+\Nsize(Y), \Nsize(X)\log \Nsize(Y)))$ \NC\NR +\NC Calculate $X \cup Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR +\NC Calculate $X \cap Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR +\NC Calculate $\{x \in X \mid p(x)\}$ \VL $O(\Nsize(X))$ \NC\NR +\NC Calculate $\{f(x) \mid x \in X\}$ \VL $O(\Nsize(X)\log \Nsize(X))$ \NC\NR +\NC Calculate $X\times Y$ \VL $O(\Nsize(X\times Y)) \,\subseteq\, O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$ \NC\NR +\stoptabulate \stoptheorem \startproof @@ -535,27 +533,25 @@ 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] {}; +\starttikzpicture[node distance=3.5cm] +\node (S 0) [state] {$q_0$}; +\node (S 1) [state, right of=S 0] {$q_1(a)$}; +\node (S 2) [state, accepting, right of=S 1] {$q_2(a,b)$}; +\node (S 3) [state, right of=S 2] {$q_3(a,b)$}; +\node (S 4) [state, below=1.5cm of S 2] {$q_4$}; -% \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] +(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 +\placetable[here][minimize_results] +{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).} +\starttabulate[|l|l|l|r|r|r|r|][distance=none] +\NC Type \NC $\Nsize(S)$ \NC $\Nsize(S^{\text{min}})$ \VL \ONS{} \NC \color[darkgray]{(Gen.)} \VL \NLambda{} \VL \LOIS{} \NC\NR +\HL +\NC rand$_{5,1}$ (x10) \NC $5$ \NC n/a \VL $0.02$s \NC \color[darkgray]{n/a} \VL $0.82$s \VL $3.14$s \NC\NR +\NC rand$_{10,1}$ (x10) \NC $10$ \NC n/a \VL $0.03$s \NC \color[darkgray]{n/a} \VL $17.03$s \VL $1$m $32$s \NC\NR +\NC rand$_{10,2}$ (x10) \NC $10$ \NC n/a \VL $0.09$s \NC \color[darkgray]{n/a} \VL $35$m $14$s \VL $> 60$m \NC\NR +\NC rand$_{15,1}$ (x10) \NC $15$ \NC n/a \VL $0.04$s \NC \color[darkgray]{n/a} \VL $1$m $27$s \VL $10$m $20$s \NC\NR +\NC rand$_{15,2}$ (x10) \NC $15$ \NC n/a \VL $0.11$s \NC \color[darkgray]{n/a} \VL $55$m $46$s \VL $> 60$m \NC\NR +\NC rand$_{15,3}$ (x10) \NC $15$ \NC n/a \VL $0.46$s \NC \color[darkgray]{n/a} \VL $> 60$m \VL $> 60$m \NC\NR +\HL +\NC FIFO($2$) \NC $13$ \NC $6$ \VL $0.01$s \NC \color[darkgray]{$0.01$s} \VL $1.37$s \VL $0.24$s \NC\NR +\NC FIFO($3$) \NC $65$ \NC $19$ \VL $0.38$s \NC \color[darkgray]{$0.09$s} \VL $11.59$s \VL $2.4$s \NC\NR +\NC FIFO($4$) \NC $440$ \NC $94$ \VL $39.11$s \NC \color[darkgray]{$1.60$s} \VL $1$m $16$s \VL $14.95$s \NC\NR +\NC FIFO($5$) \NC $3686$ \NC $635$ \VL $> 60$m \NC \color[darkgray]{$39.78$s} \VL $6$m $42$s \VL $1$m $11$s \NC\NR +\HL +\NC $ww(2)$ \NC $8$ \NC $8$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $0.14$s \VL $0.03$s \NC\NR +\NC $ww(3)$ \NC $24$ \NC $24$ \VL $0.19$s \NC \color[darkgray]{$0.02$s} \VL $0.88$s \VL $0.16$s \NC\NR +\NC $ww(4)$ \NC $112$ \NC $112$ \VL $26.44$s \NC \color[darkgray]{$0.25$s} \VL $3.41$s \VL $0.61$s \NC\NR +\NC $ww(5)$ \NC $728$ \NC $728$ \VL $> 60$m \NC \color[darkgray]{$6.37$s} \VL $10.54$s \VL $1.80$s \NC\NR +\HL +\NC $\Lmax$ \NC $5$ \NC $3$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $2.06$s \VL $0.03$s \NC\NR +\NC $\Lint$ \NC $5$ \NC $5$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $1.55$s \VL $0.03$s \NC\NR +\stoptabulate 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. @@ -762,7 +758,7 @@ In particular, it learns a nominal DFA (over an infinite alphabet) using only fi 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.} +\footnote{See \href{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 \in{Chapter}[chap:learning-nominal-automata]. @@ -771,7 +767,7 @@ For the correctness, termination, and comparison with other learning algorithms 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}.} +\footnote{Can be found on \href{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. @@ -804,33 +800,30 @@ For languages which are equivariant for the equality symmetry, the \NLambda{} im 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 +\placetable[here][learning_results] +{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.} +\starttabulate[|l|l|l|r|r|r|r|r|r|][distance=none] +\NC \NC \NC \VL \NC \ONS{} \VL \NC \NLambda{}$^{\mathit{ord}}$ \VL \NC \NLambda{}$^{\mathit{eq}}$ \NC\NR +\NC Model \NC $\Nsize(S)$ \NC $\dim(S)$ \VL time \NC MQs \VL time \NC MQs \VL time \NC MQs \NC\NR +\HL +\NC rand$_{5,1}$ \NC $4$ \NC $1$ \VL $2$m $7$s \NC $2321$ \VL $39$m $51$s \NC $1243$ \VL \NC \NC\NR +\NC rand$_{5,1}$ \NC $5$ \NC $1$ \VL $0.12$s \NC $404$ \VL $40$m $34$s \NC $435$ \VL \NC \NC\NR +\NC rand$_{5,1}$ \NC $3$ \NC $0$ \VL $0.86$s \NC $499$ \VL $30$m $19$s \NC $422$ \VL \NC \NC\NR +\NC rand$_{5,1}$ \NC $5$ \NC $1$ \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \VL \NC \NC\NR +\NC rand$_{5,1}$ \NC $4$ \NC $1$ \VL $0.08$s \NC $387$ \VL $34$m $57$s \NC $387$ \VL \NC \NC\NR +\HL +\NC FIFO$(1)$ \NC $3$ \NC $1$ \VL $0.04$s \NC $119$ \VL $3.17$s \NC $119$ \VL $1.76$s \NC $51$ \NC\NR +\NC FIFO$(2)$ \NC $6$ \NC $2$ \VL $1.73$s \NC $2655$ \VL $6$m $32$s \NC $3818$ \VL $40.00$s \NC $434$ \NC\NR +\NC FIFO$(3)$ \NC $19$ \NC $3$ \VL $46$m $34$s\NC $298400$ \VL $> 60$m \NC n/a \VL $34$m $7$s \NC $8151$ \NC\NR +\HL +\NC $ww(1)$ \NC $4$ \NC $1$ \VL $0.42$s \NC $134$ \VL $2.49$s \NC $77$ \VL $1.47$s \NC $30$ \NC\NR +\NC $ww(2)$ \NC $8$ \NC $2$ \VL $4$m $26$s \NC $3671$ \VL $3$m $48$s \NC $2140$ \VL $30.58$s \NC $237$ \NC\NR +\NC $ww(3)$ \NC $24$ \NC $3$ \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \NC\NR +\HL +\NC $\Lmax$ \NC $3$ \NC $1$ \VL $0.01$s \NC $54$ \VL $3.58$s \NC $54$ \VL \NC \NC\NR +\NC $\Lint$ \NC $5$ \NC $2$ \VL $0.59$s \NC $478$ \VL $1$m $23$s \NC $478$ \VL \NC \NC\NR +\stoptabulate \stopsubsubsection diff --git a/environment.tex b/environment.tex index 2c23f94..397f0a7 100644 --- a/environment.tex +++ b/environment.tex @@ -63,6 +63,10 @@ \setupalgorithmic[before={\startframedtext[width=0.85\textwidth,offset=none,frame=off]},after={\stopframedtext}] % To enable linenumbers in a float +\def\href#1{\useURL[#1][{#1}]{\tt\goto{\url[#1]}[url(#1)]}} + + + % Debugging %\enabletrackers[references.references, visualizers.justification] %\showmakeup