| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Fri, 16 Dec 2016 11:13:41 +0000 | |
| changeset 470 | d6babe14a3a2 | 
| parent 459 | 858f62bc930a | 
| child 471 | e5df48ff7033 | 
| 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 | |
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 7 | \begin{document}
 | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 8 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 9 | \section*{Handout 3 (Automata)}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 10 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 11 | Every formal language course I know of bombards you first with | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 12 | automata and then to a much, much smaller extend with regular | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 13 | expressions. As you can see, this course is turned upside | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 14 | down: regular expressions come first. The reason is that | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 15 | regular expressions are easier to reason about and the notion | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 16 | of derivatives, although already quite old, only became more | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 17 | widely known rather recently. Still let us in this lecture | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 18 | have a closer look at automata and their relation to regular | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 19 | expressions. This will help us with understanding why the | 
| 459 | 20 | regular expression matchers in Python, Ruby and Java are so slow | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 21 | with certain regular expressions. The central definition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 22 | is:\medskip | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 23 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 24 | \noindent | 
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 25 | A \emph{deterministic finite automaton} (DFA), say $A$, is
 | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 26 | defined by a four-tuple written $A(Q, q_0, F, \delta)$ where | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 27 | |
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 28 | \begin{itemize}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 29 | \item $Q$ is a finite set of states, | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 30 | \item $q_0 \in Q$ is the start state, | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 31 | \item $F \subseteq Q$ are the accepting states, and | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 32 | \item $\delta$ is the transition function. | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 33 | \end{itemize}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 34 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 35 | \noindent The transition function determines how to | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 36 | ``transition'' from one state to the next state with respect | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 37 | to a character. We have the assumption that these transition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 38 | functions do not need to be defined everywhere: so it can be | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 39 | the case that given a character there is no next state, in | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 40 | which case we need to raise a kind of ``failure exception''. A | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 41 | typical example of a DFA is | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 42 | |
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 43 | \begin{center}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 44 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 45 |                     every state/.style={minimum size=0pt,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 46 | inner sep=2pt,draw=blue!50,very thick, | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 47 | fill=blue!20},scale=2] | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 48 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 49 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 50 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 51 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 52 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 142 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 53 | \path[->] (q_0) edge node [above]  {$a$} (q_1);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 54 | \path[->] (q_1) edge node [above]  {$a$} (q_4);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 55 | \path[->] (q_4) edge [loop right] node  {$a, b$} ();
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 56 | \path[->] (q_3) edge node [right]  {$a$} (q_4);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 57 | \path[->] (q_2) edge node [above]  {$a$} (q_3);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 58 | \path[->] (q_1) edge node [right]  {$b$} (q_2);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 59 | \path[->] (q_0) edge node [above]  {$b$} (q_2);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 60 | \path[->] (q_2) edge [loop left] node  {$b$} ();
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 61 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {$b$} (q_0);
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 62 | \end{tikzpicture}
 | 
| 
1aa28135a2da
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
141diff
changeset | 63 | \end{center}
 | 
| 140 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 64 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 65 | \noindent In this graphical notation, the accepting state | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 66 | $q_4$ is indicated with double circles. Note that there can be | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 67 | more than one accepting state. It is also possible that a DFA | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 68 | has no accepting states at all, or that the starting state is | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 69 | also an accepting state. In the case above the transition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 70 | function is defined everywhere and can be given as a table as | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 71 | follows: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 72 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 73 | \[ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 74 | \begin{array}{lcl}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 75 | (q_0, a) &\rightarrow& q_1\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 76 | (q_0, b) &\rightarrow& q_2\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 77 | (q_1, a) &\rightarrow& q_4\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 78 | (q_1, b) &\rightarrow& q_2\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 79 | (q_2, a) &\rightarrow& q_3\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 80 | (q_2, b) &\rightarrow& q_2\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 81 | (q_3, a) &\rightarrow& q_4\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 82 | (q_3, b) &\rightarrow& q_0\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 83 | (q_4, a) &\rightarrow& q_4\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 84 | (q_4, b) &\rightarrow& q_4\\ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 85 | \end{array}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 86 | \] | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 87 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 88 | 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 | 89 | 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 | 90 | $\delta$ from characters to strings as follows: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 91 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 92 | \[ | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 93 | \begin{array}{lcl}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 94 | \hat{\delta}(q, [])        & \dn & q\\
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 95 | \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 | 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 | \noindent This lifted transition function is often called | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 100 | ``delta-hat''. Given a string, we start in the starting state | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 101 | and take the first character of the string, follow to the next | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 102 | sate, then take the second character and so on. Once the | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 103 | string is exhausted and we end up in an accepting state, then | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 104 | this string is accepted by the automaton. Otherwise it is not | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 105 | accepted. So $s$ is in the \emph{language accepted by the
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 106 | automaton} $A(Q, q_0, F, \delta)$ iff | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 107 | |
| 
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 | \hat{\delta}(q_0, s) \in F 
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 110 | \] | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 111 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 112 | \noindent I let you think about a definition that describes | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 113 | the set of strings accepted by an automaton. | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 114 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 115 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 116 | While with DFAs it will always be clear that given a character | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 117 | what the next state is (potentially none), it will be useful | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 118 | to relax this restriction. That means we have several | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 119 | potential successor states. We even allow ``silent | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 120 | transitions'', also called epsilon-transitions. They allow us | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 121 | to go from one state to the next without having a character | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 122 | consumed. We label such silent transition with the letter | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 123 | $\epsilon$. The resulting construction is called a | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 124 | \emph{non-deterministic finite automaton} (NFA) given also as
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 125 | a four-tuple $A(Q, q_0, F, \rho)$ where | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 126 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 127 | \begin{itemize}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 128 | \item $Q$ is a finite set of states | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 129 | \item $q_0$ is a start state | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 130 | \item $F$ are some accepting states with $F \subseteq Q$, and | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 131 | \item $\rho$ is a transition relation. | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 132 | \end{itemize}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 133 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 134 | \noindent | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 135 | Two typical examples of NFAs are | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 136 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 137 | \begin{tabular}[t]{c@{\hspace{9mm}}c}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 138 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 139 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 140 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 141 | \node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 142 | \node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 143 | \path[->] (q_0) edge node [left]  {$\epsilon$} (q_1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 144 | \path[->] (q_0) edge node [left]  {$\epsilon$} (q_2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 145 | \path[->] (q_0) edge [loop right] node  {$a$} ();
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 146 | \path[->] (q_1) edge [loop above] node  {$a$} ();
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 147 | \path[->] (q_2) edge [loop below] node  {$b$} ();
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 148 | \end{tikzpicture} &
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 149 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 150 | \raisebox{20mm}{
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 151 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 152 |                              every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 153 | \node[state,initial]  (r_1)  {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 154 | \node[state] (r_2) [above=of r_1] {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 155 | \node[state, accepting] (r_3) [right=of r_1] {$r_3$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 156 | \path[->] (r_1) edge node [below]  {$b$} (r_3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 157 | \path[->] (r_2) edge [bend left] node [above]  {$a$} (r_3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 158 | \path[->] (r_1) edge [bend left] node  [left] {$\epsilon$} (r_2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 159 | \path[->] (r_2) edge [bend left] node  [right] {$a$} (r_1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 160 | \end{tikzpicture}}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 161 | \end{tabular}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 162 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 163 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 164 | \noindent There are, however, a number of points you should | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 165 | note. Every DFA is a NFA, but not vice versa. The $\rho$ in | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 166 | NFAs is a transition \emph{relation} (DFAs have a transition
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 167 | function). The difference between a function and a relation is | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 168 | that a function has always a single output, while a relation | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 169 | gives, roughly speaking, several outputs. Look at the NFA on | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 170 | the right-hand side above: if you are currently in the state | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 171 | $r_2$ and you read a character $a$, then you can transition to | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 172 | either $r_1$ \emph{or} $r_3$. Which route you take is not
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 173 | determined. This means if we need to decide whether a string | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 174 | is accepted by a NFA, we might have to explore all | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 175 | possibilities. Also there is the special silent transition in | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 176 | NFAs. As mentioned already this transition means you do not | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 177 | have to ``consume'' any part of the input string, but | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 178 | ``silently'' change to a different state. In the left picture, | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 179 | for example, if you are in the starting state, you can | 
| 459 | 180 | silently move either to $q_1$ or $q_2$. This silent | 
| 181 | transition is also often called \emph{$\epsilon$-transition}.
 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 182 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 183 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 184 | \subsubsection*{Thompson Construction}
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 185 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 186 | 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 | 187 | simple (recursive) translation of regular expressions into | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 188 | NFAs. Consider the simple regular expressions $\ZERO$, | 
| 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 189 | $\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 | 190 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 191 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 192 | \begin{tabular}[t]{l@{\hspace{10mm}}l}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 193 | \raisebox{1mm}{$\ZERO$} & 
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 194 | \begin{tikzpicture}[scale=0.7,>=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 | 195 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 196 | \end{tikzpicture}\\\\
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 197 | \raisebox{1mm}{$\ONE$} & 
 | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 198 | \begin{tikzpicture}[scale=0.7,>=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 | 199 | \node[state, initial, accepting]  (q_0)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 200 | \end{tikzpicture}\\\\
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 201 | \raisebox{2mm}{$c$} & 
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 202 | \begin{tikzpicture}[scale=0.7,>=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 | 203 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 204 | \node[state, accepting]  (q_1)  [right=of q_0] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 205 | \path[->] (q_0) edge node [below]  {$c$} (q_1);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 206 | \end{tikzpicture}\\\\
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 207 | \end{tabular}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 208 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 209 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 210 | \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 | 211 | \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 | 212 | 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 | 213 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 214 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 215 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 216 |                              >=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 | 217 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 218 | \node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 219 | \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 | 220 | \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 | 221 | \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 | 222 | \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 | 223 | \node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 224 | \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 | 225 | \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 | 226 | \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 | 227 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 228 | \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)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 229 | \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 | 230 | \node [yshift=2mm] at (1.north) {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 231 | \node [yshift=2mm] at (2.north) {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 232 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 233 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 234 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 235 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 236 | \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 | 237 | 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 | 238 | accepting states with $\epsilon$-transitions to the starting | 
| 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 239 | 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 | 240 | non-accepting like so: | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 241 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 242 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 243 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 244 |                              >=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 | 245 | \node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 246 | \node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 247 | \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 | 248 | \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 | 249 | \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 | 250 | \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 | 251 | \node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 252 | \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 | 253 | \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 | 254 | \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 | 255 | \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 | 256 | \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 | 257 | \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 | 258 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 259 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 260 | \node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 261 | \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 | 262 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 263 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 264 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 265 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 266 | \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 | 267 | 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 | 268 | 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 | 269 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 270 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 271 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 272 |                              >=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 | 273 | \node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 274 | \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 | 275 | \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 | 276 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 277 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 278 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 279 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 280 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 281 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 282 | \node (b)  [right=of 3] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 283 | \node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 284 | \node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 285 | \node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 286 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 287 | \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 | 288 | \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 | 289 | \node [yshift=3mm] at (1.north) {$r_1$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 290 | \node [yshift=3mm] at (2.north) {$r_2$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 291 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 292 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 293 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 294 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 295 | \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 | 296 | 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 | 297 | 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 | 298 | 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 | 299 | two starting states above, like so | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 300 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 301 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 302 | \hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 303 |                              >=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 | 304 | \node at (0,0) [state, initial]  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 305 | \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 | 306 | \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 | 307 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 308 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 309 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 310 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 311 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 312 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 313 | \node (b)  [right=of 3] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 314 | \node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 315 | \node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 316 | \node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 317 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 318 | \path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 319 | \path[->] (1) edge node [below]  {$\epsilon$} (3);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 320 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 321 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 322 | \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 | 323 | \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 | 324 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 325 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 326 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 327 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 328 | \noindent | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 329 | 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 | 330 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 331 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 332 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 333 |                              >=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 | 334 | \node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 335 | \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 | 336 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 337 | \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 338 | \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 339 | \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 340 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 341 | \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 | 342 | \node [yshift=3mm] at (1.north) {$r$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 343 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 344 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 345 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 346 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 347 | \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 | 348 | 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 | 349 | 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 | 350 | 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 | 351 | |
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 352 | \begin{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 353 | \begin{tikzpicture}[node distance=3mm,
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 354 |                              >=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 | 355 | \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 | 356 | \node[state]  (2)  [right=16mm of 1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 357 | \node (a)  [right=of 2] {$\ldots$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 358 | \node[state]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 359 | \node[state]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 360 | \node[state]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 361 | \path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 362 | \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 | 363 | \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 | 364 | \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 | 365 | \begin{pgfonlayer}{background}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 366 | \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 | 367 | \node [yshift=3mm] at (2.north) {$r^*$};
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 368 | \end{pgfonlayer}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 369 | \end{tikzpicture}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 370 | \end{center}
 | 
| 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 371 | |
| 251 
5b5a68df6d16
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
217diff
changeset | 372 | \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 | 373 | was invented by Ken Thompson in 1968. | 
| 143 
e3fd4c5995ef
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
142diff
changeset | 374 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 375 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 376 | \subsubsection*{Subset Construction}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 377 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 378 | 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 | 379 | 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 | 380 | 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 | 381 | 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 | 382 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 383 | \begin{center}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 384 | \begin{tabular}{c@{\hspace{10mm}}c}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 385 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 386 |                     every state/.style={minimum size=0pt,
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 387 | draw=blue!50,very thick,fill=blue!20}, | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 388 | baseline=0mm] | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 389 | \node[state,initial]  (q_0)  {$0$};
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 390 | \node[state] (q_1) [above=of q_0] {$1$};
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 391 | \node[state, accepting] (q_2) [below=of q_0] {$2$};
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 392 | \path[->] (q_0) edge node [left]  {$\epsilon$} (q_1);
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 393 | \path[->] (q_0) edge node [left]  {$\epsilon$} (q_2);
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 394 | \path[->] (q_0) edge [loop right] node  {$a$} ();
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 395 | \path[->] (q_1) edge [loop above] node  {$a$} ();
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 396 | \path[->] (q_2) edge [loop below] node  {$b$} ();
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 397 | \end{tikzpicture}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 398 | & | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 399 | \begin{tabular}{r|cl}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 400 | nodes & $a$ & $b$\\ | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 401 | \hline | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 402 | $\{\}\phantom{\star}$ & $\{\}$ & $\{\}$\\
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 403 | $\{0\}\phantom{\star}$       & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 404 | $\{1\}\phantom{\star}$       & $\{1\}$       & $\{\}$\\
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 405 | $\{2\}\star$  & $\{\}$ & $\{2\}$\\
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 406 | $\{0,1\}\phantom{\star}$     & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 407 | $\{0,2\}\star$ & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 408 | $\{1,2\}\star$ & $\{1\}$       & $\{2\}$\\
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 409 | 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 | 410 | \end{tabular}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 411 | \end{tabular}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 412 | \end{center}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 413 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 414 | \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 | 415 | 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 | 416 | 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 | 417 | 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 | 418 | 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 | 419 | The next three lines are calculated as follows: | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 420 | |
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 421 | \begin{itemize}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 422 | \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 | 423 |       $a$ and the node $\{0\}$
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 424 | \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 | 425 | \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 | 426 |       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 | 427 | \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 | 428 | 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 | 429 | $a$-transition | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 430 | \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 | 431 |       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 | 432 | \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 | 433 | when given an $a$ | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 434 | \end{itemize}
 | 
| 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 435 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 436 | \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 | 437 | $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 | 438 | 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 | 439 | 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 | 440 | 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 | 441 | 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 | 442 | $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 | 443 | 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 | 444 | $\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 | 445 | 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 | 446 | 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 | 447 | 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 | 448 | 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 | 449 | above is | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 450 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 451 | \begin{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 452 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 453 |                     every state/.style={minimum size=0pt,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 454 | draw=blue!50,very thick,fill=blue!20}, | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 455 | baseline=0mm] | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 456 | \node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 457 | \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 | 458 | \node[state] (q01) [above=of q02] {$0,1$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 459 | \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 | 460 | \node[state] (q0) [right=2cm of q01] {$0$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 461 | \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 | 462 | \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 | 463 | \node[state] (qn) [right=of q1] {$\{\}$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 464 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 465 | \path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 466 | \path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 467 | \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 | 468 | \path[->] (q12) edge node [below]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 469 | \path[->] (q02) edge node [above]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 470 | \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 | 471 | \path[->] (q01) edge node [below]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 472 | \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 | 473 | \path[->] (q0) edge node [below]  {$a$} (q012);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 474 | \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 | 475 | \path[->] (q1) edge [loop above] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 476 | \path[->] (q1) edge node [above]  {$b$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 477 | \path[->] (q2) edge [loop right] node  {$b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 478 | \path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 479 | \path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 480 | \end{tikzpicture}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 481 | \end{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 482 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 483 | |
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 484 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 485 | 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 | 486 | 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 | 487 | never reachable from the starting state. For example | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 488 | 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 | 489 | 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 | 490 | 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 | 491 | 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 | 492 | 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 | 493 | 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 | 494 | 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 | 495 | 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 | 496 | 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 | 497 | 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 | 498 | 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 | 499 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 500 | 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 | 501 | gives a much more legible automaton, namely | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 502 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 503 | \begin{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 504 | \begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 505 |                     every state/.style={minimum size=0pt,
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 506 | draw=blue!50,very thick,fill=blue!20}, | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 507 | baseline=0mm] | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 508 | \node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 509 | \node[state,accepting] (q2) [right=of q012] {$2$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 510 | \node[state] (qn) [right=of q2] {$\{\}$};
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 511 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 512 | \path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 513 | \path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 514 | \path[->] (q2) edge [loop below] node  {$b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 515 | \path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 516 | \path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 517 | \end{tikzpicture}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 518 | \end{center}
 | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 519 | |
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 520 | \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 | 521 | 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 | 522 | I let you ponder about this question. | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 523 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 524 | \subsubsection*{Brzozowski's Method}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 525 | |
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 526 | 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 | 527 | DFAs to regular expressions. Brzozowski's method calculates | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 528 | a regular expression using familiar transformations for | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 529 | solving equational systems. Consider the DFA: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 530 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 531 | \begin{center}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 532 | \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 | 533 |                     every state/.style={minimum size=0pt,
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 534 | inner sep=2pt,draw=blue!50,very thick, | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 535 | fill=blue!20}] | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 536 |   \node[state, initial]        (q0) at ( 0,1) {$q_0$};
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 537 |   \node[state]                    (q1) at ( 1,1) {$q_1$};
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 538 |   \node[state, accepting] (q2) at ( 2,1) {$q_2$};
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 539 |   \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 | 540 |             (q1) edge[bend left] node[above] {$b$} (q0)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 541 |             (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 | 542 |             (q1) edge node[above] {$a$} (q2)
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 543 |             (q2) edge [loop right] node {$a$} ()
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 544 |             (q0) edge [loop below] node {$b$} ();
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 545 | \end{tikzpicture}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 546 | \end{center}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 547 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 548 | \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 | 549 | system | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 550 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 551 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 552 | q_0 & = & \ONE + q_0\,b + q_1\,b + q_2\,b\\ | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 553 | q_1 & = & q_0\,a\\ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 554 | q_2 & = & q_1\,a + q_2\,a | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 555 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 556 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 557 | \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 | 558 | 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 | 559 | constructed. First have a look at the second equation: the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 560 | left-hand side is $q_1$ and the right-hand side $q_0\,a$. The | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 561 | right-hand side is essentially all possible ways how to end up | 
| 459 | 562 | 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 | 563 | an $a$. Therefore the right hand side is this | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 564 | state followed by character---in this case $q_0\,a$. Now lets | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 565 | have a look at the third equation: there are two incoming | 
| 322 
698ed1c96cd0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
318diff
changeset | 566 | edges for $q_2$. Therefore we have two terms, namely $q_1\,a$ and | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 567 | $q_2\,a$. These terms are separated by $+$. The first states | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 568 | that if in state $q_1$ consuming an $a$ will bring you to | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 569 | $q_2$, and the secont that being in $q_2$ and consuming an $a$ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 570 | will make you stay in $q_2$. The right-hand side of the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 571 | first equation is constructed similarly: there are three | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 572 | 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 | 573 | 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 | 574 | 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 | 575 | in the DFA. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 576 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 577 | Having constructed the equational system, the question is | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 578 | 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 | 579 | solving usual linear equational systems. For example the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 580 | second equation does not contain the variable $q_1$ on the | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 581 | right-hand side of the equation. We can therefore eliminate | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 582 | $q_1$ from the system by just substituting this equation | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 583 | into the other two. This gives | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 584 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 585 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 586 | q_0 & = & \ONE + q_0\,b + q_0\,a\,b + q_2\,b\\ | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 587 | q_2 & = & q_0\,a\,a + q_2\,a | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 588 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 589 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 590 | \noindent where in Equation (4) we have two occurences | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 591 | of $q_0$. Like the laws about $+$ and $\cdot$, we can simplify | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 592 | Equation (4) to obtain the following two equations: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 593 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 594 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 595 | q_0 & = & \ONE + q_0\,(b + a\,b) + q_2\,b\\ | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 596 | q_2 & = & q_0\,a\,a + q_2\,a | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 597 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 598 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 599 | \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 | 600 | 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 | 601 | 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 | 602 | 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 | 603 | 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 | 604 | 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 | 605 | 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 | 606 | assume $+$ is symmetric, Equation (7) is of that form: $s$ is | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 607 | $q_0\,a\,a$ and $r$ is $a$. That means we can transform | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 608 | (7) to obtain the two new equations | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 609 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 610 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 611 | q_0 & = & \ONE + q_0\,(b + a\,b) + q_2\,b\\ | 
| 292 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 612 | q_2 & = & q_0\,a\,a\,(a^*) | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 613 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 614 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 615 | \noindent Now again we can substitute the second equation into | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 616 | the first in order to eliminate the variable $q_2$. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 617 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 618 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 619 | 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 | 620 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 621 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 622 | \noindent Pulling $q_0$ out as a single factor gives: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 623 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 624 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 625 | 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 | 626 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 627 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 628 | \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 | 629 | apply Arden's rule ($r$ is $b + a\,b + a\,a\,(a^*)\,b$ and $s$ | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 630 | 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 | 631 | regular expression: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 632 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 633 | \begin{eqnarray}
 | 
| 444 
3056a4c071b0
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
349diff
changeset | 634 | 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 | 635 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 636 | |
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 637 | \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 | 638 | 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 | 639 | expression | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 640 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 641 | \begin{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 642 | q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^* | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 643 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 644 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 645 | \noindent | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 646 | 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 | 647 | for the other equations. This gives: | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 648 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 649 | \begin{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 650 | q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\\ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 651 | q_1 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\\ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 652 | q_2 & = & (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 | 653 | \end{eqnarray}
 | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 654 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 655 | \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 | 656 | which correspond to a terminal state. In our running example, | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 657 | this is just $q_2$. Consequently, a regular expression | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 658 | 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 | 659 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 660 | \[ | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 661 | (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 | 662 | \] | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 663 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 664 | \noindent You can somewhat crosscheck your solution | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 665 | 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 | 666 | 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 | 667 | 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 | 668 | string is also matched by the automaton. | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 669 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 670 | 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 | 671 | an equivalent regular expression for the automaton. But | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 672 | 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 | 673 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 674 | \subsubsection*{Automata Minimization}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 675 | |
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 676 | As seen in the subset construction, the translation | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 677 | of an NFA to a DFA can result in a rather ``inefficient'' | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 678 | 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 | 679 | 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 | 680 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 681 | \begin{enumerate}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 682 | \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 | 683 | \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 | 684 | \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 | 685 | test whether | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 686 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 687 |       \begin{center} 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 688 | $(\delta(q, c), \delta(p,c))$ | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 689 |       \end{center} 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 690 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 691 | 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 | 692 | \item Repeat last step until no change. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 693 | \item All unmarked pairs can be merged. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 694 | \end{enumerate}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 695 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 696 | \noindent To illustrate this algorithm, consider the following | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 697 | DFA. | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 698 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 699 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 700 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 701 |                     every state/.style={minimum size=0pt,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 702 | inner sep=2pt,draw=blue!50,very thick, | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 703 | fill=blue!20}] | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 704 | \node[state,initial]  (q_0)  {$q_0$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 705 | \node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 706 | \node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 707 | \node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 708 | \node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 709 | \path[->] (q_0) edge node [above]  {$a$} (q_1);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 710 | \path[->] (q_1) edge node [above]  {$a$} (q_4);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 711 | \path[->] (q_4) edge [loop right] node  {$a, b$} ();
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 712 | \path[->] (q_3) edge node [right]  {$a$} (q_4);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 713 | \path[->] (q_2) edge node [above]  {$a$} (q_3);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 714 | \path[->] (q_1) edge node [right]  {$b$} (q_2);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 715 | \path[->] (q_0) edge node [above]  {$b$} (q_2);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 716 | \path[->] (q_2) edge [loop left] node  {$b$} ();
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 717 | \path[->] (q_3) edge [bend left=95, looseness=1.3] node | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 718 |   [below]  {$b$} (q_0);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 719 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 720 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 721 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 722 | \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 | 723 | of the form | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 724 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 725 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 726 | \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 | 727 | \draw (0,0) -- (4,0); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 728 | \draw (0,1) -- (4,1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 729 | \draw (0,2) -- (3,2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 730 | \draw (0,3) -- (2,3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 731 | \draw (0,4) -- (1,4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 732 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 733 | \draw (0,0) -- (0, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 734 | \draw (1,0) -- (1, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 735 | \draw (2,0) -- (2, 3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 736 | \draw (3,0) -- (3, 2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 737 | \draw (4,0) -- (4, 1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 738 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 739 | \draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 740 | \draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 741 | \draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 742 | \draw (3.5,-0.5) node {$q_3$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 743 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 744 | \draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 745 | \draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 746 | \draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 747 | \draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 748 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 749 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 750 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 751 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 752 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 753 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 754 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 755 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 756 | \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 | 757 | the corresponding pairs there is always one state that is | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 758 | accepting ($q_4$) and a state that is non-accepting (the other | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 759 | states). | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 760 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 761 | 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 | 762 | 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 | 763 | 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 | 764 | This gives the triangle | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 765 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 766 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 767 | \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 | 768 | \draw (0,0) -- (4,0); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 769 | \draw (0,1) -- (4,1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 770 | \draw (0,2) -- (3,2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 771 | \draw (0,3) -- (2,3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 772 | \draw (0,4) -- (1,4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 773 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 774 | \draw (0,0) -- (0, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 775 | \draw (1,0) -- (1, 4); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 776 | \draw (2,0) -- (2, 3); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 777 | \draw (3,0) -- (3, 2); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 778 | \draw (4,0) -- (4, 1); | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 779 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 780 | \draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 781 | \draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 782 | \draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 783 | \draw (3.5,-0.5) node {$q_3$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 784 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 785 | \draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 786 | \draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 787 | \draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 788 | \draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 789 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 790 | \draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 791 | \draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 792 | \draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 793 | \draw (3.5,0.5) node {\large$\star$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 794 | \draw (0.5,1.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 795 | \draw (2.5,1.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 796 | \draw (0.5,3.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 797 | \draw (1.5,2.5) node {\large$\star$}; 
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 798 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 799 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 800 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 801 | \noindent which means states $q_0$ and $q_2$, as well as $q_1$ | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 802 | and $q_3$ can be merged. This gives the following minimal DFA | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 803 | |
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 804 | \begin{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 805 | \begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 806 |                     every state/.style={minimum size=0pt,
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 807 | inner sep=2pt,draw=blue!50,very thick, | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 808 | fill=blue!20}] | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 809 | \node[state,initial]  (q_02)  {$q_{0, 2}$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 810 | \node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 811 | \node[state, accepting] (q_4) [right=of q_13] | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 812 |   {$q_{4\phantom{,0}}$};
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 813 | \path[->] (q_02) edge [bend left] node [above]  {$a$} (q_13);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 814 | \path[->] (q_13) edge [bend left] node [below]  {$b$} (q_02);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 815 | \path[->] (q_02) edge [loop below] node  {$b$} ();
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 816 | \path[->] (q_13) edge node [above]  {$a$} (q_4);
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 817 | \path[->] (q_4) edge [loop above] node  {$a, b$} ();
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 818 | \end{tikzpicture}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 819 | \end{center}
 | 
| 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 820 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 821 | \subsubsection*{Regular Languages}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 822 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 823 | 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 | 824 | the following overall picture: | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 825 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 826 | \begin{center}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 827 | \begin{tikzpicture}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 828 | \node (rexp)  {\bf Regexps};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 829 | \node (nfa) [right=of rexp] {\bf NFAs};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 830 | \node (dfa) [right=of nfa] {\bf DFAs};
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 831 | \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 | 832 | \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 | 833 | \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 | 834 | \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 | 835 | \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 | 836 | \end{tikzpicture}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 837 | \end{center}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 838 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 839 | \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 | 840 | 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 | 841 | 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 | 842 | 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 | 843 | 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 | 844 | 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 | 845 | language. Again we did not prove this fact. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 846 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 847 | The interesting conclusion is that automata and regular | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 848 | expressions can recognise the same set of languages: | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 849 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 850 | \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 | 851 | regular expression that recognises all its strings. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 852 | \end{quote}
 | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 853 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 854 | \noindent or equivalently | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 855 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 856 | \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 | 857 | automaton that recognises all its strings. | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 858 | \end{quote}
 | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 859 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 860 | \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 | 861 | 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 | 862 | 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 | 863 | the differences mean in computational terms. Translating a | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 864 | 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 | 865 | $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 | 866 | 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 | 867 | 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 | 868 | 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 | 869 | 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 | 870 | also have the silent $\epsilon$-transitions. If we want to | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 871 | find a path from the starting state of an NFA to an accepting | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 872 | 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 | 873 | 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 | 874 | 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 | 875 | 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 | 876 | 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 | 877 | regular expressions. An alternative to the potentially slow | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 878 | 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 | 879 | 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 | 880 | penalty. | 
| 268 
18bef085a7ca
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
251diff
changeset | 881 | |
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 882 | 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 | 883 | 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 | 884 | 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 | 885 | 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 | 886 | 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 | 887 | 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 | 888 | 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 | 889 | 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 | 890 | 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 | 891 | and runtime behaviour. But remember the subset construction | 
| 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 892 | 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 | 893 | 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 | 894 | runtime penalty. | 
| 269 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 895 | |
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 896 | 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 | 897 | 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 | 898 | 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 | 899 | 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 | 900 | regular expressions because they are useful for recognising | 
| 
83e6cb90216d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
268diff
changeset | 901 | 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 | 902 | 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 | 903 | 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 | 904 | language. Once you have the DFA it is very easy to construct | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 905 | the automaton for the language not recognised by an DFA. If | 
| 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 906 | 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 | 907 | 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 | 908 | 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 | 909 | 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 | 910 | 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 | 911 | |
| 349 
434891622131
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
344diff
changeset | 912 | 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 | 913 | 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 | 914 | 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 | 915 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 916 | \[a^n\,b^n\] | 
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 917 | |
| 
7ed2a25dd115
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
270diff
changeset | 918 | \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 | 919 | 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 | 920 | 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 | 921 | 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 | 922 | 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 | 923 | 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 | 924 | |
| 344 
408fd5994288
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
333diff
changeset | 925 | \section*{Further Reading}
 | 
| 270 
4dbeaf43031d
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
269diff
changeset | 926 | |
| 333 
8890852e18b7
updated coursework
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
325diff
changeset | 927 | Compare what a ``human expert'' would create as automaton for the | 
| 
8890852e18b7
updated coursework
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
325diff
changeset | 928 | 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 | 929 | algorithm generates. | 
| 325 
794c599cee53
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
324diff
changeset | 930 | |
| 
794c599cee53
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
324diff
changeset | 931 | %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 | 932 | \end{document}
 | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 933 | |
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 934 | %%% Local Variables: | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 935 | %%% mode: latex | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 936 | %%% TeX-master: t | 
| 
1be892087df2
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 937 | %%% End: |