handouts/ho03.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 03 Nov 2014 16:17:58 +0000
changeset 296 796b9b81ac8d
parent 292 7ed2a25dd115
child 318 7975e4f0d4de
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
140
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\begin{document}
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
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
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
    20
regular expression matchers in Python and Ruby 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
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    27
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
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,
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    32
\item $\delta$ is the transition function.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    33
\end{itemize}
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    42
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    43
\begin{center}
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    48
\node[state,initial]  (q_0)  {$q_0$};
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
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$};
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
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
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);
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);
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$} ();
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);
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);
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);
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);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    60
\path[->] (q_2) edge [loop left] node  {$b$} ();
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);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    62
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    63
\end{center}
140
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    72
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    73
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    74
\begin{array}{lcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    75
(q_0, a) &\rightarrow& q_1\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    76
(q_0, b) &\rightarrow& q_2\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    77
(q_1, a) &\rightarrow& q_4\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    78
(q_1, b) &\rightarrow& q_2\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    79
(q_2, a) &\rightarrow& q_3\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    80
(q_2, b) &\rightarrow& q_2\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    81
(q_3, a) &\rightarrow& q_4\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    82
(q_3, b) &\rightarrow& q_0\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    83
(q_4, a) &\rightarrow& q_4\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    84
(q_4, b) &\rightarrow& q_4\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    85
\end{array}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    86
\]
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    91
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    92
\[
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
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)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    96
\end{array}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    97
\]
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   107
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   108
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   109
\hat{\delta}(q_0, s) \in F 
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   114
  
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   126
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   127
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   128
\item $Q$ is a finite set of states
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   129
\item $q_0$ is a start state
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   131
\item $\rho$ is a transition relation.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   132
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   133
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   134
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   135
Two typical examples of NFAs are
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   136
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   137
\begin{tabular}[t]{c@{\hspace{9mm}}c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   138
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
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},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   140
\node[state,initial]  (q_0)  {$q_0$};
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$};
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$};
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);
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);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   145
\path[->] (q_0) edge [loop right] node  {$a$} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   146
\path[->] (q_1) edge [loop above] node  {$a$} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   147
\path[->] (q_2) edge [loop below] node  {$b$} ();
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   148
\end{tikzpicture} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   149
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   150
\raisebox{20mm}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   151
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
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},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   153
\node[state,initial]  (r_1)  {$r_1$};
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$};
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$};
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);
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);
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);
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);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   160
\end{tikzpicture}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   161
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   162
\end{center}
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 
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   180
silently move either to $q_1$ or $q_2$.
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   181
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   182
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   183
\subsubsection*{Thompson Construction}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   184
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   185
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
   186
simple (recursive) translation of regular expressions into
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   187
NFAs. Consider the simple regular expressions $\varnothing$,
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   188
$\epsilon$ and $c$. They can be translated as follows:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   189
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   190
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   191
\begin{tabular}[t]{l@{\hspace{10mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   192
\raisebox{1mm}{$\varnothing$} & 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   193
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   194
\node[state, initial]  (q_0)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   195
\end{tikzpicture}\\\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   196
\raisebox{1mm}{$\epsilon$} & 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   197
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   198
\node[state, initial, accepting]  (q_0)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   199
\end{tikzpicture}\\\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   200
\raisebox{2mm}{$c$} & 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   201
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   202
\node[state, initial]  (q_0)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   203
\node[state, accepting]  (q_1)  [right=of q_0] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   204
\path[->] (q_0) edge node [below]  {$c$} (q_1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   205
\end{tikzpicture}\\\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   206
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   207
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   208
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   209
\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
   210
\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
   211
automata representing $r_1$ and $r_2$ respectively. 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   213
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   214
\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   215
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   216
\node[state, initial]  (q_0)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   217
\node (r_1)  [right=of q_0] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   218
\node[state, accepting]  (t_1)  [right=of r_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   219
\node[state, accepting]  (t_2)  [above=of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   220
\node[state, accepting]  (t_3)  [below=of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   221
\node[state, initial]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   222
\node (b_1)  [right=of a_0] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   223
\node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   224
\node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   225
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   226
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   227
\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)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   228
\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)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   229
\node [yshift=2mm] at (1.north) {$r_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   230
\node [yshift=2mm] at (2.north) {$r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   231
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   232
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   233
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   234
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   235
\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
   236
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
   237
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
   238
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
   239
non-accepting like so:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   240
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   241
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   242
\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   243
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   244
\node[state, initial]  (q_0)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   245
\node (r_1)  [right=of q_0] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   246
\node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   247
\node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   248
\node[state]  (t_3)  [below=of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   249
\node[state]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   250
\node (b_1)  [right=of a_0] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   251
\node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   252
\node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   253
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   254
\path[->] (t_1) edge node [above, pos=0.3]  {$\epsilon$} (a_0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   255
\path[->] (t_2) edge node [above]  {$\epsilon$} (a_0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   256
\path[->] (t_3) edge node [below]  {$\epsilon$} (a_0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   257
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   258
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   259
\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   260
\node [yshift=2mm] at (3.north) {$r_1\cdot r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   261
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   262
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   263
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   264
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   265
\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
   266
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
   267
automata representing $r_1$ and $r_2$ respectively. 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   268
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   269
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   270
\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   271
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   272
\node at (0,0)  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   273
\node[state, initial]  (2)  [above right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   274
\node[state, initial]  (3)  [below right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   275
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   276
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   277
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   278
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   279
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   280
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   281
\node (b)  [right=of 3] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   282
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   283
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   284
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   285
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   286
\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   287
\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   288
\node [yshift=3mm] at (1.north) {$r_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   289
\node [yshift=3mm] at (2.north) {$r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   290
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   291
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   292
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   293
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   294
\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
   295
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
   296
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
   297
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
   298
two starting states above, like so
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   299
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   300
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   301
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   302
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   303
\node at (0,0) [state, initial]  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   304
\node[state]  (2)  [above right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   305
\node[state]  (3)  [below right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   306
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   307
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   308
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   309
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   310
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   311
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   312
\node (b)  [right=of 3] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   313
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   314
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   315
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   316
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   317
\path[->] (1) edge node [above]  {$\epsilon$} (2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   318
\path[->] (1) edge node [below]  {$\epsilon$} (3);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   319
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   320
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   321
\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   322
\node [yshift=3mm] at (3.north) {$r_1+ r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   323
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   324
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   325
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   326
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   327
\noindent 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   328
Finally for the $*$-case we have an automaton for $r$
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   329
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   330
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   331
\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   332
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   333
\node at (0,0)  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   334
\node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   335
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   336
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   337
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   338
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   339
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   340
\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   341
\node [yshift=3mm] at (1.north) {$r$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   342
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   343
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   344
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   345
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   346
\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
   347
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
   348
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
   349
empty string. This gives the following automaton for $r^*$:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   350
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   351
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   352
\begin{tikzpicture}[node distance=3mm,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   353
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   354
\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   355
\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   356
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   357
\node[state]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   358
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   359
\node[state]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   360
\path[->] (1) edge node [above]  {$\epsilon$} (2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   361
\path[->] (a1) edge [bend left=45] node [above]  {$\epsilon$} (1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   362
\path[->] (a2) edge [bend right] node [below]  {$\epsilon$} (1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   363
\path[->] (a3) edge [bend left=45] node [below]  {$\epsilon$} (1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   364
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   365
\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   366
\node [yshift=3mm] at (2.north) {$r^*$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   367
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   368
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   369
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   370
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
   371
\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
   372
was invented by Ken Thompson in 1968.
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   373
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   374
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   375
\subsubsection*{Subset Construction}
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   376
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   377
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
   378
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
   379
done by the \emph{subset construction}. Consider again the NFA
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   380
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
   381
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   382
\begin{center}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   383
\begin{tabular}{c@{\hspace{10mm}}c}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   384
\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
   385
                    every state/.style={minimum size=0pt,
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   386
                    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
   387
                    baseline=0mm]
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   388
\node[state,initial]  (q_0)  {$0$};
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   389
\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
   390
\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
   391
\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
   392
\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
   393
\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
   394
\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
   395
\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
   396
\end{tikzpicture}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   397
&
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   398
\begin{tabular}{r|cl}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   399
nodes & $a$ & $b$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   400
\hline
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   401
$\varnothing\phantom{\star}$ & $\varnothing$ & $\varnothing$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   402
$\{0\}\phantom{\star}$       & $\{0,1,2\}$   & $\{2\}$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   403
$\{1\}\phantom{\star}$       & $\{1\}$       & $\varnothing$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   404
$\{2\}\star$  & $\varnothing$ & $\{2\}$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   405
$\{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
   406
$\{0,2\}\star$ & $\{0,1,2\}$   & $\{2\}$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   407
$\{1,2\}\star$ & $\{1\}$       & $\{2\}$\\
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   408
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
   409
\end{tabular}
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{center}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   412
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   413
\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
   414
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
   415
column on the right). The table shows the transition function
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   416
for the DFA. The first row states that $\varnothing$ is the
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   417
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
   418
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
   419
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   420
\begin{itemize}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   421
\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
   422
      $a$ and the node $\{0\}$
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   423
\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
   424
\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
   425
      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
   426
\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
   427
      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
   428
      $a$-transition
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   429
\item from the remaining set, do as many $\epsilon$-transition
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   430
      as you can, this yields $\{0,1,2\}$     
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   431
\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
   432
      when given an $a$ 
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   433
\end{itemize}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   434
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   435
\noindent Similarly for the other entries in the rows for
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   436
$\{0\}$, $\{1\}$ and $\{2\}$. The other rows are calculated by
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   437
just taking the union of the single node entries. For example
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   438
for $a$ and $\{0,1\}$ we need to take the union of $\{0,1,2\}$
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   439
(for $0$) and $\{1\}$ (for $1$). The starting state of the DFA
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   440
can be calculated from the starting state of the NFA, that is
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   441
$0$, and then do as many $\epsilon$-transitions as possible.
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   442
This gives $\{0,1,2\}$ which is the starting state of the DFA.
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   443
The terminal states in the DFA are given by all sets that
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   444
contain a $2$, which is the terminal state of the NFA. This
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   445
completes the subset construction.
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   446
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   447
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
   448
resulting DFA contains a number of ``dead'' nodes that are
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   449
never reachable from the starting state (that is that the
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   450
calculated DFA in this example is not a minimal DFA). Such
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   451
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
   452
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
   453
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
   454
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
   455
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
   456
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
   457
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
   458
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
   459
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   460
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   461
\subsubsection*{Brzozowski's Method}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   462
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   463
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
   464
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
   465
a regular expression using familiar transformations for
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   466
solving equational systems. Consider the DFA:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   467
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   468
\begin{center}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   469
\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
   470
                    every state/.style={minimum size=0pt,
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   471
                    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
   472
                    fill=blue!20}]
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   473
  \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
   474
  \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
   475
  \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
   476
  \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
   477
            (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
   478
            (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
   479
            (q1) edge node[above] {$a$} (q2)
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   480
            (q2) edge [loop right] node {$a$} ()
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   481
            (q0) edge [loop below] node {$b$} ();
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   482
\end{tikzpicture}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   483
\end{center}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   484
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   485
\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
   486
system
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   487
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   488
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   489
q_0 & = & \epsilon + q_0\,b + q_1\,b +  q_2\,b\\
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   490
q_1 & = & q_0\,a\\
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   491
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
   492
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   493
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   494
\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
   495
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
   496
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
   497
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
   498
right-hand side is essentially all possible ways how to end up
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   499
in $q_1$. There is only one incoming edge from $q_0$ consuming
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   500
an $a$. Therefore we say: if we are in $q_0$ consuming an $a$
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   501
then we end up in $q_1$. Therefore the right hand side is
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   502
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
   503
have a look at the third equation: there are two incoming
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   504
edges. Therefore we have two terms, namely $q_1\,a$ and
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   505
$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
   506
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
   507
$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
   508
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
   509
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
   510
incoming edges, therefore there are three terms. There is
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   511
one exception in that we also ``add'' $\epsilon$ to the
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   512
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
   513
in the DFA.
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   514
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   515
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
   516
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
   517
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
   518
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
   519
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
   520
$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
   521
into the other two. This gives
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   522
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   523
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   524
q_0 & = & \epsilon + q_0\,b + q_0\,a\,b +  q_2\,b\\
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   525
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
   526
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   527
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   528
\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
   529
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
   530
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
   531
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   532
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   533
q_0 & = & \epsilon + q_0\,(b + a\,b) +  q_2\,b\\
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   534
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
   535
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   536
 
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   537
\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
   538
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
   539
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
   540
Here we need to now use a law that is different from the usual
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   541
laws. It is called \emph{Arden's rule}. It states that
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   542
if an equation is of the form $q = q\,r + s$ then it can be
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   543
transformed to $q = s\, r^*$. Since we can assume $+$ is 
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   544
symmetric, equation (7) is of that form: $s$ is $q_0\,a\,a$
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   545
and $r$ is $a$. That means we can transform Equation (7)
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   546
to obtain the two new equations
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
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   549
q_0 & = & \epsilon + q_0\,(b + a\,b) +  q_2\,b\\
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   550
q_2 & = & q_0\,a\,a\,(a^*)
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   551
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   552
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   553
\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
   554
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
   555
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   556
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   557
q_0 & = & \epsilon + q_0\,(b + a\,b) +  q_0\,a\,a\,(a^*)\,b
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   558
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   559
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   560
\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
   561
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   562
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   563
q_0 & = & \epsilon + 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
   564
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   565
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   566
\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
   567
apply Arden's rule ($r$ is $b + a\,b + a\,a\,(a^*)\,b$ and $s$
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   568
is $\epsilon$). This gives as solution for $q_0$ the following
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   569
regular expression:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   570
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   571
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   572
q_0 & = & \epsilon\,(b + a\,b + a\,a\,(a^*)\,b)^*
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   573
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   574
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   575
\noindent SInce this is a regular expression, we can simplify
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   576
away the $\epsilon$ to obtain the slightly simpler regular
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   577
expression
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   578
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   579
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   580
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
   581
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   582
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   583
\noindent 
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   584
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
   585
for the other equations. This gives:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   586
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   587
\begin{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   588
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
   589
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
   590
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
   591
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   592
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   593
\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
   594
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
   595
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
   596
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
   597
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
(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
   600
\]
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   601
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   602
\noindent You can somewhat crosscheck your solution
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   603
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
   604
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
   605
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
   606
string is also matched by the automaton.
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   607
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   608
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
   609
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
   610
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
   611
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   612
\subsubsection*{Automata Minimization}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   613
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   614
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
   615
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
   616
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
   617
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
   618
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   619
\begin{enumerate}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   620
\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
   621
\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
   622
\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
   623
      test whether 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   624
      
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   625
      \begin{center} 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   626
      $(\delta(q, c), \delta(p,c))$ 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   627
      \end{center} 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   628
      
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   629
      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
   630
\item Repeat last step until no change.
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   631
\item All unmarked pairs can be merged.
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   632
\end{enumerate}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   633
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   634
\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
   635
DFA.
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   636
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   637
\begin{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   638
\begin{tikzpicture}[>=stealth',very thick,auto,
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   639
                    every state/.style={minimum size=0pt,
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   640
                    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
   641
                    fill=blue!20}]
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   642
\node[state,initial]  (q_0)  {$q_0$};
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   643
\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
   644
\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
   645
\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
   646
\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
   647
\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
   648
\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
   649
\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
   650
\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
   651
\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
   652
\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
   653
\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
   654
\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
   655
\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
   656
  [below]  {$b$} (q_0);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   657
\end{tikzpicture}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   658
\end{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   659
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   660
\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
   661
of the form
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   662
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   663
\begin{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   664
\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
   665
\draw (0,0) -- (4,0);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   666
\draw (0,1) -- (4,1);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   667
\draw (0,2) -- (3,2);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   668
\draw (0,3) -- (2,3);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   669
\draw (0,4) -- (1,4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   670
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   671
\draw (0,0) -- (0, 4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   672
\draw (1,0) -- (1, 4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   673
\draw (2,0) -- (2, 3);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   674
\draw (3,0) -- (3, 2);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   675
\draw (4,0) -- (4, 1);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   676
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   677
\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
   678
\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
   679
\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
   680
\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
   681
 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   682
\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
   683
\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
   684
\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
   685
\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
   686
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   687
\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
   688
\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
   689
\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
   690
\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
   691
\end{tikzpicture}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   692
\end{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   693
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   694
\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
   695
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
   696
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
   697
states).
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
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
   700
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
   701
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
   702
This gives the triangle
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   703
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   704
\begin{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   705
\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
   706
\draw (0,0) -- (4,0);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   707
\draw (0,1) -- (4,1);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   708
\draw (0,2) -- (3,2);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   709
\draw (0,3) -- (2,3);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   710
\draw (0,4) -- (1,4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   711
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   712
\draw (0,0) -- (0, 4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   713
\draw (1,0) -- (1, 4);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   714
\draw (2,0) -- (2, 3);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   715
\draw (3,0) -- (3, 2);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   716
\draw (4,0) -- (4, 1);
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   717
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   718
\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
   719
\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
   720
\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
   721
\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
   722
 
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   723
\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
   724
\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
   725
\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
   726
\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
   727
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   728
\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
   729
\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
   730
\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
   731
\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
   732
\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
   733
\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
   734
\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
   735
\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
   736
\end{tikzpicture}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   737
\end{center}
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
\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
   740
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
   741
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   742
\begin{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   743
\begin{tikzpicture}[>=stealth',very thick,auto,
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   744
                    every state/.style={minimum size=0pt,
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   745
                    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
   746
                    fill=blue!20}]
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   747
\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
   748
\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
   749
\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
   750
  {$q_{4\phantom{,0}}$};
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   751
\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
   752
\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
   753
\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
   754
\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
   755
\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
   756
\end{tikzpicture}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   757
\end{center}
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   758
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   759
\subsubsection*{Regular Languages}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   760
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   761
Given the constructions in the previous sections we obtain 
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   762
the following picture:
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   763
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   764
\begin{center}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   765
\begin{tikzpicture}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   766
\node (rexp)  {\bf Regexps};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   767
\node (nfa) [right=of rexp] {\bf NFAs};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   768
\node (dfa) [right=of nfa] {\bf DFAs};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   769
\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
   770
\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
   771
\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
   772
\path[->,line width=1mm] (dfa) edge node [below=5mm, black] {minimisation} (mdfa);
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   773
\path[->,line width=1mm] (dfa) edge [bend left=45] (rexp);
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   774
\end{tikzpicture}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   775
\end{center}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   776
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   777
\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
   778
we can always ensure that for every regular expression there
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   779
exists a NFA and DFA that can recognise the same language.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   780
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
   781
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
   782
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
   783
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
   784
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   785
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
   786
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
   787
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   788
\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
   789
regular expression that recognises all its strings.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   790
\end{quote}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   791
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   792
\noindent or equivalently 
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   793
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   794
\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
   795
automaton that recognises all its strings.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   796
\end{quote}
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   797
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   798
\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
   799
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
   800
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
   801
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
   802
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
   803
$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
   804
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
   805
is that the problem of deciding whether a string is accepted
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   806
is computationally not cheap. Remember with NFAs we have
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   807
potentially many next states even for the same input and also
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   808
have the silent $\epsilon$-transitions. If we want to find a
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   809
path from the starting state of an NFA to an accepting state,
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   810
we need to consider all possibilities. In Ruby and Python this
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   811
is done by a depth-first search, which in turn means that if a
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   812
``wrong'' choice is made, the algorithm has to backtrack and
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   813
thus explore all potential candidates. This is exactly the
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   814
reason why Ruby and Python are so slow for evil regular
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   815
expressions. The alternative is to explore the search space
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   816
in a breadth-first fashion, but this might incur a memory
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   817
penalty.  
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   818
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   819
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
   820
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
   821
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
   822
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
   823
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
   824
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
   825
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
   826
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
   827
resulting DFAs in order to have an acceptable memory 
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   828
and runtime behaviour.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   829
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   830
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
   831
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
   832
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
   833
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
   834
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
   835
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
   836
for this is as follows: take a regular expression, translate
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   837
it into a NFA and DFA that recognise the same language. Once
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   838
you have the DFA it is very easy to construct the automaton
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   839
for the language not recognised by an DFA. If the DAF is
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   840
completed (this is important!), then you just need to exchange
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   841
the accepting and non-accepting states. You can then translate
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   842
this DFA back into a regular expression. 
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   843
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   844
Not all languages are regular. The most well-known example
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   845
of a language that is not regular consists of all the strings
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   846
of the form
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   847
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   848
\[a^n\,b^n\]
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   849
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   850
\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
   851
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
   852
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
   853
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
   854
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
   855
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
   856
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   857
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   858
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   859
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   860
%%% Local Variables: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   861
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   862
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   863
%%% End: