joshua/phd-thesis
Archived
1
Fork 0
Code Activity

fixups

Browse source
This commit is contained in:
Joshua Moerman 2018-09-17 17:46:32 +02:00
parent 25a70d0c9b
commit 198d102f5d
2 changed files with 45 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
content.tex
View file

@ -15,7 +15,6 @@
\section{Nominal Techniques} \section{Nominal Techniques}
\component content/test-methods \component content/test-methods
\component content/applying-automata-learning \component content/applying-automata-learning
\chapter{Learning Embedded Stuff}
\chapter{Separating Sequences} \chapter{Separating Sequences}
\component content/learning-nominal-automata \component content/learning-nominal-automata
\chapter{Ordered Nominal Sets} \chapter{Ordered Nominal Sets}

88
content/learning-nominal-automata.tex
View file

@ -184,7 +184,7 @@ The table is closed and consistent, so we construct the hypothesis $\autom_1$.
\stoptikzpicture \stoptikzpicture
\starttikzpicture \starttikzpicture
\node[initial,state,initial text={$\autom_1 = $}] (q0) {$q_0$}; \node[initial,state,initial text={$\autom_1 = $}] (q0) {$q_0$};
\path (q0) edge[loop right] node[trlab,right] {$a,b$} (q0); \path (q0) edge[loop right] node[right] {$a,b$} (q0);
\stoptikzpicture \stoptikzpicture
\startformula \startformula
q_0 = row(\epsilon) = \{ \epsilon \mapsto 0 \} q_0 = row(\epsilon) = \{ \epsilon \mapsto 0 \}
@ -246,11 +246,11 @@ The new table is closed and consistent and a new hypothesis $\autom_2$ is constr
\node[state,accepting,below of=q1] (q2) {$q_2$}; \node[state,accepting,below of=q1] (q2) {$q_2$};
\path[->] \path[->]
(q0) edge[loop below] node[trlab,below] {$b$} (q0) (q0) edge[loop below] node[below] {$b$} (q0)
(q0) edge[bend right] node[trlab,above] {$a$} (q1) (q0) edge[bend right] node[above] {$a$} (q1)
(q1) edge[bend right] node[trlab,above] {$b$} (q0) (q1) edge[bend right] node[above] {$b$} (q0)
(q1) edge node[trlab,right] {$a$} (q2) (q1) edge node[right] {$a$} (q2)
(q2) edge node[trlab,midway,fill=white] {$a, b$} (q0); (q2) edge node[midway,fill=white] {$a, b$} (q0);
\stoptikzpicture \stoptikzpicture
The Teacher again replies {\bf no} and gives the counterexample $bb$, which should be accepted by $\autom_2$ but it is not. Therefore we put $S \gets S \cup \{b,bb\}$. The Teacher again replies {\bf no} and gives the counterexample $bb$, which should be accepted by $\autom_2$ but it is not. Therefore we put $S \gets S \cup \{b,bb\}$.
@ -316,13 +316,13 @@ The new hypothesis is $\autom_3$.
\node[state,accepting,right of=q2] (q3) {$q_3$}; \node[state,accepting,right of=q2] (q3) {$q_3$};
\path[->] \path[->]
(q0) edge[bend left] node[trlab,above] {$a$} (q1) (q0) edge[bend left] node[above] {$a$} (q1)
(q1) edge[bend left] node[trlab,above] {$b$} (q0) (q1) edge[bend left] node[above] {$b$} (q0)
(q1) edge node[trlab,right] {$a$} (q3) (q1) edge node[right] {$a$} (q3)
(q0) edge[bend right] node[trlab,left] {$b$} (q2) (q0) edge[bend right] node[left] {$b$} (q2)
(q2) edge[bend right] node[trlab,left] {$a$} (q0) (q2) edge[bend right] node[left] {$a$} (q0)
(q2) edge node[trlab,above] {$b$} (q3) (q2) edge node[above] {$b$} (q3)
(q3) edge node[trlab,fill=white,midway] {$a,b$} (q0); (q3) edge node[fill=white,midway] {$a,b$} (q0);
\stoptikzpicture \stoptikzpicture
The Teacher replies {\bf no} and provides the counterexample $babb$, so $S \gets S \cup \{ba,bab\}$. The Teacher replies {\bf no} and provides the counterexample $babb$, so $S \gets S \cup \{ba,bab\}$.
@ -339,14 +339,14 @@ One more step brings us to the correct hypothesis $\autom_4$ (details are omitte
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\path[->] \path[->]
(q0) edge node[trlab,above left] {$a$} (q1) (q0) edge node[above left] {$a$} (q1)
(q1) edge node[trlab,above right] {$a$} (q3) (q1) edge node[above right] {$a$} (q3)
(q0) edge node[trlab,below left] {$b$} (q2) (q0) edge node[below left] {$b$} (q2)
(q2) edge node[trlab,below right] {$b$} (q3) (q2) edge node[below right] {$b$} (q3)
(q1) edge[bend left] node[trlab,above] {$b$} (q4) (q1) edge[bend left] node[above] {$b$} (q4)
(q3) edge node[trlab,above] {$a,b$} (q4) (q3) edge node[above] {$a,b$} (q4)
(q2) edge[bend right] node[trlab,below] {$a$} (q4) (q2) edge[bend right] node[below] {$a$} (q4)
(q4) edge[loop right] node[trlab,right] {$a,b$} (q4); (q4) edge[loop right] node[right] {$a,b$} (q4);
\stoptikzpicture \stoptikzpicture
\stopstep \stopstep
@ -370,17 +370,17 @@ Classical theory of finite automata does not apply to this kind of languages, bu
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\path[->] \path[->]
(q0) edge node[trlab,above left] {$a$} (qa) (q0) edge node[above left] {$a$} (qa)
(qa) edge node[trlab,above right] {$a$} (q3) (qa) edge node[above right] {$a$} (q3)
(q0) edge node[trlab,above] {$b$} (qb) (q0) edge node[above] {$b$} (qb)
(qb) edge node[trlab,above] {$b$} (q3) (qb) edge node[above] {$b$} (q3)
(q0) edge node[trlab] {} (qdots) (q0) edge node {} (qdots)
(qdots) edge node[trlab] {} (q3) (qdots) edge node {} (q3)
(qa) edge[bend left] node[trlab,above] {${\neq} a$} (q4) (qa) edge[bend left] node[above] {${\neq} a$} (q4)
(q3) edge node[trlab,above] {$A$} (q4) (q3) edge node[above] {$A$} (q4)
(qb) edge[bend right] node[trlab,below] {${\neq} b$} (q4) (qb) edge[bend right] node[below] {${\neq} b$} (q4)
(qdots) edge[bend right] node[trlab] {} (q4) (qdots) edge[bend right] node {} (q4)
(q4) edge[loop right] node[trlab,right] {$A$} (q4); (q4) edge[loop right] node[right] {$A$} (q4);
\stoptikzpicture \stoptikzpicture
where $\tot{A}$ and $\tot{{\neq} a}$ stand for the infinitely-many transitions labelled by elements of $A$ and $A \setminus \{a\}$, respectively. where $\tot{A}$ and $\tot{{\neq} a}$ stand for the infinitely-many transitions labelled by elements of $A$ and $A \setminus \{a\}$, respectively.
@ -391,14 +391,14 @@ This automaton is infinite, but it can be finitely presented in a variety of way
\node[state, right of=q0] (qx) {$q_x$}; \node[state, right of=q0] (qx) {$q_x$};
\node[state,accepting,right of=qx] (q3) {$q_3$}; \node[state,accepting,right of=qx] (q3) {$q_3$};
\node[state,right of=q3] (q4) {$q_4$}; \node[state,right of=q3] (q4) {$q_4$};
\node[above = 0pt of qx] (qa) {\scriptsize{$\forall x \in A$}}; \node[above = 0pt of qx] (qa) {$\forall x \in A$};
\path[->] \path[->]
(q0) edge node[trlab,above] {$x$} (qx) (q0) edge node[above] {$x$} (qx)
(qx) edge node[trlab,above] {$x$} (q3) (qx) edge node[above] {$x$} (q3)
(q3) edge node[trlab,above] {$A$} (q4) (q3) edge node[above] {$A$} (q4)
(qx) edge[bend right] node[trlab,below] {${\neq} x$} (q4) (qx) edge[bend right] node[below] {${\neq} x$} (q4)
(q4) edge[loop right] node[trlab,right] {$A$} (q4); (q4) edge[loop right] node[right] {$A$} (q4);
\stoptikzpicture \stoptikzpicture
One can formalize the quantifier notation above (or indeed the \quotation{dots} notation above that) in several ways. One can formalize the quantifier notation above (or indeed the \quotation{dots} notation above that) in several ways.
@ -470,7 +470,7 @@ Then, by {\bf (P2)}, $row(\pi(a))(\epsilon) = row(a)(\epsilon) = 0$, for all $\p
\stoptikzpicture \stoptikzpicture
\starttikzpicture \starttikzpicture
\node[initial,state,initial text={$\autom'_1 = $}] (q0) {$q_0$}; \node[initial,state,initial text={$\autom'_1 = $}] (q0) {$q_0$};
\path (q0) edge[loop right] node[trlab,right] {$A$} (q0); \path (q0) edge[loop right] node[right] {$A$} (q0);
\stoptikzpicture \stoptikzpicture
It is closed and consistent. It is closed and consistent.
@ -543,10 +543,10 @@ The hypothesis automaton is
\node[right of=q2] (dummy) {$\forall x \in A$}; \node[right of=q2] (dummy) {$\forall x \in A$};
\path[->] \path[->]
(q0) edge[bend left] node[trlab,above] {$x$} (qx) (q0) edge[bend left] node[above] {$x$} (qx)
(qx) edge[bend left] node[trlab,above] {$\neq x$} (q0) (qx) edge[bend left] node[above] {$\neq x$} (q0)
(qx) edge node[trlab,above] {$x$} (q2) (qx) edge node[above] {$x$} (q2)
(q2) edge[bend right=50] node[trlab,below] {$A$} (q0); (q2) edge[bend right=50] node[below] {$A$} (q0);
\stoptikzpicture \stoptikzpicture
This is again incorrect, but one additional step will give the correct hypothesis automaton, shown earlier in \in{?}[eq:aut]). This is again incorrect, but one additional step will give the correct hypothesis automaton, shown earlier in \in{?}[eq:aut]).
@ -698,7 +698,7 @@ The learning algorithm for nominal automata, \nLStar{}, will be very similar to
In fact, we only change the following lines: In fact, we only change the following lines:
\placeformula[eq:changes] \placeformula[eq:changes]
\startformula[interlinespace=small]\startmathmatrix[n=2, align={middle, left}, distance=1cm] \startformula[interlinespace=small]\startmathmatrix[n=2, align={middle, left}, distance=1cm]
\NC \text{\color[darkgray]{7'} \NC S \gets S \cup \orb(sa) \NR \NC \text{\color[darkgray]{7'}} \NC S \gets S \cup \orb(sa) \NR
\NC \text{\color[darkgray]{11'}} \NC E \gets E \cup \orb(ae) \NR \NC \text{\color[darkgray]{11'}} \NC E \gets E \cup \orb(ae) \NR
\NC \text{\color[darkgray]{16'}} \NC S \gets S \cup \pref(\orb(t)) \NR \NC \text{\color[darkgray]{16'}} \NC S \gets S \cup \pref(\orb(t)) \NR
\stopmathmatrix\stopformula \stopmathmatrix\stopformula