| author | Christian Urban <urbanc@in.tum.de> | 
| Sat, 22 Oct 2016 15:18:11 +0100 | |
| changeset 459 | 858f62bc930a | 
| parent 444 | 3056a4c071b0 | 
| 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: 
217 
diff
changeset
 | 
2  | 
\usepackage{../style}
 | 
| 
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
changeset
 | 
3  | 
\usepackage{../langs}
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
21  | 
with certain regular expressions. The central definition  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
22  | 
is:\medskip  | 
| 
142
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
23  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
24  | 
\noindent  | 
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
141 
diff
changeset
 | 
27  | 
|
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
28  | 
\begin{itemize}
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
changeset
 | 
32  | 
\item $\delta$ is the transition function.  | 
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
33  | 
\end{itemize}
 | 
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
34  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
changeset
 | 
35  | 
\noindent The transition function determines how to  | 
| 
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
41  | 
typical example of a DFA is  | 
| 
142
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
42  | 
|
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
43  | 
\begin{center}
 | 
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
changeset
 | 
44  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
45  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
46  | 
inner sep=2pt,draw=blue!50,very thick,  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
47  | 
fill=blue!20},scale=2]  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
48  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
141 
diff
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: 
141 
diff
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: 
142 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
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: 
141 
diff
changeset
 | 
60  | 
\path[->] (q_2) edge [loop left] node  {$b$} ();
 | 
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
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: 
141 
diff
changeset
 | 
62  | 
\end{tikzpicture}
 | 
| 
 
1aa28135a2da
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
141 
diff
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: 
251 
diff
changeset
 | 
65  | 
\noindent In this graphical notation, the accepting state  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
71  | 
follows:  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
72  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
73  | 
\[  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
74  | 
\begin{array}{lcl}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
75  | 
(q_0, a) &\rightarrow& q_1\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
76  | 
(q_0, b) &\rightarrow& q_2\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
77  | 
(q_1, a) &\rightarrow& q_4\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
78  | 
(q_1, b) &\rightarrow& q_2\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
79  | 
(q_2, a) &\rightarrow& q_3\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
80  | 
(q_2, b) &\rightarrow& q_2\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
81  | 
(q_3, a) &\rightarrow& q_4\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
82  | 
(q_3, b) &\rightarrow& q_0\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
83  | 
(q_4, a) &\rightarrow& q_4\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
84  | 
(q_4, b) &\rightarrow& q_4\\  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
85  | 
\end{array}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
86  | 
\]  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
87  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
90  | 
$\delta$ from characters to strings as follows:  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
91  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
92  | 
\[  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
93  | 
\begin{array}{lcl}
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
94  | 
\hat{\delta}(q, [])        & \dn & q\\
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
96  | 
\end{array}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
97  | 
\]  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
98  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
99  | 
\noindent This lifted transition function is often called  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
142 
diff
changeset
 | 
107  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
108  | 
\[  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
109  | 
\hat{\delta}(q_0, s) \in F 
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
110  | 
\]  | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
111  | 
|
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
142 
diff
changeset
 | 
114  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
115  | 
|
| 
292
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
119  | 
potential successor states. We even allow ``silent  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
120  | 
transitions'', also called epsilon-transitions. They allow us  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
123  | 
$\epsilon$. The resulting construction is called a  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
142 
diff
changeset
 | 
126  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
127  | 
\begin{itemize}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
128  | 
\item $Q$ is a finite set of states  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
129  | 
\item $q_0$ is a start state  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
131  | 
\item $\rho$ is a transition relation.  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
132  | 
\end{itemize}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
133  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
134  | 
\noindent  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
135  | 
Two typical examples of NFAs are  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
136  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
137  | 
\begin{tabular}[t]{c@{\hspace{9mm}}c}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
138  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
140  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
145  | 
\path[->] (q_0) edge [loop right] node  {$a$} ();
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
146  | 
\path[->] (q_1) edge [loop above] node  {$a$} ();
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
147  | 
\path[->] (q_2) edge [loop below] node  {$b$} ();
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
148  | 
\end{tikzpicture} &
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
149  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
150  | 
\raisebox{20mm}{
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
151  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
153  | 
\node[state,initial]  (r_1)  {$r_1$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
160  | 
\end{tikzpicture}}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
161  | 
\end{tabular}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
162  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
163  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
182  | 
|
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
183  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
184  | 
\subsubsection*{Thompson Construction}
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
185  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
changeset
 | 
187  | 
simple (recursive) translation of regular expressions into  | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
changeset
 | 
188  | 
NFAs. Consider the simple regular expressions $\ZERO$,  | 
| 
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
142 
diff
changeset
 | 
190  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
191  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
192  | 
\begin{tabular}[t]{l@{\hspace{10mm}}l}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
changeset
 | 
193  | 
\raisebox{1mm}{$\ZERO$} & 
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
195  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
196  | 
\end{tikzpicture}\\\\
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
changeset
 | 
197  | 
\raisebox{1mm}{$\ONE$} & 
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
199  | 
\node[state, initial, accepting]  (q_0)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
200  | 
\end{tikzpicture}\\\\
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
201  | 
\raisebox{2mm}{$c$} & 
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
203  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
206  | 
\end{tikzpicture}\\\\
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
207  | 
\end{tabular}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
208  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
209  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
217 
diff
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: 
142 
diff
changeset
 | 
213  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
214  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
215  | 
\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
217  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
218  | 
\node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
223  | 
\node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
227  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
230  | 
\node [yshift=2mm] at (1.north) {$r_1$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
231  | 
\node [yshift=2mm] at (2.north) {$r_2$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
232  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
233  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
234  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
235  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
217 
diff
changeset
 | 
238  | 
accepting states with $\epsilon$-transitions to the starting  | 
| 
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
changeset
 | 
240  | 
non-accepting like so:  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
241  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
242  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
243  | 
\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
245  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
246  | 
\node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
251  | 
\node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
258  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
259  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
262  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
263  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
264  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
265  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
217 
diff
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: 
142 
diff
changeset
 | 
269  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
270  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
271  | 
\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
273  | 
\node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
276  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
277  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
278  | 
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
279  | 
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
280  | 
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
281  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
282  | 
\node (b)  [right=of 3] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
283  | 
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
284  | 
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
285  | 
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
286  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
289  | 
\node [yshift=3mm] at (1.north) {$r_1$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
290  | 
\node [yshift=3mm] at (2.north) {$r_2$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
291  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
292  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
293  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
294  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
217 
diff
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: 
217 
diff
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: 
217 
diff
changeset
 | 
299  | 
two starting states above, like so  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
300  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
301  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
302  | 
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
304  | 
\node at (0,0) [state, initial]  (1)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
307  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
308  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
309  | 
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
310  | 
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
311  | 
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
312  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
313  | 
\node (b)  [right=of 3] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
314  | 
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
315  | 
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
316  | 
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
317  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
318  | 
\path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
319  | 
\path[->] (1) edge node [below]  {$\epsilon$} (3);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
320  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
321  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
324  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
325  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
326  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
327  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
328  | 
\noindent  | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
330  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
331  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
332  | 
\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
334  | 
\node at (0,0)  (1)  {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
336  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
337  | 
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
338  | 
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
339  | 
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
340  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
342  | 
\node [yshift=3mm] at (1.north) {$r$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
343  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
344  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
345  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
346  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
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: 
251 
diff
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: 
217 
diff
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: 
142 
diff
changeset
 | 
351  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
352  | 
\begin{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
353  | 
\begin{tikzpicture}[node distance=3mm,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
356  | 
\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
357  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
358  | 
\node[state]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
359  | 
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
360  | 
\node[state]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
361  | 
\path[->] (1) edge node [above]  {$\epsilon$} (2);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
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: 
142 
diff
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: 
142 
diff
changeset
 | 
365  | 
\begin{pgfonlayer}{background}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
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: 
142 
diff
changeset
 | 
367  | 
\node [yshift=3mm] at (2.north) {$r^*$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
368  | 
\end{pgfonlayer}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
369  | 
\end{tikzpicture}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
370  | 
\end{center}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
371  | 
|
| 
251
 
5b5a68df6d16
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
217 
diff
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: 
217 
diff
changeset
 | 
373  | 
was invented by Ken Thompson in 1968.  | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
374  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
375  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
376  | 
\subsubsection*{Subset Construction}
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
377  | 
|
| 
292
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
333 
diff
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: 
251 
diff
changeset
 | 
382  | 
|
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
383  | 
\begin{center}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
384  | 
\begin{tabular}{c@{\hspace{10mm}}c}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
385  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
386  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
387  | 
draw=blue!50,very thick,fill=blue!20},  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
388  | 
baseline=0mm]  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
389  | 
\node[state,initial]  (q_0)  {$0$};
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
394  | 
\path[->] (q_0) edge [loop right] node  {$a$} ();
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
395  | 
\path[->] (q_1) edge [loop above] node  {$a$} ();
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
396  | 
\path[->] (q_2) edge [loop below] node  {$b$} ();
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
397  | 
\end{tikzpicture}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
398  | 
&  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
399  | 
\begin{tabular}{r|cl}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
400  | 
nodes & $a$ & $b$\\  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
401  | 
\hline  | 
| 
344
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
402  | 
$\{\}\phantom{\star}$ & $\{\}$ & $\{\}$\\
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
403  | 
$\{0\}\phantom{\star}$       & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
344
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
404  | 
$\{1\}\phantom{\star}$       & $\{1\}$       & $\{\}$\\
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
405  | 
$\{2\}\star$  & $\{\}$ & $\{2\}$\\
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
406  | 
$\{0,1\}\phantom{\star}$     & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
407  | 
$\{0,2\}\star$ & $\{0,1,2\}$   & $\{2\}$\\
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
408  | 
$\{1,2\}\star$ & $\{1\}$       & $\{2\}$\\
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
changeset
 | 
410  | 
\end{tabular}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
411  | 
\end{tabular}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
412  | 
\end{center}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
413  | 
|
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
333 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
419  | 
The next three lines are calculated as follows:  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
420  | 
|
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
421  | 
\begin{itemize}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
changeset
 | 
423  | 
      $a$ and the node $\{0\}$
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
429  | 
$a$-transition  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
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: 
333 
diff
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: 
251 
diff
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: 
251 
diff
changeset
 | 
433  | 
when given an $a$  | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
434  | 
\end{itemize}
 | 
| 
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
435  | 
|
| 
344
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
333 
diff
changeset
 | 
449  | 
above is  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
450  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
451  | 
\begin{center}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
452  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
453  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
454  | 
draw=blue!50,very thick,fill=blue!20},  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
455  | 
baseline=0mm]  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
456  | 
\node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
458  | 
\node[state] (q01) [above=of q02] {$0,1$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
460  | 
\node[state] (q0) [right=2cm of q01] {$0$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
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: 
333 
diff
changeset
 | 
463  | 
\node[state] (qn) [right=of q1] {$\{\}$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
464  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
465  | 
\path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
466  | 
\path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
468  | 
\path[->] (q12) edge node [below]  {$b$} (q2);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
469  | 
\path[->] (q02) edge node [above]  {$a$} (q012);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
471  | 
\path[->] (q01) edge node [below]  {$a$} (q012);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
473  | 
\path[->] (q0) edge node [below]  {$a$} (q012);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
475  | 
\path[->] (q1) edge [loop above] node  {$a$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
476  | 
\path[->] (q1) edge node [above]  {$b$} (qn);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
477  | 
\path[->] (q2) edge [loop right] node  {$b$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
478  | 
\path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
479  | 
\path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
480  | 
\end{tikzpicture}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
481  | 
\end{center}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
482  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
483  | 
|
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
484  | 
|
| 
292
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
333 
diff
changeset
 | 
487  | 
never reachable from the starting state. For example  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
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: 
333 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
251 
diff
changeset
 | 
499  | 
|
| 
344
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
changeset
 | 
501  | 
gives a much more legible automaton, namely  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
502  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
503  | 
\begin{center}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
504  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
505  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
506  | 
draw=blue!50,very thick,fill=blue!20},  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
507  | 
baseline=0mm]  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
508  | 
\node[state,initial,accepting]  (q012)  {$0,1,2$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
509  | 
\node[state,accepting] (q2) [right=of q012] {$2$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
510  | 
\node[state] (qn) [right=of q2] {$\{\}$};
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
511  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
512  | 
\path[->] (q012) edge [loop below] node  {$a$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
513  | 
\path[->] (q012) edge node [above]  {$b$} (q2);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
514  | 
\path[->] (q2) edge [loop below] node  {$b$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
515  | 
\path[->] (q2) edge node [below]  {$a$} (qn);
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
516  | 
\path[->] (qn) edge [loop above] node  {$a,b$} ();
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
517  | 
\end{tikzpicture}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
518  | 
\end{center}
 | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
519  | 
|
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
333 
diff
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: 
333 
diff
changeset
 | 
522  | 
I let you ponder about this question.  | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
523  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
524  | 
\subsubsection*{Brzozowski's Method}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
525  | 
|
| 
292
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
527  | 
DFAs to regular expressions. Brzozowski's method calculates  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
528  | 
a regular expression using familiar transformations for  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
529  | 
solving equational systems. Consider the DFA:  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
530  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
531  | 
\begin{center}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
533  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
534  | 
inner sep=2pt,draw=blue!50,very thick,  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
535  | 
fill=blue!20}]  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
537  | 
  \node[state]                    (q1) at ( 1,1) {$q_1$};
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
540  | 
            (q1) edge[bend left] node[above] {$b$} (q0)
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
542  | 
            (q1) edge node[above] {$a$} (q2)
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
543  | 
            (q2) edge [loop right] node {$a$} ()
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
544  | 
            (q0) edge [loop below] node {$b$} ();
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
545  | 
\end{tikzpicture}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
546  | 
\end{center}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
547  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
549  | 
system  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
550  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
551  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
changeset
 | 
553  | 
q_1 & = & q_0\,a\\  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
554  | 
q_2 & = & q_1\,a + q_2\,a  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
555  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
556  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
318 
diff
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: 
270 
diff
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: 
270 
diff
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: 
318 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
571  | 
first equation is constructed similarly: there are three  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
349 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
575  | 
in the DFA.  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
576  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
577  | 
Having constructed the equational system, the question is  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
579  | 
solving usual linear equational systems. For example the  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
583  | 
into the other two. This gives  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
584  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
585  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
588  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
589  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
592  | 
Equation (4) to obtain the following two equations:  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
593  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
594  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
597  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
598  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
changeset
 | 
608  | 
(7) to obtain the two new equations  | 
| 
292
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
609  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
610  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
changeset
 | 
612  | 
q_2 & = & q_0\,a\,a\,(a^*)  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
613  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
614  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
617  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
618  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
changeset
 | 
620  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
621  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
623  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
624  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
changeset
 | 
626  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
627  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
349 
diff
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: 
270 
diff
changeset
 | 
631  | 
regular expression:  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
632  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
633  | 
\begin{eqnarray}
 | 
| 
444
 
3056a4c071b0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
349 
diff
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: 
270 
diff
changeset
 | 
635  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
636  | 
|
| 
349
 
434891622131
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
344 
diff
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: 
349 
diff
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: 
270 
diff
changeset
 | 
639  | 
expression  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
640  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
641  | 
\begin{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
643  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
644  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
645  | 
\noindent  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
647  | 
for the other equations. This gives:  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
648  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
649  | 
\begin{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
653  | 
\end{eqnarray}
 | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
654  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
659  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
660  | 
\[  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
662  | 
\]  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
663  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
664  | 
\noindent You can somewhat crosscheck your solution  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
changeset
 | 
668  | 
string is also matched by the automaton.  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
669  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
changeset
 | 
671  | 
an equivalent regular expression for the automaton. But  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
268 
diff
changeset
 | 
673  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
674  | 
\subsubsection*{Automata Minimization}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
675  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
676  | 
As seen in the subset construction, the translation  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
680  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
681  | 
\begin{enumerate}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
685  | 
test whether  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
686  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
687  | 
      \begin{center} 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
688  | 
$(\delta(q, c), \delta(p,c))$  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
689  | 
      \end{center} 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
690  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
changeset
 | 
692  | 
\item Repeat last step until no change.  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
693  | 
\item All unmarked pairs can be merged.  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
694  | 
\end{enumerate}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
695  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
696  | 
\noindent To illustrate this algorithm, consider the following  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
697  | 
DFA.  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
698  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
699  | 
\begin{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
700  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
701  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
702  | 
inner sep=2pt,draw=blue!50,very thick,  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
703  | 
fill=blue!20}]  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
704  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
716  | 
\path[->] (q_2) edge [loop left] node  {$b$} ();
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
changeset
 | 
718  | 
  [below]  {$b$} (q_0);
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
719  | 
\end{tikzpicture}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
720  | 
\end{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
721  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
changeset
 | 
723  | 
of the form  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
724  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
725  | 
\begin{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
changeset
 | 
727  | 
\draw (0,0) -- (4,0);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
728  | 
\draw (0,1) -- (4,1);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
729  | 
\draw (0,2) -- (3,2);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
730  | 
\draw (0,3) -- (2,3);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
731  | 
\draw (0,4) -- (1,4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
732  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
733  | 
\draw (0,0) -- (0, 4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
734  | 
\draw (1,0) -- (1, 4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
735  | 
\draw (2,0) -- (2, 3);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
736  | 
\draw (3,0) -- (3, 2);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
737  | 
\draw (4,0) -- (4, 1);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
738  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
739  | 
\draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
740  | 
\draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
741  | 
\draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
742  | 
\draw (3.5,-0.5) node {$q_3$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
743  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
744  | 
\draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
745  | 
\draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
746  | 
\draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
747  | 
\draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
748  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
749  | 
\draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
750  | 
\draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
751  | 
\draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
752  | 
\draw (3.5,0.5) node {\large$\star$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
753  | 
\end{tikzpicture}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
754  | 
\end{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
755  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
759  | 
states).  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
760  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
764  | 
This gives the triangle  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
765  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
766  | 
\begin{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
changeset
 | 
768  | 
\draw (0,0) -- (4,0);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
769  | 
\draw (0,1) -- (4,1);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
770  | 
\draw (0,2) -- (3,2);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
771  | 
\draw (0,3) -- (2,3);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
772  | 
\draw (0,4) -- (1,4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
773  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
774  | 
\draw (0,0) -- (0, 4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
775  | 
\draw (1,0) -- (1, 4);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
776  | 
\draw (2,0) -- (2, 3);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
777  | 
\draw (3,0) -- (3, 2);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
778  | 
\draw (4,0) -- (4, 1);  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
779  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
780  | 
\draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
781  | 
\draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
782  | 
\draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
783  | 
\draw (3.5,-0.5) node {$q_3$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
784  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
785  | 
\draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
786  | 
\draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
787  | 
\draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
788  | 
\draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
789  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
790  | 
\draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
791  | 
\draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
792  | 
\draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
793  | 
\draw (3.5,0.5) node {\large$\star$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
794  | 
\draw (0.5,1.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
795  | 
\draw (2.5,1.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
796  | 
\draw (0.5,3.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
797  | 
\draw (1.5,2.5) node {\large$\star$}; 
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
798  | 
\end{tikzpicture}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
799  | 
\end{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
800  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
803  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
804  | 
\begin{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
805  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
806  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
807  | 
inner sep=2pt,draw=blue!50,very thick,  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
808  | 
fill=blue!20}]  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
809  | 
\node[state,initial]  (q_02)  {$q_{0, 2}$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
812  | 
  {$q_{4\phantom{,0}}$};
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
815  | 
\path[->] (q_02) edge [loop below] node  {$b$} ();
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
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: 
269 
diff
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: 
269 
diff
changeset
 | 
818  | 
\end{tikzpicture}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
819  | 
\end{center}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
820  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
821  | 
\subsubsection*{Regular Languages}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
822  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
344 
diff
changeset
 | 
824  | 
the following overall picture:  | 
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
825  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
826  | 
\begin{center}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
827  | 
\begin{tikzpicture}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
828  | 
\node (rexp)  {\bf Regexps};
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
829  | 
\node (nfa) [right=of rexp] {\bf NFAs};
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
830  | 
\node (dfa) [right=of nfa] {\bf DFAs};
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
333 
diff
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: 
268 
diff
changeset
 | 
836  | 
\end{tikzpicture}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
837  | 
\end{center}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
838  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
344 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
changeset
 | 
845  | 
language. Again we did not prove this fact.  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
846  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
847  | 
The interesting conclusion is that automata and regular  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
848  | 
expressions can recognise the same set of languages:  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
849  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
changeset
 | 
851  | 
regular expression that recognises all its strings.  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
852  | 
\end{quote}
 | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
853  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
854  | 
\noindent or equivalently  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
855  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
changeset
 | 
857  | 
automaton that recognises all its strings.  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
858  | 
\end{quote}
 | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
859  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
changeset
 | 
863  | 
the differences mean in computational terms. Translating a  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
changeset
 | 
877  | 
regular expressions. An alternative to the potentially slow  | 
| 
 
434891622131
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
344 
diff
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: 
344 
diff
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: 
268 
diff
changeset
 | 
880  | 
penalty.  | 
| 
268
 
18bef085a7ca
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
251 
diff
changeset
 | 
881  | 
|
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
333 
diff
changeset
 | 
891  | 
and runtime behaviour. But remember the subset construction  | 
| 
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
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: 
344 
diff
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: 
344 
diff
changeset
 | 
894  | 
runtime penalty.  | 
| 
269
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
changeset
 | 
895  | 
|
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
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: 
268 
diff
changeset
 | 
900  | 
regular expressions because they are useful for recognising  | 
| 
 
83e6cb90216d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
268 
diff
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: 
268 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
251 
diff
changeset
 | 
911  | 
|
| 
349
 
434891622131
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
344 
diff
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: 
344 
diff
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: 
344 
diff
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: 
270 
diff
changeset
 | 
915  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
916  | 
\[a^n\,b^n\]  | 
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
917  | 
|
| 
 
7ed2a25dd115
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
270 
diff
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: 
269 
diff
changeset
 | 
924  | 
|
| 
344
 
408fd5994288
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
333 
diff
changeset
 | 
925  | 
\section*{Further Reading}
 | 
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
269 
diff
changeset
 | 
926  | 
|
| 
333
 
8890852e18b7
updated coursework
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
325 
diff
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: 
325 
diff
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: 
325 
diff
changeset
 | 
929  | 
algorithm generates.  | 
| 
325
 
794c599cee53
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
324 
diff
changeset
 | 
930  | 
|
| 
 
794c599cee53
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
324 
diff
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:  |