| author | Christian Urban <urbanc@in.tum.de> | 
| Tue, 11 Apr 2017 06:22:46 +0800 | |
| changeset 483 | faba5360372c | 
| parent 482 | 74149519e436 | 
| child 484 | 8182eb3278e0 | 
| permissions | -rw-r--r-- | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1 | \documentclass{article}
 | 
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 2 | \usepackage{../style}
 | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 3 | \usepackage{../langs}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 4 | \usepackage{../graphics}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 5 | |
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 6 | |
| 480 | 7 | %We can even allow ``silent | 
| 8 | %transitions'', also called epsilon-transitions. They allow us | |
| 9 | %to go from one state to the next without having a character | |
| 10 | %consumed. We label such silent transition with the letter | |
| 11 | %$\epsilon$. | |
| 12 | ||
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 13 | \begin{document}
 | 
| 480 | 14 | \fnote{\copyright{} Christian Urban, King's College London, 2014, 2015, 2016, 2017}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 15 | |
| 482 | 16 | \section*{Handout 3 (Finite Automata)}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 17 | |
| 480 | 18 | Every formal language and compiler course I know of bombards you first | 
| 19 | with automata and then to a much, much smaller extend with regular | |
| 20 | expressions. As you can see, this course is turned upside down: | |
| 21 | regular expressions come first. The reason is that regular expressions | |
| 22 | are easier to reason about and the notion of derivatives, although | |
| 23 | already quite old, only became more widely known rather | |
| 24 | recently. Still let us in this lecture have a closer look at automata | |
| 25 | and their relation to regular expressions. This will help us with | |
| 26 | understanding why the regular expression matchers in Python, Ruby and | |
| 482 | 27 | Java are so slow with certain regular expressions. | 
| 28 | ||
| 29 | ||
| 30 | \subsection*{Deterministic Finite Automata}
 | |
| 31 | ||
| 483 | 32 | The central definition is:\medskip | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 33 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 34 | \noindent | 
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 35 | A \emph{deterministic finite automaton} (DFA), say $A$, is
 | 
| 483 | 36 | given by a five-tuple written $A(\Sigma, Qs, Q_0, F, \delta)$ where | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 37 | |
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 38 | \begin{itemize}
 | 
| 483 | 39 | \item $\Sigma$ is an alphabet, | 
| 482 | 40 | \item $Qs$ is a finite set of states, | 
| 41 | \item $Q_0 \in Qs$ is the start state, | |
| 42 | \item $F \subseteq Qs$ are the accepting states, and | |
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 43 | \item $\delta$ is the transition function. | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 44 | \end{itemize}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 45 | |
| 482 | 46 | \noindent The transition function determines how to ``transition'' | 
| 47 | from one state to the next state with respect to a character. We have | |
| 48 | the assumption that these transition functions do not need to be | |
| 49 | defined everywhere: so it can be the case that given a character there | |
| 50 | is no next state, in which case we need to raise a kind of ``failure | |
| 483 | 51 | exception''.  That means actually we have \emph{partial} functions as
 | 
| 52 | transitions---see the implementation later on. A typical example of a | |
| 482 | 53 | DFA is | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 54 | |
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 55 | \begin{center}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 56 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 57 |                     every state/.style={minimum size=0pt,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 58 | inner sep=2pt,draw=blue!50,very thick, | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 59 | fill=blue!20},scale=2] | 
| 482 | 60 | \node[state,initial]  (Q_0)  {$Q_0$};
 | 
| 61 | \node[state] (Q_1) [right=of Q_0] {$Q_1$};
 | |
| 62 | \node[state] (Q_2) [below right=of Q_0] {$Q_2$};
 | |
| 63 | \node[state] (Q_3) [right=of Q_2] {$Q_3$};
 | |
| 64 | \node[state, accepting] (Q_4) [right=of Q_1] {$Q_4$};
 | |
| 65 | \path[->] (Q_0) edge node [above]  {$a$} (Q_1);
 | |
| 66 | \path[->] (Q_1) edge node [above]  {$a$} (Q_4);
 | |
| 67 | \path[->] (Q_4) edge [loop right] node  {$a, b$} ();
 | |
| 68 | \path[->] (Q_3) edge node [right]  {$a$} (Q_4);
 | |
| 69 | \path[->] (Q_2) edge node [above]  {$a$} (Q_3);
 | |
| 70 | \path[->] (Q_1) edge node [right]  {$b$} (Q_2);
 | |
| 71 | \path[->] (Q_0) edge node [above]  {$b$} (Q_2);
 | |
| 72 | \path[->] (Q_2) edge [loop left] node  {$b$} ();
 | |
| 73 | \path[->] (Q_3) edge [bend left=95, looseness=1.3] node [below]  {$b$} (Q_0);
 | |
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 74 | \end{tikzpicture}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 75 | \end{center}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 76 | |
| 482 | 77 | \noindent In this graphical notation, the accepting state $Q_4$ is | 
| 78 | indicated with double circles. Note that there can be more than one | |
| 79 | accepting state. It is also possible that a DFA has no accepting | |
| 80 | states at all, or that the starting state is also an accepting | |
| 81 | state. In the case above the transition function is defined everywhere | |
| 82 | and can also be given as a table as follows: | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 83 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 84 | \[ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 85 | \begin{array}{lcl}
 | 
| 482 | 86 | (Q_0, a) &\rightarrow& Q_1\\ | 
| 87 | (Q_0, b) &\rightarrow& Q_2\\ | |
| 88 | (Q_1, a) &\rightarrow& Q_4\\ | |
| 89 | (Q_1, b) &\rightarrow& Q_2\\ | |
| 90 | (Q_2, a) &\rightarrow& Q_3\\ | |
| 91 | (Q_2, b) &\rightarrow& Q_2\\ | |
| 92 | (Q_3, a) &\rightarrow& Q_4\\ | |
| 93 | (Q_3, b) &\rightarrow& Q_0\\ | |
| 94 | (Q_4, a) &\rightarrow& Q_4\\ | |
| 95 | (Q_4, b) &\rightarrow& Q_4\\ | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 96 | \end{array}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 97 | \] | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 98 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 99 | We need to define the notion of what language is accepted by | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 100 | an automaton. For this we lift the transition function | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 101 | $\delta$ from characters to strings as follows: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 102 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 103 | \[ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 104 | \begin{array}{lcl}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 105 | \hat{\delta}(q, [])        & \dn & q\\
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 106 | \hat{\delta}(q, c\!::\!s) & \dn & \hat{\delta}(\delta(q, c), s)\\
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 107 | \end{array}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 108 | \] | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 109 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 110 | \noindent This lifted transition function is often called | 
| 480 | 111 | ``delta-hat''. Given a string, we start in the starting state and take | 
| 112 | the first character of the string, follow to the next sate, then take | |
| 113 | the second character and so on. Once the string is exhausted and we | |
| 114 | end up in an accepting state, then this string is accepted by the | |
| 115 | automaton. Otherwise it is not accepted. This also means that if along | |
| 116 | the way we hit the case where the transition function $\delta$ is not | |
| 117 | defined, we need to raise an error. In our implementation we will deal | |
| 482 | 118 | with this case elegantly by using Scala's \texttt{Try}. So a string
 | 
| 483 | 119 | $s$ is in the \emph{language accepted by the automaton} $A(\Sigma, Q, Q_0, F,
 | 
| 482 | 120 | \delta)$ iff | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 121 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 122 | \[ | 
| 482 | 123 | \hat{\delta}(Q_0, s) \in F 
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 124 | \] | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 125 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 126 | \noindent I let you think about a definition that describes | 
| 483 | 127 | the set of all strings accepted by an automaton. | 
| 480 | 128 | |
| 129 | \begin{figure}[p]
 | |
| 130 | \small | |
| 131 | \lstinputlisting[numbers=left,linebackgroundcolor= | |
| 132 |                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
 | |
| 133 |                   {../progs/dfa.scala}
 | |
| 482 | 134 | \caption{A Scala implementation of DFAs using partial functions.
 | 
| 480 | 135 |   Notice some subtleties: \texttt{deltas} implements the delta-hat
 | 
| 136 | construction by lifting the transition (partial) function to | |
| 483 | 137 |   lists of characters. Since \texttt{delta} is given
 | 
| 138 | as a partial function, it can obviously go ``wrong'' in which | |
| 480 | 139 |   case the \texttt{Try} in \texttt{accepts} catches the error and
 | 
| 482 | 140 |   returns \texttt{false}---that means the string is not accepted.
 | 
| 141 |   The example \texttt{delta} implements the DFA example shown
 | |
| 142 |   earlier in the handout.\label{dfa}}
 | |
| 480 | 143 | \end{figure}
 | 
| 144 | ||
| 482 | 145 | A simple Scala implementation for DFAs is given in | 
| 483 | 146 | Figure~\ref{dfa}. As you can see, there are many features of the
 | 
| 482 | 147 | mathematical definition that are quite closely reflected in the | 
| 148 | code. In the DFA-class, there is a starting state, called | |
| 483 | 149 | \texttt{start}, with the polymorphic type \texttt{A}.  There is a
 | 
| 150 | partial function \texttt{delta} for specifying the transitions---these
 | |
| 151 | partial functions take a state (of polymorphic type \texttt{A}) and an
 | |
| 152 | input (of polymorphic type \texttt{C}) and produce a new state (of
 | |
| 153 | type \texttt{A}). For the moment it is OK to assume that \texttt{A} is
 | |
| 154 | some arbitrary type for states and the input is just characters. (The | |
| 155 | reason for having a polymorphic types for the states and the input of | |
| 156 | DFAs will become clearer later on.) | |
| 157 | ||
| 158 | I used partial functions for representing the transitions in Scala; | |
| 159 | alternatives would have been \texttt{Maps} or even \texttt{Lists}. One
 | |
| 160 | of the main advantages of using partial functions is that transitions | |
| 161 | can be quite nicely defined by a series of \texttt{case} statements
 | |
| 162 | (see Lines 28 -- 38 for an example). If you need to represent an | |
| 163 | automaton with a sink state (catch-all-state), you can use Scala's | |
| 164 | pattern matching and write something like | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 165 | |
| 480 | 166 | {\small\begin{lstlisting}[language=Scala,linebackgroundcolor=
 | 
| 167 |                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
 | |
| 168 | abstract class State | |
| 169 | ... | |
| 170 | case object Sink extends State | |
| 171 | ||
| 172 | val delta : (State, Char) :=> State = | |
| 173 |   { case (S0, 'a') => S1
 | |
| 174 | case (S1, 'a') => S2 | |
| 175 | case _ => Sink | |
| 176 | } | |
| 177 | \end{lstlisting}}  
 | |
| 178 | ||
| 482 | 179 | \noindent The DFA-class has also an argument for specifying final | 
| 483 | 180 | states. In the implementation it not a set of states, as in the | 
| 181 | matemathical definition, but is a function from states to booleans | |
| 182 | (this function is supposed to return true whenever a state is meant to | |
| 183 | be final; false otherwise). While this boolean function is different | |
| 184 | from the sets of states, Scala allows to use sets for such functions | |
| 185 | (see Line 40 where the DFA is initialised). Again it will become clear | |
| 186 | later on why I use functions for final states, rather than sets. | |
| 480 | 187 | |
| 188 | I let you ponder whether this is a good implementation of DFAs. In | |
| 482 | 189 | doing so I hope you notice that the $Qs$ component (the set of finite | 
| 480 | 190 | states) is missing from the class definition. This means that the | 
| 191 | implementation allows you to do some fishy things you are not meant to | |
| 192 | do with DFAs. Which fishy things could that be? | |
| 193 | ||
| 482 | 194 | |
| 195 | ||
| 196 | \subsection*{Non-Deterministic Finite Automata}
 | |
| 197 | ||
| 198 | While with DFAs it will always be clear that given a state and a | |
| 199 | character what the next state is (potentially none), it will be useful | |
| 200 | to relax this restriction. That means we allow to have several | |
| 201 | potential successor states. We even allow more than one starting | |
| 202 | state. The resulting construction is called a \emph{non-deterministic
 | |
| 483 | 203 |   finite automaton} (NFA) given also as a five-tuple $A(\Sigma, Qs, Q_{0s}, F,
 | 
| 482 | 204 | \rho)$ where | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 205 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 206 | \begin{itemize}
 | 
| 483 | 207 | \item $\Sigma$ is an alphabet, | 
| 482 | 208 | \item $Qs$ is a finite set of states | 
| 209 | \item $Q_{0s}$ is a set of start states ($Q_{0s} \subseteq Qs$)
 | |
| 210 | \item $F$ are some accepting states with $F \subseteq Qs$, and | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 211 | \item $\rho$ is a transition relation. | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 212 | \end{itemize}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 213 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 214 | \noindent | 
| 483 | 215 | A typical example of a NFA is | 
| 482 | 216 | |
| 217 | % A NFA for (ab* + b)*a | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 218 | \begin{center}
 | 
| 483 | 219 | \begin{tikzpicture}[>=stealth',very thick, auto,
 | 
| 220 |     every state/.style={minimum size=0pt,inner sep=3pt,
 | |
| 221 | draw=blue!50,very thick,fill=blue!20},scale=2] | |
| 482 | 222 | \node[state,initial]  (Q_0)  {$Q_0$};
 | 
| 223 | \node[state] (Q_1) [right=of Q_0] {$Q_1$};
 | |
| 224 | \node[state, accepting] (Q_2) [right=of Q_1] {$Q_2$};
 | |
| 225 | \path[->] (Q_0) edge [loop above] node  {$b$} ();
 | |
| 226 | \path[<-] (Q_0) edge node [below]  {$b$} (Q_1);
 | |
| 227 | \path[->] (Q_0) edge [bend left] node [above]  {$a$} (Q_1);
 | |
| 228 | \path[->] (Q_0) edge [bend right] node [below]  {$a$} (Q_2);
 | |
| 229 | \path[->] (Q_1) edge [loop above] node  {$a,b$} ();
 | |
| 230 | \path[->] (Q_1) edge node  [above] {$a$} (Q_2);
 | |
| 231 | \end{tikzpicture}
 | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 232 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 233 | |
| 482 | 234 | \noindent | 
| 235 | This NFA happens to have only one starting state, but in general there | |
| 236 | could be more. Notice that in state $Q_0$ we might go to state $Q_1$ | |
| 483 | 237 | \emph{or} to state $Q_2$ when receiving an $a$. Similarly in state
 | 
| 238 | $Q_1$ and receiving an $a$, we can stay in state $Q_1$ or go to | |
| 239 | $Q_2$. This kind of choice is not allowed with DFAs. The downside is | |
| 240 | that when it comes to deciding whether a string is accepted by a NFA | |
| 241 | we potentially have to explore all possibilities. I let you think | |
| 242 | which kind of strings the above NFA accepts. | |
| 482 | 243 | |
| 244 | ||
| 483 | 245 | There are a number of additional points you should note with | 
| 246 | NFAs. Every DFA is a NFA, but not vice versa. The $\rho$ in NFAs is a | |
| 247 | transition \emph{relation} (DFAs have a transition function). The
 | |
| 248 | difference between a function and a relation is that a function has | |
| 249 | always a single output, while a relation gives, roughly speaking, | |
| 250 | several outputs. Look again at the NFA above: if you are currently in | |
| 251 | the state $Q_1$ and you read a character $b$, then you can transition | |
| 252 | to either $Q_0$ \emph{or} $Q_2$. Which route, or output, you take is
 | |
| 253 | not determined. This non-determinism can be represented by a | |
| 254 | relation. | |
| 482 | 255 | |
| 483 | 256 | My implementation of NFAs in Scala is shown in Figure~\ref{nfa}.
 | 
| 257 | Perhaps interestingly, I do not actually use relations for my NFAs, | |
| 258 | and I also do not use transition functions that return sets of states | |
| 259 | (another popular choice for implementing NFAs). For reasons that | |
| 260 | become clear in a moment, I use sets of partial functions | |
| 261 | instead---see Line 7 in Figure~\ref{nfa}. DFAs have only one such
 | |
| 262 | partial function; my NFAs have a set. Another parameter, | |
| 263 | \texttt{Starts}, is in NFAs a set of states; \texttt{fins} is again a
 | |
| 264 | function from states to booleans. The \texttt{next} function
 | |
| 265 | calculates the set of next states reachable from a single state | |
| 266 | \texttt{q} by a character \texttt{c}---this is calculated by going
 | |
| 267 | through all the partial functions in the \texttt{delta}-set and apply
 | |
| 268 | \texttt{q} and \texttt{c} (see Line 13). This gives us a set of
 | |
| 269 | \texttt{Some}s (in case the application succeeded) and possibly some
 | |
| 270 | \texttt{None}s (in case the partial function is not defined or produces an
 | |
| 271 | error).  The \texttt{None}s are filtered out by the \texttt{flatMap},
 | |
| 272 | leaving the values inside the \texttt{Some}s. The function
 | |
| 273 | \texttt{nexts} just lifts this function to sets of
 | |
| 274 | states. \texttt{Deltas} and \texttt{accept} are similar to the DFA
 | |
| 275 | definitions. | |
| 482 | 276 | |
| 277 | \begin{figure}[t]
 | |
| 278 | \small | |
| 279 | \lstinputlisting[numbers=left,linebackgroundcolor= | |
| 280 |                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
 | |
| 281 |                   {../progs/nfa.scala}
 | |
| 282 | \caption{A Scala implementation of NFAs using sets of partial functions.
 | |
| 483 | 283 |   Notice some subtleties: Since \texttt{delta} is given
 | 
| 284 | as a set of partial functions, each of them can obviously go ``wrong'' in which | |
| 285 |   case the \texttt{Try}. The function \texttt{accepts} implements the
 | |
| 286 | acceptance of a string in a breath-first fashion. This can be costly | |
| 287 |   way of deciding whether a string is accepted in practical contexts.\label{nfa}}
 | |
| 482 | 288 | \end{figure}
 | 
| 289 | ||
| 483 | 290 | The reason for using sets of partial functions for specifying the | 
| 291 | transitions in NFAs has to do with examples like this one: a | |
| 292 | popular benchmark regular expression is $(.)^*\cdot a\cdot | |
| 293 | (.)^{\{n\}}\cdot b\cdot c$. A NFA that accepts the same strings
 | |
| 294 | (for $n=3$) is as follows: | |
| 482 | 295 | |
| 483 | 296 | \begin{center}
 | 
| 297 | \begin{tikzpicture}[>=stealth',very thick, auto, node distance=7mm,
 | |
| 298 |     every state/.style={minimum size=0pt,inner sep=1pt,
 | |
| 299 | draw=blue!50,very thick,fill=blue!20},scale=0.5] | |
| 300 | \node[state,initial]  (Q_0)  {$Q_0$};
 | |
| 301 | \node[state] (Q_1) [right=of Q_0] {$Q_1$};
 | |
| 302 | \node[state] (Q_2) [right=of Q_1] {$Q_2$};
 | |
| 303 | \node[state] (Q_3) [right=of Q_2] {$Q_3$};
 | |
| 304 | \node[state] (Q_4) [right=of Q_3] {$Q_4$};
 | |
| 305 | \node[state] (Q_5) [right=of Q_4] {$Q_5$};
 | |
| 306 | \node[state,accepting] (Q_6) [right=of Q_5] {$Q_6$};
 | |
| 307 | \path[->] (Q_0) edge [loop above] node  {$.$} ();
 | |
| 308 | \path[->] (Q_0) edge node [above]  {$a$} (Q_1);
 | |
| 309 | \path[->] (Q_1) edge node [above]  {$.$} (Q_2);
 | |
| 310 | \path[->] (Q_2) edge node [above]  {$.$} (Q_3);
 | |
| 311 | \path[->] (Q_3) edge node [above]  {$.$} (Q_4);
 | |
| 312 | \path[->] (Q_4) edge node [above]  {$b$} (Q_5);
 | |
| 313 | \path[->] (Q_5) edge node [above]  {$c$} (Q_6);
 | |
| 314 | \end{tikzpicture}
 | |
| 315 | \end{center}
 | |
| 316 | ||
| 317 | \noindent | |
| 318 | The $.$ stands for accepting any single character: for example if we | |
| 319 | are in $Q_0$ and read an $a$ we can either stay in $Q_0$ (since any | |
| 320 | character will do for this) or advance to $Q_1$ (but only if it is an | |
| 321 | $a$). Why this is a good benchmark regular expression is irrelevant | |
| 322 | here. The point is that this NFA can be conveniently represented by | |
| 323 | the code: | |
| 324 | ||
| 325 | {\small\begin{lstlisting}[language=Scala,linebackgroundcolor=
 | |
| 326 |                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
 | |
| 327 | val delta = Set[(State, Char) :=> State]( | |
| 328 |   { case (Q0, 'a') => Q1 },
 | |
| 329 |   { case (Q0, _)   => Q0 },
 | |
| 330 |   { case (Q1, _)   => Q2 },
 | |
| 331 |   { case (Q2, _)   => Q3 },
 | |
| 332 |   { case (Q3, _)   => Q4 },
 | |
| 333 |   { case (Q4, 'b') => Q5 },
 | |
| 334 |   { case (Q5, 'c') => Q6 }
 | |
| 335 | ) | |
| 336 | ||
| 337 | NFA(Set[State](Q0), delta, Set[State](Q6)) | |
| 338 | \end{lstlisting}}
 | |
| 339 | ||
| 340 | \noindent | |
| 341 | where the $.$-transitions translate into a | |
| 342 | underscore-pattern-matching. Recall that in $Q_0$ if we read an $a$ we | |
| 343 | can go to $Q_1$ (by the first partial function in the set) and also | |
| 344 | stay in $Q_0$ (by the second partial function). Representing such | |
| 345 | transitions in any other way is somehow awkward; the set of partial | |
| 346 | function representation makes them easy to implement. | |
| 347 | ||
| 348 | Look very careful again at the \texttt{accepts} and \texttt{deltas}
 | |
| 349 | functions in NFAs and remember that when accepting a string by an NFA | |
| 350 | we might have to explore all possible transitions (which state to go | |
| 351 | to is not unique anymore). The shown implementation achieves this | |
| 352 | exploration in a \emph{breath-first search}. This is fine for very
 | |
| 353 | small NFAs, but can lead to problems when the NFAs are bigger. Take | |
| 354 | for example the regular expression $(.)^*\cdot a\cdot (.)^{\{n\}}\cdot
 | |
| 355 | b\cdot c$ from above. If $n$ is large, say 100 or 1000, then the | |
| 356 | corresponding NFA will have 104, respectively 1004, nodes. The problem | |
| 357 | is that with certain strings this can lead to 1000 ``active'' nodes | |
| 358 | which we need to analyse when determining the next states. This can be | |
| 359 | a real memory strain in practical applications. As a result, some | |
| 360 | regular expression matching engines resort to a \emph{depth-first
 | |
| 361 |   search} with \emph{backtracking} in unsuccessful cases. In our
 | |
| 362 | implementation we could implement a depth-first version of | |
| 363 | \texttt{accepts} using Scala's \texttt{exists} as follows:
 | |
| 364 | ||
| 365 | ||
| 366 | {\small\begin{lstlisting}[language=Scala,linebackgroundcolor=
 | |
| 367 |                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
 | |
| 368 | def search(q: A, s: List[C]) : Boolean = s match {
 | |
| 369 | case Nil => fins(q) | |
| 370 | case c::cs => | |
| 371 | delta.exists((d) => Try(search(d(q, c), cs)) getOrElse false) | |
| 372 | } | |
| 373 | ||
| 374 | def accepts(s: List[C]) : Boolean = | |
| 375 | starts.exists(search(_, s)) | |
| 376 | \end{lstlisting}}
 | |
| 377 | ||
| 378 | \noindent | |
| 379 | This depth-first way of exploration seems to work efficiently in many | |
| 380 | examples and is much less of strain on memory. The problem is that the | |
| 381 | backtracking can get catastrophic in some examples---remember the | |
| 382 | catastrophic backtracking from earlier lectures. This depth-first | |
| 383 | search with backtracking is the reason for the abysmal performance of | |
| 384 | regular expression macthing in Java, Ruby and Python. | |
| 482 | 385 | |
| 386 | %This means if | |
| 387 | %we need to decide whether a string is accepted by a NFA, we might have | |
| 388 | %to explore all possibilities. Also there is the special silent | |
| 389 | %transition in NFAs. As mentioned already this transition means you do | |
| 390 | %not have to ``consume'' any part of the input string, but ``silently'' | |
| 391 | %change to a different state. In the left picture, for example, if you | |
| 392 | %are in the starting state, you can silently move either to $Q_1$ or | |
| 393 | %%$Q_2$. This silent transition is also often called | |
| 394 | %\emph{$\epsilon$-transition}.
 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 395 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 396 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 397 | \subsubsection*{Thompson Construction}
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 398 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 399 | The reason for introducing NFAs is that there is a relatively | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 400 | simple (recursive) translation of regular expressions into | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 401 | NFAs. Consider the simple regular expressions $\ZERO$, | 
| 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 402 | $\ONE$ and $c$. They can be translated as follows: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 403 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 404 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 405 | \begin{tabular}[t]{l@{\hspace{10mm}}l}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 406 | \raisebox{1mm}{$\ZERO$} & 
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 407 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 482 | 408 | \node[state, initial]  (Q_0)  {$\mbox{}$};
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 409 | \end{tikzpicture}\\\\
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 410 | \raisebox{1mm}{$\ONE$} & 
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 411 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 482 | 412 | \node[state, initial, accepting]  (Q_0)  {$\mbox{}$};
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 413 | \end{tikzpicture}\\\\
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 414 | \raisebox{2mm}{$c$} & 
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 415 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 482 | 416 | \node[state, initial]  (Q_0)  {$\mbox{}$};
 | 
| 417 | \node[state, accepting]  (Q_1)  [right=of Q_0] {$\mbox{}$};
 | |
| 418 | \path[->] (Q_0) edge node [below]  {$c$} (Q_1);
 | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 419 | \end{tikzpicture}\\\\
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 420 | \end{tabular}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 421 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 422 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 423 | \noindent The case for the sequence regular expression $r_1 | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 424 | \cdot r_2$ is as follows: We are given by recursion two | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 425 | automata representing $r_1$ and $r_2$ respectively. | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 426 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 427 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 428 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 429 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 482 | 430 | \node[state, initial]  (Q_0)  {$\mbox{}$};
 | 
| 431 | \node (r_1)  [right=of Q_0] {$\ldots$};
 | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 432 | \node[state, accepting]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 433 | \node[state, accepting]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 434 | \node[state, accepting]  (t_3)  [below=of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 435 | \node[state, initial]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 436 | \node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 437 | \node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 438 | \node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 439 | \node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 440 | \begin{pgfonlayer}{background}
 | 
| 482 | 441 | \node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (Q_0) (r_1) (t_1) (t_2) (t_3)] {};
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 442 | \node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 443 | \node [yshift=2mm] at (1.north) {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 444 | \node [yshift=2mm] at (2.north) {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 445 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 446 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 447 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 448 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 449 | \noindent The first automaton has some accepting states. We | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 450 | obtain an automaton for $r_1\cdot r_2$ by connecting these | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 451 | accepting states with $\epsilon$-transitions to the starting | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 452 | state of the second automaton. By doing so we make them | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 453 | non-accepting like so: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 454 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 455 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 456 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 457 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 482 | 458 | \node[state, initial]  (Q_0)  {$\mbox{}$};
 | 
| 459 | \node (r_1)  [right=of Q_0] {$\ldots$};
 | |
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 460 | \node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 461 | \node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 462 | \node[state]  (t_3)  [below=of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 463 | \node[state]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 464 | \node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 465 | \node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 466 | \node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 467 | \node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 468 | \path[->] (t_1) edge node [above, pos=0.3]  {$\epsilon$} (a_0);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 469 | \path[->] (t_2) edge node [above]  {$\epsilon$} (a_0);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 470 | \path[->] (t_3) edge node [below]  {$\epsilon$} (a_0);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 471 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 472 | \begin{pgfonlayer}{background}
 | 
| 482 | 473 | \node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (Q_0) (c_1) (c_2) (c_3)] {};
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 474 | \node [yshift=2mm] at (3.north) {$r_1\cdot r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 475 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 476 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 477 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 478 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 479 | \noindent The case for the choice regular expression $r_1 + | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 480 | r_2$ is slightly different: We are given by recursion two | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 481 | automata representing $r_1$ and $r_2$ respectively. | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 482 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 483 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 484 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 485 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 486 | \node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 487 | \node[state, initial]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 488 | \node[state, initial]  (3)  [below right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 489 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 490 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 491 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 492 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 493 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 494 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 495 | \node (b)  [right=of 3] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 496 | \node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 497 | \node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 498 | \node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 499 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 500 | \node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 501 | \node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 502 | \node [yshift=3mm] at (1.north) {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 503 | \node [yshift=3mm] at (2.north) {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 504 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 505 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 506 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 507 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 508 | \noindent Each automaton has a single start state and | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 509 | potentially several accepting states. We obtain a NFA for the | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 510 | regular expression $r_1 + r_2$ by introducing a new starting | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 511 | state and connecting it with an $\epsilon$-transition to the | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 512 | two starting states above, like so | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 513 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 514 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 515 | \hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 516 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 517 | \node at (0,0) [state, initial]  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 518 | \node[state]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 519 | \node[state]  (3)  [below right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 520 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 521 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 522 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 523 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 524 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 525 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 526 | \node (b)  [right=of 3] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 527 | \node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 528 | \node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 529 | \node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 530 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 531 | \path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 532 | \path[->] (1) edge node [below]  {$\epsilon$} (3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 533 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 534 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 535 | \node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 536 | \node [yshift=3mm] at (3.north) {$r_1+ r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 537 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 538 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 539 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 540 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 541 | \noindent | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 542 | Finally for the $*$-case we have an automaton for $r$ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 543 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 544 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 545 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 546 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 547 | \node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 548 | \node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 549 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 550 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 551 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 552 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 553 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 554 | \node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 555 | \node [yshift=3mm] at (1.north) {$r$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 556 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 557 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 558 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 559 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 560 | \noindent and connect its accepting states to a new starting | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 561 | state via $\epsilon$-transitions. This new starting state is | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 562 | also an accepting state, because $r^*$ can recognise the | 
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 563 | empty string. This gives the following automaton for $r^*$: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 564 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 565 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 566 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 567 |                              >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 568 | \node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 569 | \node[state]  (2)  [right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 570 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 571 | \node[state]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 572 | \node[state]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 573 | \node[state]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 574 | \path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 575 | \path[->] (a1) edge [bend left=45] node [above]  {$\epsilon$} (1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 576 | \path[->] (a2) edge [bend right] node [below]  {$\epsilon$} (1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 577 | \path[->] (a3) edge [bend left=45] node [below]  {$\epsilon$} (1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 578 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 579 | \node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 580 | \node [yshift=3mm] at (2.north) {$r^*$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 581 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 582 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 583 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 584 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 585 | \noindent This construction of a NFA from a regular expression | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 586 | was invented by Ken Thompson in 1968. | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 587 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 588 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 589 | \subsubsection*{Subset Construction}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 590 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 591 | What is interesting is that for every NFA we can find a DFA | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 592 | which recognises the same language. This can, for example, be | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 593 | done by the \emph{subset construction}. Consider again the NFA
 | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 594 | below on the left, consisting of nodes labeled $0$, $1$ and $2$. | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 595 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 596 | \begin{center}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 597 | \begin{tabular}{c@{\hspace{10mm}}c}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 598 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 599 |                     every state/.style={minimum size=0pt,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 600 | draw=blue!50,very thick,fill=blue!20}, | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 601 | baseline=0mm] | 
| 482 | 602 | \node[state,initial]  (Q_0)  {$0$};
 | 
| 603 | \node[state] (Q_1) [above=of Q_0] {$1$};
 | |
| 604 | \node[state, accepting] (Q_2) [below=of Q_0] {$2$};
 | |
| 605 | \path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_1);
 | |
| 606 | \path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_2);
 | |
| 607 | \path[->] (Q_0) edge [loop right] node  {$a$} ();
 | |
| 608 | \path[->] (Q_1) edge [loop above] node  {$a$} ();
 | |
| 609 | \path[->] (Q_2) edge [loop below] node  {$b$} ();
 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 610 | \end{tikzpicture}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 611 | & | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 612 | \begin{tabular}{r|cl}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 613 | nodes & $a$ & $b$\\ | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 614 | \hline | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 615 | $\{\}\phantom{\star}$ & $\{\}$ & $\{\}$\\
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 616 | $\{0\}\phantom{\star}$       & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 617 | $\{1\}\phantom{\star}$       & $\{1\}$       & $\{\}$\\
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 618 | $\{2\}\star$  & $\{\}$ & $\{2\}$\\
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 619 | $\{0,1\}\phantom{\star}$     & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 620 | $\{0,2\}\star$ & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 621 | $\{1,2\}\star$ & $\{1\}$       & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 622 | s: $\{0,1,2\}\star$ & $\{0,1,2\}$ & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 623 | \end{tabular}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 624 | \end{tabular}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 625 | \end{center}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 626 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 627 | \noindent The nodes of the DFA are given by calculating all | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 628 | subsets of the set of nodes of the NFA (seen in the nodes | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 629 | column on the right). The table shows the transition function | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 630 | for the DFA. The first row states that $\{\}$ is the
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 631 | sink node which has transitions for $a$ and $b$ to itself. | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 632 | The next three lines are calculated as follows: | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 633 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 634 | \begin{itemize}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 635 | \item suppose you calculate the entry for the transition for | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 636 |       $a$ and the node $\{0\}$
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 637 | \item start from the node $0$ in the NFA | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 638 | \item do as many $\epsilon$-transition as you can obtaining a | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 639 |       set of nodes, in this case $\{0,1,2\}$
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 640 | \item filter out all notes that do not allow an $a$-transition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 641 | from this set, this excludes $2$ which does not permit a | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 642 | $a$-transition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 643 | \item from the remaining set, do as many $\epsilon$-transition | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 644 |       as you can, this yields again $\{0,1,2\}$     
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 645 | \item the resulting set specifies the transition from $\{0\}$
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 646 | when given an $a$ | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 647 | \end{itemize}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 648 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 649 | \noindent So the transition from the state $\{0\}$ reading an
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 650 | $a$ goes to the state $\{0,1,2\}$. Similarly for the other
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 651 | entries in the rows for $\{0\}$, $\{1\}$ and $\{2\}$. The
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 652 | other rows are calculated by just taking the union of the | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 653 | single node entries. For example for $a$ and $\{0,1\}$ we need
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 654 | to take the union of $\{0,1,2\}$ (for $0$) and $\{1\}$ (for
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 655 | $1$). The starting state of the DFA can be calculated from the | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 656 | starting state of the NFA, that is $0$, and then do as many | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 657 | $\epsilon$-transitions as possible. This gives $\{0,1,2\}$
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 658 | which is the starting state of the DFA. The terminal states in | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 659 | the DFA are given by all sets that contain a $2$, which is the | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 660 | terminal state of the NFA. This completes the subset | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 661 | construction. So the corresponding DFA to the NFA from | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 662 | above is | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 663 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 664 | \begin{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 665 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 666 |                     every state/.style={minimum size=0pt,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 667 | draw=blue!50,very thick,fill=blue!20}, | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 668 | baseline=0mm] | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 669 | \node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 670 | \node[state,accepting] (q02) [right=of q012] {$0,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 671 | \node[state] (q01) [above=of q02] {$0,1$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 672 | \node[state,accepting] (q12) [below=of q02] {$1,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 673 | \node[state] (q0) [right=2cm of q01] {$0$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 674 | \node[state] (q1) [right=2.5cm of q02] {$1$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 675 | \node[state,accepting] (q2) [right=1.5cm of q12] {$2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 676 | \node[state] (qn) [right=of q1] {$\{\}$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 677 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 678 | \path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 679 | \path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 680 | \path[->] (q12) edge [bend left] node [below,pos=0.4]  {$a$} (q1);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 681 | \path[->] (q12) edge node [below]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 682 | \path[->] (q02) edge node [above]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 683 | \path[->] (q02) edge [bend left] node [above, pos=0.8]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 684 | \path[->] (q01) edge node [below]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 685 | \path[->] (q01) edge [bend left] node [above]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 686 | \path[->] (q0) edge node [below]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 687 | \path[->] (q0) edge node [right, pos=0.2]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 688 | \path[->] (q1) edge [loop above] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 689 | \path[->] (q1) edge node [above]  {$b$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 690 | \path[->] (q2) edge [loop right] node  {$b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 691 | \path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 692 | \path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 693 | \end{tikzpicture}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 694 | \end{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 695 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 696 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 697 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 698 | There are two points to note: One is that very often the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 699 | resulting DFA contains a number of ``dead'' nodes that are | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 700 | never reachable from the starting state. For example | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 701 | there is no way to reach node $\{0,2\}$ from the starting
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 702 | state $\{0,1,2\}$. I let you find the other dead states.
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 703 | In effect the DFA in this example is not a minimal DFA. Such | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 704 | dead nodes can be safely removed without changing the language | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 705 | that is recognised by the DFA. Another point is that in some | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 706 | cases, however, the subset construction produces a DFA that | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 707 | does \emph{not} contain any dead nodes\ldots{}that means it
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 708 | calculates a minimal DFA. Which in turn means that in some | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 709 | cases the number of nodes by going from NFAs to DFAs | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 710 | exponentially increases, namely by $2^n$ (which is the number | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 711 | of subsets you can form for $n$ nodes). | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 712 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 713 | Removing all the dead states in the automaton above, | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 714 | gives a much more legible automaton, namely | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 715 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 716 | \begin{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 717 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 718 |                     every state/.style={minimum size=0pt,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 719 | draw=blue!50,very thick,fill=blue!20}, | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 720 | baseline=0mm] | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 721 | \node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 722 | \node[state,accepting] (q2) [right=of q012] {$2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 723 | \node[state] (qn) [right=of q2] {$\{\}$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 724 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 725 | \path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 726 | \path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 727 | \path[->] (q2) edge [loop below] node  {$b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 728 | \path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 729 | \path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 730 | \end{tikzpicture}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 731 | \end{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 732 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 733 | \noindent Now the big question is whether this DFA | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 734 | can recognise the same language as the NFA we started with. | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 735 | I let you ponder about this question. | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 736 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 737 | \subsubsection*{Brzozowski's Method}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 738 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 739 | As said before, we can also go into the other direction---from | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 740 | DFAs to regular expressions. Brzozowski's method calculates | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 741 | a regular expression using familiar transformations for | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 742 | solving equational systems. Consider the DFA: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 743 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 744 | \begin{center}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 745 | \begin{tikzpicture}[scale=1.5,>=stealth',very thick,auto,
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 746 |                     every state/.style={minimum size=0pt,
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 747 | inner sep=2pt,draw=blue!50,very thick, | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 748 | fill=blue!20}] | 
| 482 | 749 |   \node[state, initial]        (q0) at ( 0,1) {$Q_0$};
 | 
| 750 |   \node[state]                    (q1) at ( 1,1) {$Q_1$};
 | |
| 751 |   \node[state, accepting] (q2) at ( 2,1) {$Q_2$};
 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 752 |   \path[->] (q0) edge[bend left] node[above] {$a$} (q1)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 753 |             (q1) edge[bend left] node[above] {$b$} (q0)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 754 |             (q2) edge[bend left=50] node[below] {$b$} (q0)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 755 |             (q1) edge node[above] {$a$} (q2)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 756 |             (q2) edge [loop right] node {$a$} ()
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 757 |             (q0) edge [loop below] node {$b$} ();
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 758 | \end{tikzpicture}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 759 | \end{center}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 760 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 761 | \noindent for which we can set up the following equational | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 762 | system | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 763 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 764 | \begin{eqnarray}
 | 
| 482 | 765 | Q_0 & = & \ONE + Q_0\,b + Q_1\,b + Q_2\,b\\ | 
| 766 | Q_1 & = & Q_0\,a\\ | |
| 767 | Q_2 & = & Q_1\,a + Q_2\,a | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 768 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 769 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 770 | \noindent There is an equation for each node in the DFA. Let | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 771 | us have a look how the right-hand sides of the equations are | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 772 | constructed. First have a look at the second equation: the | 
| 482 | 773 | left-hand side is $Q_1$ and the right-hand side $Q_0\,a$. The | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 774 | right-hand side is essentially all possible ways how to end up | 
| 482 | 775 | in node $Q_1$. There is only one incoming edge from $Q_0$ consuming | 
| 322 
698ed1c96cd0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
318diff
changeset | 776 | an $a$. Therefore the right hand side is this | 
| 482 | 777 | state followed by character---in this case $Q_0\,a$. Now lets | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 778 | have a look at the third equation: there are two incoming | 
| 482 | 779 | edges for $Q_2$. Therefore we have two terms, namely $Q_1\,a$ and | 
| 780 | $Q_2\,a$. These terms are separated by $+$. The first states | |
| 781 | that if in state $Q_1$ consuming an $a$ will bring you to | |
| 782 | $Q_2$, and the secont that being in $Q_2$ and consuming an $a$ | |
| 783 | will make you stay in $Q_2$. The right-hand side of the | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 784 | first equation is constructed similarly: there are three | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 785 | incoming edges, therefore there are three terms. There is | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 786 | one exception in that we also ``add'' $\ONE$ to the | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 787 | first equation, because it corresponds to the starting state | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 788 | in the DFA. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 789 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 790 | Having constructed the equational system, the question is | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 791 | how to solve it? Remarkably the rules are very similar to | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 792 | solving usual linear equational systems. For example the | 
| 482 | 793 | second equation does not contain the variable $Q_1$ on the | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 794 | right-hand side of the equation. We can therefore eliminate | 
| 482 | 795 | $Q_1$ from the system by just substituting this equation | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 796 | into the other two. This gives | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 797 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 798 | \begin{eqnarray}
 | 
| 482 | 799 | Q_0 & = & \ONE + Q_0\,b + Q_0\,a\,b + Q_2\,b\\ | 
| 800 | Q_2 & = & Q_0\,a\,a + Q_2\,a | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 801 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 802 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 803 | \noindent where in Equation (4) we have two occurences | 
| 482 | 804 | of $Q_0$. Like the laws about $+$ and $\cdot$, we can simplify | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 805 | Equation (4) to obtain the following two equations: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 806 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 807 | \begin{eqnarray}
 | 
| 482 | 808 | Q_0 & = & \ONE + Q_0\,(b + a\,b) + Q_2\,b\\ | 
| 809 | Q_2 & = & Q_0\,a\,a + Q_2\,a | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 810 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 811 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 812 | \noindent Unfortunately we cannot make any more progress with | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 813 | substituting equations, because both (6) and (7) contain the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 814 | variable on the left-hand side also on the right-hand side. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 815 | Here we need to now use a law that is different from the usual | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 816 | laws about linear equations. It is called \emph{Arden's rule}.
 | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 817 | It states that if an equation is of the form $q = q\,r + s$ | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 818 | then it can be transformed to $q = s\, r^*$. Since we can | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 819 | assume $+$ is symmetric, Equation (7) is of that form: $s$ is | 
| 482 | 820 | $Q_0\,a\,a$ and $r$ is $a$. That means we can transform | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 821 | (7) to obtain the two new equations | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 822 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 823 | \begin{eqnarray}
 | 
| 482 | 824 | Q_0 & = & \ONE + Q_0\,(b + a\,b) + Q_2\,b\\ | 
| 825 | Q_2 & = & Q_0\,a\,a\,(a^*) | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 826 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 827 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 828 | \noindent Now again we can substitute the second equation into | 
| 482 | 829 | the first in order to eliminate the variable $Q_2$. | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 830 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 831 | \begin{eqnarray}
 | 
| 482 | 832 | Q_0 & = & \ONE + Q_0\,(b + a\,b) + Q_0\,a\,a\,(a^*)\,b | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 833 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 834 | |
| 482 | 835 | \noindent Pulling $Q_0$ out as a single factor gives: | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 836 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 837 | \begin{eqnarray}
 | 
| 482 | 838 | Q_0 & = & \ONE + Q_0\,(b + a\,b + a\,a\,(a^*)\,b) | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 839 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 840 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 841 | \noindent This equation is again of the form so that we can | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 842 | apply Arden's rule ($r$ is $b + a\,b + a\,a\,(a^*)\,b$ and $s$ | 
| 482 | 843 | is $\ONE$). This gives as solution for $Q_0$ the following | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 844 | regular expression: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 845 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 846 | \begin{eqnarray}
 | 
| 482 | 847 | Q_0 & = & \ONE\,(b + a\,b + a\,a\,(a^*)\,b)^* | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 848 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 849 | |
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 850 | \noindent Since this is a regular expression, we can simplify | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 851 | away the $\ONE$ to obtain the slightly simpler regular | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 852 | expression | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 853 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 854 | \begin{eqnarray}
 | 
| 482 | 855 | Q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^* | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 856 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 857 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 858 | \noindent | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 859 | Now we can unwind this process and obtain the solutions | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 860 | for the other equations. This gives: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 861 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 862 | \begin{eqnarray}
 | 
| 482 | 863 | Q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\\ | 
| 864 | Q_1 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\\ | |
| 865 | Q_2 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a)^* | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 866 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 867 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 868 | \noindent Finally, we only need to ``add'' up the equations | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 869 | which correspond to a terminal state. In our running example, | 
| 482 | 870 | this is just $Q_2$. Consequently, a regular expression | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 871 | that recognises the same language as the automaton is | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 872 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 873 | \[ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 874 | (b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a)^* | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 875 | \] | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 876 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 877 | \noindent You can somewhat crosscheck your solution | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 878 | by taking a string the regular expression can match and | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 879 | and see whether it can be matched by the automaton. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 880 | One string for example is $aaa$ and \emph{voila} this 
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 881 | string is also matched by the automaton. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 882 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 883 | We should prove that Brzozowski's method really produces | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 884 | an equivalent regular expression for the automaton. But | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 885 | for the purposes of this module, we omit this. | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 886 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 887 | \subsubsection*{Automata Minimization}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 888 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 889 | As seen in the subset construction, the translation | 
| 483 | 890 | of a NFA to a DFA can result in a rather ``inefficient'' | 
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 891 | DFA. Meaning there are states that are not needed. A | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 892 | DFA can be \emph{minimised} by the following algorithm:
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 893 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 894 | \begin{enumerate}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 895 | \item Take all pairs $(q, p)$ with $q \not= p$ | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 896 | \item Mark all pairs that accepting and non-accepting states | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 897 | \item For all unmarked pairs $(q, p)$ and all characters $c$ | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 898 | test whether | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 899 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 900 |       \begin{center} 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 901 | $(\delta(q, c), \delta(p,c))$ | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 902 |       \end{center} 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 903 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 904 | are marked. If there is one, then also mark $(q, p)$. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 905 | \item Repeat last step until no change. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 906 | \item All unmarked pairs can be merged. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 907 | \end{enumerate}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 908 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 909 | \noindent To illustrate this algorithm, consider the following | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 910 | DFA. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 911 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 912 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 913 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 914 |                     every state/.style={minimum size=0pt,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 915 | inner sep=2pt,draw=blue!50,very thick, | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 916 | fill=blue!20}] | 
| 482 | 917 | \node[state,initial]  (Q_0)  {$Q_0$};
 | 
| 918 | \node[state] (Q_1) [right=of Q_0] {$Q_1$};
 | |
| 919 | \node[state] (Q_2) [below right=of Q_0] {$Q_2$};
 | |
| 920 | \node[state] (Q_3) [right=of Q_2] {$Q_3$};
 | |
| 921 | \node[state, accepting] (Q_4) [right=of Q_1] {$Q_4$};
 | |
| 922 | \path[->] (Q_0) edge node [above]  {$a$} (Q_1);
 | |
| 923 | \path[->] (Q_1) edge node [above]  {$a$} (Q_4);
 | |
| 924 | \path[->] (Q_4) edge [loop right] node  {$a, b$} ();
 | |
| 925 | \path[->] (Q_3) edge node [right]  {$a$} (Q_4);
 | |
| 926 | \path[->] (Q_2) edge node [above]  {$a$} (Q_3);
 | |
| 927 | \path[->] (Q_1) edge node [right]  {$b$} (Q_2);
 | |
| 928 | \path[->] (Q_0) edge node [above]  {$b$} (Q_2);
 | |
| 929 | \path[->] (Q_2) edge [loop left] node  {$b$} ();
 | |
| 930 | \path[->] (Q_3) edge [bend left=95, looseness=1.3] node | |
| 931 |   [below]  {$b$} (Q_0);
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 932 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 933 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 934 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 935 | \noindent In Step 1 and 2 we consider essentially a triangle | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 936 | of the form | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 937 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 938 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 939 | \begin{tikzpicture}[scale=0.6,line width=0.8mm]
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 940 | \draw (0,0) -- (4,0); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 941 | \draw (0,1) -- (4,1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 942 | \draw (0,2) -- (3,2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 943 | \draw (0,3) -- (2,3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 944 | \draw (0,4) -- (1,4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 945 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 946 | \draw (0,0) -- (0, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 947 | \draw (1,0) -- (1, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 948 | \draw (2,0) -- (2, 3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 949 | \draw (3,0) -- (3, 2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 950 | \draw (4,0) -- (4, 1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 951 | |
| 482 | 952 | \draw (0.5,-0.5) node {$Q_0$}; 
 | 
| 953 | \draw (1.5,-0.5) node {$Q_1$}; 
 | |
| 954 | \draw (2.5,-0.5) node {$Q_2$}; 
 | |
| 955 | \draw (3.5,-0.5) node {$Q_3$};
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 956 | |
| 482 | 957 | \draw (-0.5, 3.5) node {$Q_1$}; 
 | 
| 958 | \draw (-0.5, 2.5) node {$Q_2$}; 
 | |
| 959 | \draw (-0.5, 1.5) node {$Q_3$}; 
 | |
| 960 | \draw (-0.5, 0.5) node {$Q_4$}; 
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 961 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 962 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 963 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 964 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 965 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 966 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 967 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 968 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 969 | \noindent where the lower row is filled with stars, because in | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 970 | the corresponding pairs there is always one state that is | 
| 482 | 971 | accepting ($Q_4$) and a state that is non-accepting (the other | 
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 972 | states). | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 973 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 974 | Now in Step 3 we need to fill in more stars according whether | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 975 | one of the next-state pairs are marked. We have to do this | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 976 | for every unmarked field until there is no change anymore. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 977 | This gives the triangle | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 978 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 979 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 980 | \begin{tikzpicture}[scale=0.6,line width=0.8mm]
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 981 | \draw (0,0) -- (4,0); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 982 | \draw (0,1) -- (4,1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 983 | \draw (0,2) -- (3,2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 984 | \draw (0,3) -- (2,3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 985 | \draw (0,4) -- (1,4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 986 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 987 | \draw (0,0) -- (0, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 988 | \draw (1,0) -- (1, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 989 | \draw (2,0) -- (2, 3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 990 | \draw (3,0) -- (3, 2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 991 | \draw (4,0) -- (4, 1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 992 | |
| 482 | 993 | \draw (0.5,-0.5) node {$Q_0$}; 
 | 
| 994 | \draw (1.5,-0.5) node {$Q_1$}; 
 | |
| 995 | \draw (2.5,-0.5) node {$Q_2$}; 
 | |
| 996 | \draw (3.5,-0.5) node {$Q_3$};
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 997 | |
| 482 | 998 | \draw (-0.5, 3.5) node {$Q_1$}; 
 | 
| 999 | \draw (-0.5, 2.5) node {$Q_2$}; 
 | |
| 1000 | \draw (-0.5, 1.5) node {$Q_3$}; 
 | |
| 1001 | \draw (-0.5, 0.5) node {$Q_4$}; 
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1002 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1003 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1004 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1005 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1006 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1007 | \draw (0.5,1.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1008 | \draw (2.5,1.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1009 | \draw (0.5,3.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1010 | \draw (1.5,2.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1011 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1012 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1013 | |
| 482 | 1014 | \noindent which means states $Q_0$ and $Q_2$, as well as $Q_1$ | 
| 1015 | and $Q_3$ can be merged. This gives the following minimal DFA | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1016 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1017 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1018 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1019 |                     every state/.style={minimum size=0pt,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1020 | inner sep=2pt,draw=blue!50,very thick, | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1021 | fill=blue!20}] | 
| 482 | 1022 | \node[state,initial]  (Q_02)  {$Q_{0, 2}$};
 | 
| 1023 | \node[state] (Q_13) [right=of Q_02] {$Q_{1, 3}$};
 | |
| 1024 | \node[state, accepting] (Q_4) [right=of Q_13] | |
| 1025 |   {$Q_{4\phantom{,0}}$};
 | |
| 1026 | \path[->] (Q_02) edge [bend left] node [above]  {$a$} (Q_13);
 | |
| 1027 | \path[->] (Q_13) edge [bend left] node [below]  {$b$} (Q_02);
 | |
| 1028 | \path[->] (Q_02) edge [loop below] node  {$b$} ();
 | |
| 1029 | \path[->] (Q_13) edge node [above]  {$a$} (Q_4);
 | |
| 1030 | \path[->] (Q_4) edge [loop above] node  {$a, b$} ();
 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1031 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1032 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1033 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1034 | \subsubsection*{Regular Languages}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1035 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1036 | Given the constructions in the previous sections we obtain | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1037 | the following overall picture: | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1038 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1039 | \begin{center}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1040 | \begin{tikzpicture}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1041 | \node (rexp)  {\bf Regexps};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1042 | \node (nfa) [right=of rexp] {\bf NFAs};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1043 | \node (dfa) [right=of nfa] {\bf DFAs};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1044 | \node (mdfa) [right=of dfa] {\bf\begin{tabular}{c}minimal\\ DFAs\end{tabular}};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1045 | \path[->,line width=1mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1046 | \path[->,line width=1mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1047 | \path[->,line width=1mm] (dfa) edge node [below=5mm, black] {minimisation} (mdfa);
 | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 1048 | \path[->,line width=1mm] (dfa) edge [bend left=45] node [below] {\begin{tabular}{l}Brzozowski's\\ method\end{tabular}} (rexp);
 | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1049 | \end{tikzpicture}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1050 | \end{center}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1051 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1052 | \noindent By going from regular expressions over NFAs to DFAs, | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1053 | we can always ensure that for every regular expression there | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1054 | exists a NFA and a DFA that can recognise the same language. | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1055 | Although we did not prove this fact. Similarly by going from | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1056 | DFAs to regular expressions, we can make sure for every DFA | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1057 | there exists a regular expression that can recognise the same | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1058 | language. Again we did not prove this fact. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1059 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1060 | The interesting conclusion is that automata and regular | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1061 | expressions can recognise the same set of languages: | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1062 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1063 | \begin{quote} A language is \emph{regular} iff there exists a
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1064 | regular expression that recognises all its strings. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1065 | \end{quote}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1066 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1067 | \noindent or equivalently | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1068 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1069 | \begin{quote} A language is \emph{regular} iff there exists an
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1070 | automaton that recognises all its strings. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1071 | \end{quote}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 1072 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1073 | \noindent So for deciding whether a string is recognised by a | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1074 | regular expression, we could use our algorithm based on | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1075 | derivatives or NFAs or DFAs. But let us quickly look at what | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1076 | the differences mean in computational terms. Translating a | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1077 | regular expression into a NFA gives us an automaton that has | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1078 | $O(n)$ nodes---that means the size of the NFA grows linearly | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1079 | with the size of the regular expression. The problem with NFAs | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1080 | is that the problem of deciding whether a string is accepted | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1081 | or not is computationally not cheap. Remember with NFAs we | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1082 | have potentially many next states even for the same input and | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1083 | also have the silent $\epsilon$-transitions. If we want to | 
| 483 | 1084 | find a path from the starting state of a NFA to an accepting | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1085 | state, we need to consider all possibilities. In Ruby and | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1086 | Python this is done by a depth-first search, which in turn | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1087 | means that if a ``wrong'' choice is made, the algorithm has to | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1088 | backtrack and thus explore all potential candidates. This is | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1089 | exactly the reason why Ruby and Python are so slow for evil | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1090 | regular expressions. An alternative to the potentially slow | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1091 | depth-first search is to explore the search space in a | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1092 | breadth-first fashion, but this might incur a big memory | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1093 | penalty. | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 1094 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1095 | To avoid the problems with NFAs, we can translate them | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1096 | into DFAs. With DFAs the problem of deciding whether a | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1097 | string is recognised or not is much simpler, because in | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1098 | each state it is completely determined what the next | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1099 | state will be for a given input. So no search is needed. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1100 | The problem with this is that the translation to DFAs | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1101 | can explode exponentially the number of states. Therefore when | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1102 | this route is taken, we definitely need to minimise the | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1103 | resulting DFAs in order to have an acceptable memory | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 1104 | and runtime behaviour. But remember the subset construction | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 1105 | in the worst case explodes the number of states by $2^n$. | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1106 | Effectively also the translation to DFAs can incur a big | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1107 | runtime penalty. | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1108 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1109 | But this does not mean that everything is bad with automata. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1110 | Recall the problem of finding a regular expressions for the | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1111 | language that is \emph{not} recognised by a regular
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1112 | expression. In our implementation we added explicitly such a | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1113 | regular expressions because they are useful for recognising | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1114 | comments. But in principle we did not need to. The argument | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 1115 | for this is as follows: take a regular expression, translate | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1116 | it into a NFA and then a DFA that both recognise the same | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1117 | language. Once you have the DFA it is very easy to construct | 
| 483 | 1118 | the automaton for the language not recognised by a DFA. If | 
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1119 | the DFA is completed (this is important!), then you just need | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1120 | to exchange the accepting and non-accepting states. You can | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1121 | then translate this DFA back into a regular expression and | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1122 | that will be the regular expression that can match all strings | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1123 | the original regular expression could \emph{not} match.
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 1124 | |
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1125 | It is also interesting that not all languages are regular. The | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1126 | most well-known example of a language that is not regular | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 1127 | consists of all the strings of the form | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1128 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1129 | \[a^n\,b^n\] | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1130 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1131 | \noindent meaning strings that have the same number of $a$s | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1132 | and $b$s. You can try, but you cannot find a regular | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1133 | expression for this language and also not an automaton. One | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1134 | can actually prove that there is no regular expression nor | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1135 | automaton for this language, but again that would lead us too | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 1136 | far afield for what we want to do in this module. | 
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1137 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 1138 | \section*{Further Reading}
 | 
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 1139 | |
| 471 | 1140 | Compare what a ``human expert'' would create as an automaton for the | 
| 333 
8890852e18b7
updated coursework
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
325diff
changeset | 1141 | regular expression $a (b + c)^*$ and what the Thomson | 
| 
8890852e18b7
updated coursework
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
325diff
changeset | 1142 | algorithm generates. | 
| 325 
794c599cee53
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
324diff
changeset | 1143 | |
| 
794c599cee53
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
324diff
changeset | 1144 | %http://www.inf.ed.ac.uk/teaching/courses/ct/ | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1145 | \end{document}
 | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1146 | |
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1147 | %%% Local Variables: | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1148 | %%% mode: latex | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1149 | %%% TeX-master: t | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1150 | %%% End: | 
| 482 | 1151 | |
| 1152 | ||
| 1153 | \noindent | |
| 1154 | Two typical examples of NFAs are | |
| 1155 | \begin{center}
 | |
| 1156 | \begin{tabular}[t]{c@{\hspace{9mm}}c}
 | |
| 1157 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | |
| 1158 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | |
| 1159 | \node[state,initial]  (Q_0)  {$Q_0$};
 | |
| 1160 | \node[state] (Q_1) [above=of Q_0] {$Q_1$};
 | |
| 1161 | \node[state, accepting] (Q_2) [below=of Q_0] {$Q_2$};
 | |
| 1162 | \path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_1);
 | |
| 1163 | \path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_2);
 | |
| 1164 | \path[->] (Q_0) edge [loop right] node  {$a$} ();
 | |
| 1165 | \path[->] (Q_1) edge [loop above] node  {$a$} ();
 | |
| 1166 | \path[->] (Q_2) edge [loop below] node  {$b$} ();
 | |
| 1167 | \end{tikzpicture} &
 | |
| 1168 | ||
| 1169 | \raisebox{20mm}{
 | |
| 1170 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | |
| 1171 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | |
| 1172 | \node[state,initial]  (r_1)  {$r_1$};
 | |
| 1173 | \node[state] (r_2) [above=of r_1] {$r_2$};
 | |
| 1174 | \node[state, accepting] (r_3) [right=of r_1] {$r_3$};
 | |
| 1175 | \path[->] (r_1) edge node [below]  {$b$} (r_3);
 | |
| 1176 | \path[->] (r_2) edge [bend left] node [above]  {$a$} (r_3);
 | |
| 1177 | \path[->] (r_1) edge [bend left] node  [left] {$\epsilon$} (r_2);
 | |
| 1178 | \path[->] (r_2) edge [bend left] node  [right] {$a$} (r_1);
 | |
| 1179 | \end{tikzpicture}}
 | |
| 1180 | \end{tabular}
 | |
| 1181 | \end{center}
 |