handouts/ho03.tex
author Christian Urban <urbanc@in.tum.de>
Tue, 09 May 2017 12:31:55 +0100
changeset 490 4fee50f38305
parent 489 e28d7a327870
child 491 d5776c6018f0
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
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
     6
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\begin{document}
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
     8
\fnote{\copyright{} Christian Urban, King's College London, 2014, 2015, 2016, 2017}
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    10
\section*{Handout 3 (Finite Automata)}
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    12
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    13
Every formal language and compiler course I know of bombards you first
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    14
with automata and then to a much, much smaller extend with regular
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    15
expressions. As you can see, this course is turned upside down:
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    16
regular expressions come first. The reason is that regular expressions
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    17
are easier to reason about and the notion of derivatives, although
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    18
already quite old, only became more widely known rather
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    19
recently. Still, let us in this lecture have a closer look at automata
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    20
and their relation to regular expressions. This will help us with
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
    21
understanding why the regular expression matchers in Python, Ruby and
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
    22
Java are so slow with certain regular expressions. On the way we will
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    23
also see what are the limitations of regular
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    24
expressions. Unfortunately, they cannot be used for \emph{everything}.
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    25
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    26
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    27
\subsection*{Deterministic Finite Automata}
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    28
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
    29
Lets start\ldots the central definition is:\medskip
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    30
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
    31
\noindent 
251
5b5a68df6d16 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
    32
A \emph{deterministic finite automaton} (DFA), say $A$, is
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
    33
given by a five-tuple written ${\cal A}(\varSigma, Qs, Q_0, F, \delta)$ where
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    34
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    35
\begin{itemize}
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
    36
\item $\varSigma$ is an alphabet,  
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    37
\item $Qs$ is a finite set of states,
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    38
\item $Q_0 \in Qs$ is the start state,
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    39
\item $F \subseteq Qs$ are the accepting states, and
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    40
\item $\delta$ is the transition function.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    41
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    42
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
    43
\noindent I am sure you have seen this definition already
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    44
before. The transition function determines how to ``transition'' from
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    45
one state to the next state with respect to a character. We have the
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    46
assumption that these transition functions do not need to be defined
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    47
everywhere: so it can be the case that given a character there is no
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
    48
next state, in which case we need to raise a kind of ``failure
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
    49
exception''.  That means actually we have \emph{partial} functions as
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
    50
transitions---see the Scala implementation of DFAs later on.  A
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
    51
typical example of a DFA is
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    52
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    53
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    54
\begin{tikzpicture}[>=stealth',very thick,auto,
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
    55
                    every state/.style={minimum size=0pt,
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
    56
                    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
    57
                    fill=blue!20},scale=2]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    58
\node[state,initial]  (Q_0)  {$Q_0$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    59
\node[state] (Q_1) [right=of Q_0] {$Q_1$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    60
\node[state] (Q_2) [below right=of Q_0] {$Q_2$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    61
\node[state] (Q_3) [right=of Q_2] {$Q_3$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    62
\node[state, accepting] (Q_4) [right=of Q_1] {$Q_4$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    63
\path[->] (Q_0) edge node [above]  {$a$} (Q_1);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    64
\path[->] (Q_1) edge node [above]  {$a$} (Q_4);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    65
\path[->] (Q_4) edge [loop right] node  {$a, b$} ();
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    66
\path[->] (Q_3) edge node [right]  {$a$} (Q_4);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    67
\path[->] (Q_2) edge node [above]  {$a$} (Q_3);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    68
\path[->] (Q_1) edge node [right]  {$b$} (Q_2);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    69
\path[->] (Q_0) edge node [above]  {$b$} (Q_2);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    70
\path[->] (Q_2) edge [loop left] node  {$b$} ();
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    71
\path[->] (Q_3) edge [bend left=95, looseness=1.3] node [below]  {$b$} (Q_0);
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    72
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 141
diff changeset
    73
\end{center}
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    75
\noindent In this graphical notation, the accepting state $Q_4$ is
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    76
indicated with double circles. Note that there can be more than one
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    77
accepting state. It is also possible that a DFA has no accepting
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
    78
state at all, or that the starting state is also an accepting
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    79
state. In the case above the transition function is defined everywhere
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    80
and can also be given as a table as follows:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    81
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    82
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    83
\begin{array}{lcl}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    84
(Q_0, a) &\rightarrow& Q_1\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    85
(Q_0, b) &\rightarrow& Q_2\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    86
(Q_1, a) &\rightarrow& Q_4\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    87
(Q_1, b) &\rightarrow& Q_2\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    88
(Q_2, a) &\rightarrow& Q_3\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    89
(Q_2, b) &\rightarrow& Q_2\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    90
(Q_3, a) &\rightarrow& Q_4\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    91
(Q_3, b) &\rightarrow& Q_0\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    92
(Q_4, a) &\rightarrow& Q_4\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
    93
(Q_4, b) &\rightarrow& Q_4\\
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    94
\end{array}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    95
\]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
    96
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
    97
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
    98
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
    99
$\delta$ from characters to strings as follows:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   100
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   101
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   102
\begin{array}{lcl}
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   103
\widehat{\delta}(q, [])        & \dn & q\\
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   104
\widehat{\delta}(q, c\!::\!s) & \dn & \widehat{\delta}(\delta(q, c), s)\\
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   105
\end{array}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   106
\]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   107
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   108
\noindent This lifted transition function is often called
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   109
\emph{delta-hat}. Given a string, we start in the starting state and
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   110
take the first character of the string, follow to the next state, then
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   111
take the second character and so on. Once the string is exhausted and
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   112
we end up in an accepting state, then this string is accepted by the
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   113
automaton. Otherwise it is not accepted. This also means that if along
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   114
the way we hit the case where the transition function $\delta$ is not
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   115
defined, we need to raise an error. In our implementation we will deal
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   116
with this case elegantly by using Scala's \texttt{Try}.  Summing up: a
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   117
string $s$ is in the \emph{language accepted by the automaton} ${\cal
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   118
  A}(\varSigma, Q, Q_0, F, \delta)$ iff
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   120
\[
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   121
\widehat{\delta}(Q_0, s) \in F 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   122
\]
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   123
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   124
\noindent I let you think about a definition that describes the set of
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   125
all strings accepted by a deterministic finite automaton.
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   126
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   127
\begin{figure}[p]
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   128
\small
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   129
\lstinputlisting[numbers=left]{../progs/display/dfa.scala}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   130
\caption{A Scala implementation of DFAs using partial functions.
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   131
  Note some subtleties: \texttt{deltas} implements the delta-hat
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   132
  construction by lifting the (partial) transition  function to lists
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   133
  of characters. Since \texttt{delta} is given as a partial function,
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   134
  it can obviously go ``wrong'' in which case the \texttt{Try} in
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   135
  \texttt{accepts} catches the error and returns \texttt{false}---that
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   136
  means the string is not accepted.  The example \texttt{delta} in
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   137
  Line 28--38 implements the DFA example shown earlier in the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   138
  handout.\label{dfa}}
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   139
\end{figure}
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   140
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   141
My take on an implementation of DFAs in Scala is given in
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   142
Figure~\ref{dfa}. As you can see, there are many features of the
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   143
mathematical definition that are quite closely reflected in the
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   144
code. In the DFA-class, there is a starting state, called
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   145
\texttt{start}, with the polymorphic type \texttt{A}.  There is a
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   146
partial function \texttt{delta} for specifying the transitions---these
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   147
partial functions take a state (of polymorphic type \texttt{A}) and an
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   148
input (of polymorphic type \texttt{C}) and produce a new state (of
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   149
type \texttt{A}). For the moment it is OK to assume that \texttt{A} is
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   150
some arbitrary type for states and the input is just characters.  (The
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   151
reason for not having concrete types, but polymorphic types for the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   152
states and the input of DFAs will become clearer later on.)
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   153
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   154
The DFA-class has also an argument for specifying final states. In the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   155
implementation it is not a set of states, as in the mathematical
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   156
definition, but a function from states to booleans (this function is
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   157
supposed to return true whenever a state is final; false
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   158
otherwise). While this boolean function is different from the sets of
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   159
states, Scala allows to use sets for such functions (see Line 40 where
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   160
the DFA is initialised). Again it will become clear later on why I use
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   161
functions for final states, rather than sets.
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   162
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   163
The most important point in the implementation is that I use Scala's
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   164
partial functions for representing the transitions; alternatives would
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   165
have been \texttt{Maps} or even \texttt{Lists}. One of the main
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   166
advantages of using partial functions is that transitions can be quite
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   167
nicely defined by a series of \texttt{case} statements (see Lines 28
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   168
-- 38 for an example). If you need to represent an automaton with a
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   169
sink state (catch-all-state), you can use Scala's pattern matching and
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   170
write something like
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   171
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   172
{\small\begin{lstlisting}[language=Scala]
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   173
abstract class State
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   174
...
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   175
case object Sink extends State
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   176
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   177
val delta : (State, Char) :=> State = 
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   178
  { case (S0, 'a') => S1
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   179
    case (S1, 'a') => S2
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   180
    case _ => Sink
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   181
  }
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   182
\end{lstlisting}}  
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   183
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   184
\noindent I let you think what the corresponding DFA looks like in the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   185
graph notation.
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   186
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   187
Finally, I let you ponder whether this is a good implementation of
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   188
DFAs or not. In doing so I hope you notice that the $\varSigma$ and
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   189
$Qs$ components (the alphabet and the set of finite states,
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   190
respectively) are missing from the class definition. This means that
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   191
the implementation allows you to do some fishy things you are not
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   192
meant to do with DFAs. Which fishy things could that be?
480
9e42ccbbd1e6 updated
Christian Urban <urbanc@in.tum.de>
parents: 471
diff changeset
   193
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   194
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   195
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   196
\subsection*{Non-Deterministic Finite Automata}
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   197
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   198
Remember we want to find out what the relation is between regular
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   199
expressions and automata. To do this with DFAs is a bit unwieldy.
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   200
While with DFAs it is always clear that given a state and a character
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   201
what the next state is (potentially none), it will be convenient to
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   202
relax this restriction. That means we allow states to have several
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   203
potential successor states. We even allow more than one starting
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   204
state. The resulting construction is called a \emph{Non-Deterministic
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   205
  Finite Automaton} (NFA) given also as a five-tuple ${\cal
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   206
  A}(\varSigma, Qs, Q_{0s}, F, \rho)$ where
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   207
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   208
\begin{itemize}
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   209
\item $\varSigma$ is an alphabet,  
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   210
\item $Qs$ is a finite set of states
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   211
\item $Q_{0s}$ is a set of start states ($Q_{0s} \subseteq Qs$)
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   212
\item $F$ are some accepting states with $F \subseteq Qs$, and
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   213
\item $\rho$ is a transition relation.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   214
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   215
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   216
\noindent
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   217
A typical example of a NFA is
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   218
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   219
% A NFA for (ab* + b)*a
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   220
\begin{center}
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   221
\begin{tikzpicture}[>=stealth',very thick, auto,
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   222
    every state/.style={minimum size=0pt,inner sep=3pt,
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   223
      draw=blue!50,very thick,fill=blue!20},scale=2]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   224
\node[state,initial]  (Q_0)  {$Q_0$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   225
\node[state] (Q_1) [right=of Q_0] {$Q_1$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   226
\node[state, accepting] (Q_2) [right=of Q_1] {$Q_2$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   227
\path[->] (Q_0) edge [loop above] node  {$b$} ();
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   228
\path[<-] (Q_0) edge node [below]  {$b$} (Q_1);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   229
\path[->] (Q_0) edge [bend left] node [above]  {$a$} (Q_1);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   230
\path[->] (Q_0) edge [bend right] node [below]  {$a$} (Q_2);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   231
\path[->] (Q_1) edge [loop above] node  {$a,b$} ();
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   232
\path[->] (Q_1) edge node  [above] {$a$} (Q_2);
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   233
\end{tikzpicture}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   234
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   235
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   236
\noindent
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   237
This NFA happens to have only one starting state, but in general there
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   238
could be more.  Notice that in state $Q_0$ we might go to state $Q_1$
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   239
\emph{or} to state $Q_2$ when receiving an $a$. Similarly in state
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   240
$Q_1$ and receiving an $a$, we can stay in state $Q_1$ \emph{or} go to
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   241
$Q_2$. This kind of choice is not allowed with DFAs. The downside of
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   242
this choice in NFAs is that when it comes to deciding whether a string is
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   243
accepted by a NFA we potentially have to explore all possibilities. I
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   244
let you think which strings the above NFA accepts.
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   245
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   246
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   247
There are a number of additional points you should note about
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   248
NFAs. Every DFA is a NFA, but not vice versa. The $\rho$ in NFAs is a
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   249
transition \emph{relation} (DFAs have a transition function). The
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   250
difference between a function and a relation is that a function has
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   251
always a single output, while a relation gives, roughly speaking,
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   252
several outputs. Look again at the NFA above: if you are currently in
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   253
the state $Q_1$ and you read a character $b$, then you can transition
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   254
to either $Q_0$ \emph{or} $Q_2$. Which route, or output, you take is
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   255
not determined.  This non-determinism can be represented by a
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   256
relation.
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   257
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   258
My implementation of NFAs in Scala is shown in Figure~\ref{nfa}.
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   259
Perhaps interestingly, I do not actually use relations for my NFAs,
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   260
but use transition functions that return sets of states.  DFAs have
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   261
partial transition functions that return a single state; my NFAs
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   262
return a set of states. I let you think about this representation for
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   263
NFA-transitions and how it corresponds to the relations used in the
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   264
mathematical definition of NFAs. An example of a transition function
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   265
in Scala for the NFA shown above is
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   266
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   267
{\small\begin{lstlisting}[language=Scala]
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   268
val nfa_delta : (State, Char) :=> Set[State] = 
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   269
  { case (Q0, 'a') => Set(Q1, Q2)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   270
    case (Q0, 'b') => Set(Q0)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   271
    case (Q1, 'a') => Set(Q1, Q2)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   272
    case (Q1, 'b') => Set(Q0, Q1) }
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   273
\end{lstlisting}}  
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   274
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   275
Like in the mathematical definition, \texttt{starts} is in
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   276
NFAs a set of states; \texttt{fins} is again a function from states to
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   277
booleans. The \texttt{next} function calculates the set of next states
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   278
reachable from a single state \texttt{q} by a character~\texttt{c}. In
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   279
case there is no such state---the partial transition function is
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   280
undefined---the empty set is returned (see function
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   281
\texttt{applyOrElse} in Lines 9 and 10). The function \texttt{nexts}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   282
just lifts this function to sets of states.
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   283
 
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   284
\begin{figure}[p]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   285
\small
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   286
\lstinputlisting[numbers=left]{../progs/display/nfa.scala}
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   287
\caption{A Scala implementation of NFAs using partial functions.
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   288
  Notice that the function \texttt{accepts} implements the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   289
  acceptance of a string in a breath-first search fashion. This can be a costly
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   290
  way of deciding whether a string is accepted or not in applications that need to handle
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   291
  large NFAs and large inputs.\label{nfa}}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   292
\end{figure}
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   293
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   294
Look very careful at the \texttt{accepts} and \texttt{deltas}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   295
functions in NFAs and remember that when accepting a string by a NFA
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   296
we might have to explore all possible transitions (recall which state
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   297
to go to is not unique anymore with NFAs\ldots{}we need to explore
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   298
potentially all next states). The implementation achieves this
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   299
exploration through a \emph{breadth-first search}. This is fine for
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   300
small NFAs, but can lead to real memory problems when the NFAs are
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   301
bigger and larger strings need to be processed. As result, some
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   302
regular expression matching engines resort to a \emph{depth-first
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   303
  search} with \emph{backtracking} in unsuccessful cases. In our
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   304
implementation we can implement a depth-first version of
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   305
\texttt{accepts} using Scala's \texttt{exists}-function as follows:
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   306
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   307
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   308
{\small\begin{lstlisting}[language=Scala]
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   309
def search(q: A, s: List[C]) : Boolean = s match {
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   310
  case Nil => fins(q)
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   311
  case c::cs => next(q, c).exists(search(_, cs)) 
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   312
}
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   313
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   314
def accepts2(s: List[C]) : Boolean = 
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   315
  starts.exists(search(_, s))
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   316
\end{lstlisting}}
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   317
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
   318
\noindent
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   319
This depth-first way of exploration seems to work quite efficiently in
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   320
many examples and is much less of a strain on memory. The problem is
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   321
that the backtracking can get ``catastrophic'' in some
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   322
examples---remember the catastrophic backtracking from earlier
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   323
lectures. This depth-first search with backtracking is the reason for
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   324
the abysmal performance of some regular expression matchings in Java,
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   325
Ruby and Python. I like to show you this in the next two sections.
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   326
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   327
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   328
\subsection*{Epsilon NFAs}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   329
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   330
In order to get an idea what calculations are performed by Java \&
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   331
friends, we need a method for transforming a regular expression into
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   332
an automaton. This automaton should accept exactly those strings that
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   333
are accepted by the regular expression.  The simplest and most
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   334
well-known method for this is called \emph{Thompson Construction},
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   335
after the Turing Award winner Ken Thompson. This method is by
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   336
recursion over regular expressions and depends on the non-determinism
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   337
in NFAs described in the previous section. You will see shortly why
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   338
this construction works well with NFAs, but is not so straightforward
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   339
with DFAs.
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   340
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   341
Unfortunately we are still one step away from our intended target
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   342
though---because this construction uses a version of NFAs that allows
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   343
``silent transitions''. The idea behind silent transitions is that
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   344
they allow us to go from one state to the next without having to
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   345
consume a character. We label such silent transition with the letter
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   346
$\epsilon$ and call the automata $\epsilon$NFAs. Two typical examples
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   347
of $\epsilon$NFAs are:
484
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   348
e61ffb28994d updated
Christian Urban <urbanc@in.tum.de>
parents: 483
diff changeset
   349
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   350
\begin{center}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   351
\begin{tabular}[t]{c@{\hspace{9mm}}c}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   352
\begin{tikzpicture}[>=stealth',very thick,
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   353
    every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   354
\node[state,initial]  (Q_0)  {$Q_0$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   355
\node[state] (Q_1) [above=of Q_0] {$Q_1$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   356
\node[state, accepting] (Q_2) [below=of Q_0] {$Q_2$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   357
\path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_1);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   358
\path[->] (Q_0) edge node [left]  {$\epsilon$} (Q_2);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   359
\path[->] (Q_0) edge [loop right] node  {$a$} ();
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   360
\path[->] (Q_1) edge [loop right] node  {$a$} ();
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   361
\path[->] (Q_2) edge [loop right] node  {$b$} ();
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   362
\end{tikzpicture} &
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   363
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   364
\raisebox{20mm}{
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   365
\begin{tikzpicture}[>=stealth',very thick,
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   366
    every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   367
\node[state,initial]  (r_1)  {$R_1$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   368
\node[state] (r_2) [above=of r_1] {$R_2$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   369
\node[state, accepting] (r_3) [right=of r_1] {$R_3$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   370
\path[->] (r_1) edge node [below]  {$b$} (r_3);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   371
\path[->] (r_2) edge [bend left] node [above]  {$a$} (r_3);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   372
\path[->] (r_1) edge [bend left] node  [left] {$\epsilon$} (r_2);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   373
\path[->] (r_2) edge [bend left] node  [right] {$a$} (r_1);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   374
\end{tikzpicture}}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   375
\end{tabular}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   376
\end{center}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   377
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   378
\noindent
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   379
Consider the $\epsilon$NFA on the left-hand side: the
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   380
$\epsilon$-transitions mean you do not have to ``consume'' any part of
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   381
the input string, but ``silently'' change to a different state. In
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   382
this example, if you are in the starting state $Q_0$, you can silently
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   383
move either to $Q_1$ or $Q_2$. You can see that once you are in $Q_1$,
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   384
respectively $Q_2$, you cannot ``go back'' to the other states. So it
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   385
seems allowing $\epsilon$-transitions is a rather substantial
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   386
extension to NFAs. On first appearances, $\epsilon$-transitions might
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   387
even look rather strange, or even silly. To start with, silent
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   388
transitions make the decision whether a string is accepted by an
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   389
automaton even harder: with $\epsilon$NFAs we have to look whether we
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   390
can do first some $\epsilon$-transitions and then do a
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   391
``proper''-transition; and after any ``proper''-transition we again
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   392
have to check whether we can do again some silent transitions. Even
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   393
worse, if there is a silent transition pointing back to the same
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   394
state, then we have to be careful our decision procedure for strings
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   395
does not loop (remember the depth-first search for exploring all
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   396
states).
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   397
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   398
The obvious question is: Do we get anything in return for this hassle
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   399
with silent transitions?  Well, we still have to work for it\ldots
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   400
unfortunately.  If we were to follow the many textbooks on the
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   401
subject, we would now start with defining what $\epsilon$NFAs
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   402
are---that would require extending the transition relation of
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   403
NFAs. Next, we would show that the $\epsilon$NFAs are equivalent to
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   404
NFAs and so on. Once we have done all this on paper, we would need to
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   405
implement $\epsilon$NFAs. Lets try to take a shortcut instead. We are
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   406
not really interested in $\epsilon$NFAs; they are only a convenient
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   407
tool for translating regular expressions into automata. So we are not
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   408
going to implementing them explicitly, but translate them immediately
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   409
into NFAs (in a sense $\epsilon$NFAs are just a convenient API for
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   410
lazy people ;o).  How does the translation work? Well we have to find
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   411
all transitions of the form
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   412
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   413
\[
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   414
q\stackrel{\epsilon}{\longrightarrow}\ldots\stackrel{\epsilon}{\longrightarrow}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   415
\;\stackrel{a}{\longrightarrow}\;
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   416
\stackrel{\epsilon}{\longrightarrow}\ldots\stackrel{\epsilon}{\longrightarrow} q'
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   417
\]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   418
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   419
\noindent and replace them with $q \stackrel{a}{\longrightarrow}
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   420
q'$. Doing this to the $\epsilon$NFA on the right-hand side above gives
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   421
the NFA
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   422
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   423
\begin{center}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   424
\begin{tikzpicture}[>=stealth',very thick,
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   425
    every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   426
\node[state,initial]  (r_1)  {$R_1$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   427
\node[state] (r_2) [above=of r_1] {$R_2$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   428
\node[state, accepting] (r_3) [right=of r_1] {$R_3$};
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   429
\path[->] (r_1) edge node [above]  {$b$} (r_3);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   430
\path[->] (r_2) edge [bend left] node [above]  {$a$} (r_3);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   431
\path[->] (r_1) edge [bend left] node  [left] {$a$} (r_2);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   432
\path[->] (r_2) edge [bend left] node  [right] {$a$} (r_1);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   433
\path[->] (r_1) edge [loop below] node  {$a$} ();
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   434
\path[->] (r_1) edge [bend right] node [below]  {$a$} (r_3);
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   435
\end{tikzpicture}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   436
\end{center}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   437
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   438
\noindent where the single $\epsilon$-transition is replaced by
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   439
three additional $a$-transitions. Please do the calculations yourself
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   440
and verify that I did not forget any transition.
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   441
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   442
So in what follows, whenever we are given an $\epsilon$NFA we will
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   443
replace it by an equivalent NFA. The Scala code for this translation
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   444
is given in Figure~\ref{enfa}. The main workhorse in this code is a
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   445
function that calculates a fixpoint of function (Lines 5--10). This
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   446
function is used for ``discovering'' which states are reachable by
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   447
$\epsilon$-transitions. Once no new state is discovered, a fixpoint is
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   448
reached. This is used for example when calculating the starting states
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   449
of an equivalent NFA (see Line 36): we start with all starting states
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   450
of the $\epsilon$NFA and then look for all additional states that can
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   451
be reached by $\epsilon$-transitions. We keep on doing this until no
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   452
new state can be reached. This is what the $\epsilon$-closure, named
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   453
in the code \texttt{ecl}, calculates. Similarly, an accepting state of
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   454
the NFA is when we can reach an accepting state of the $\epsilon$NFA
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   455
by $\epsilon$-transitions.
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   456
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   457
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   458
\begin{figure}[p]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   459
\small
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   460
\lstinputlisting[numbers=left]{../progs/display/enfa.scala}
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   461
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   462
\caption{A Scala function that translates $\epsilon$NFA into NFAs. The
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   463
  transition function of $\epsilon$NFA takes as input an \texttt{Option[C]}.
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   464
  \texttt{None} stands for an $\epsilon$-transition; \texttt{Some(c)}
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   465
  for a ``proper'' transition consuming a character. The functions in
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   466
  Lines 18--26 calculate
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   467
  all states reachable by one or more $\epsilon$-transition for a given
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   468
  set of states. The NFA is constructed in Lines 36--38.\label{enfa}}
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   469
\end{figure}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   470
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   471
Also look carefully how the transitions of $\epsilon$NFAs are
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   472
implemented. The additional possibility of performing silent
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   473
transitions is encoded by using \texttt{Option[C]} as the type for the
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   474
``input''. The \texttt{Some}s stand for ``proper'' transitions where
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   475
a character is consumed; \texttt{None} stands for
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   476
$\epsilon$-transitions. The transition functions for the two
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   477
$\epsilon$NFAs from the beginning of this section can be defined as
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   478
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   479
{\small\begin{lstlisting}[language=Scala]
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   480
val enfa_trans1 : (State, Option[Char]) :=> Set[State] = 
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   481
  { case (Q0, Some('a')) => Set(Q0)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   482
    case (Q0, None) => Set(Q1, Q2)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   483
    case (Q1, Some('a')) => Set(Q1)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   484
    case (Q2, Some('b')) => Set(Q2) }
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   485
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   486
val enfa_trans2 : (State, Option[Char]) :=> Set[State] = 
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   487
  { case (R1, Some('b')) => Set(R3)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   488
    case (R1, None) => Set(R2)
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   489
    case (R2, Some('a')) => Set(R1, R3) }
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   490
\end{lstlisting}}
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   491
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   492
\noindent
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   493
I hope you agree now with my earlier statement that the $\epsilon$NFAs
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   494
are just an API for NFAs.
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   495
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   496
\subsection*{Thompson Construction}
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   497
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   498
Having the translation of $\epsilon$NFAs to NFAs in place, we can
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   499
finally return to the problem of translating regular expressions into
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   500
equivalent NFAs. Recall that by equivalent we mean that the NFAs
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   501
recognise the same language. Consider the simple regular expressions
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   502
$\ZERO$, $\ONE$ and $c$. They can be translated into equivalent NFAs
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   503
as follows:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   504
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   505
\begin{equation}\mbox{
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   506
\begin{tabular}[t]{l@{\hspace{10mm}}l}
444
3056a4c071b0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 349
diff changeset
   507
\raisebox{1mm}{$\ZERO$} & 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   508
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   509
\node[state, initial]  (Q_0)  {$\mbox{}$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   510
\end{tikzpicture}\\\\
444
3056a4c071b0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 349
diff changeset
   511
\raisebox{1mm}{$\ONE$} & 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   512
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   513
\node[state, initial, accepting]  (Q_0)  {$\mbox{}$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   514
\end{tikzpicture}\\\\
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   515
\raisebox{3mm}{$c$} & 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   516
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   517
\node[state, initial]  (Q_0)  {$\mbox{}$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   518
\node[state, accepting]  (Q_1)  [right=of Q_0] {$\mbox{}$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   519
\path[->] (Q_0) edge node [below]  {$c$} (Q_1);
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   520
\end{tikzpicture}\\
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   521
\end{tabular}}\label{simplecases}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   522
\end{equation}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   523
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   524
\noindent
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   525
I let you think whether the NFAs can match exactly those strings the
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   526
regular expressions can match. To do this translation in code we need
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   527
a way to construct states programatically...and as an additional
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   528
constrain Scala needs to recognise that these states are being distinct.
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   529
For this I implemented in Figure~\ref{thompson1} a class
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   530
\texttt{TState} that includes a counter and a companion object that
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   531
increases this counter whenever a new state is created.\footnote{You might
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   532
  have to read up what \emph{companion objects} do in Scala.}
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   533
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   534
\begin{figure}[p]
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   535
\small
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   536
\lstinputlisting[numbers=left]{../progs/display/thompson1.scala}
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   537
\caption{The first part of the Thompson Construction. Lines 7--16
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   538
  implement a way of how to create new states that are all
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   539
  distinct by virtue of a counter. This counter is
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   540
  increased in the companion object of \texttt{TState}
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   541
  whenever a new state is created. The code in Lines 24--40
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   542
  constructs NFAs for the simple regular expressions $\ZERO$, $\ONE$ and $c$.
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   543
  Compare the pictures given in \eqref{simplecases}.
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   544
  \label{thompson1}}
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   545
\end{figure}
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   546
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   547
\begin{figure}[p]
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   548
\small
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   549
\lstinputlisting[numbers=left]{../progs/display/thompson2.scala}
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   550
\caption{The second part of the Thompson Construction implementing
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   551
  the composition of NFAs according to $\cdot$, $+$ and ${}^*$.
487
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   552
  The implicit class about rich partial functions
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   553
  implements the infix operation \texttt{+++} which
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   554
  combines an $\epsilon$NFA transition with a NFA transition
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   555
  (both given as partial functions).\label{thompson2}}
a697421eaa04 updated
Christian Urban <urbanc@in.tum.de>
parents: 485
diff changeset
   556
\end{figure}
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
   557
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   558
The case for the sequence regular expression $r_1 \cdot r_2$ is a bit more
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   559
complicated: Say, we are given by recursion two NFAs representing the regular
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   560
expressions $r_1$ and $r_2$ respectively.
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   561
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   562
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   563
\begin{tikzpicture}[node distance=3mm,
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   564
    >=stealth',very thick,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   565
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   566
\node[state, initial]  (Q_0)  {$\mbox{}$};
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   567
\node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   568
\node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   569
\node (R_1)  [right=of Q_0] {$\ldots$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   570
\node[state, accepting]  (T_1)  [right=of R_1] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   571
\node[state, accepting]  (T_2)  [above=of T_1] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   572
\node[state, accepting]  (T_3)  [below=of T_1] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   573
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   574
\node (A_0)  [right=2.5cm of T_1] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   575
\node[state, initial]  (A_01)  [above=1mm of A_0] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   576
\node[state, initial]  (A_02)  [below=1mm of A_0] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   577
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   578
\node (b_1)  [right=of A_0] {$\ldots$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   579
\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
   580
\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
   581
\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
   582
\begin{pgfonlayer}{background}
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   583
  \node (1) [rounded corners, inner sep=1mm, thick,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   584
    draw=black!60, fill=black!20, fit= (Q_0) (R_1) (T_1) (T_2) (T_3)] {};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   585
  \node (2) [rounded corners, inner sep=1mm, thick,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   586
    draw=black!60, fill=black!20, fit= (A_0) (b_1) (c_1) (c_2) (c_3)] {};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   587
\node [yshift=2mm] at (1.north) {$r_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   588
\node [yshift=2mm] at (2.north) {$r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   589
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   590
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   591
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   592
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   593
\noindent The first NFA has some accepting states and the second some
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   594
starting states. We obtain an $\epsilon$NFA for $r_1\cdot r_2$ by
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   595
connecting the accepting states of the first NFA with
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   596
$\epsilon$-transitions to the starting states of the second
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   597
automaton. By doing so we make the accepting states of the first NFA
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   598
to be non-accepting like so:
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   599
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   600
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   601
\begin{tikzpicture}[node distance=3mm,
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   602
    >=stealth',very thick,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   603
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   604
\node[state, initial]  (Q_0)  {$\mbox{}$};
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   605
\node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   606
\node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};  
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   607
\node (r_1)  [right=of Q_0] {$\ldots$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   608
\node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   609
\node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   610
\node[state]  (t_3)  [below=of t_1] {$\mbox{}$};
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   611
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   612
\node  (A_0)  [right=2.5cm of t_1] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   613
\node[state]  (A_01)  [above=1mm of A_0] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   614
\node[state]  (A_02)  [below=1mm of A_0] {$\mbox{}$};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   615
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   616
\node (b_1)  [right=of A_0] {$\ldots$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   617
\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
   618
\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
   619
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   620
\path[->] (t_1) edge (A_01);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   621
\path[->] (t_2) edge node [above]  {$\epsilon$} (A_01);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   622
\path[->] (t_3) edge (A_01);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   623
\path[->] (t_1) edge (A_02);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   624
\path[->] (t_2) edge (A_02);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   625
\path[->] (t_3) edge node [below]  {$\epsilon$} (A_02);
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   626
 
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   627
\begin{pgfonlayer}{background}
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   628
  \node (3) [rounded corners, inner sep=1mm, thick,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   629
    draw=black!60, fill=black!20, fit= (Q_0) (c_1) (c_2) (c_3)] {};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   630
\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
   631
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   632
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   633
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   634
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   635
\noindent The idea behind this construction is that the start of any
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   636
string is first recognised by the first NFA, then we silently change
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   637
to the second NFA; the ending of the string is recognised by the
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   638
second NFA...just like matching of a string by the regular expression
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   639
$r_1\cdot r_2$. The Scala code for this construction is given in
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   640
Figure~\ref{thompson2} in Lines 16--23. The starting states of the
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   641
$\epsilon$NFA are the starting states of the first NFA (corresponding
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   642
to $r_1$); the accepting function is the accepting function of the
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   643
second NFA (corresponding to $r_2$). The new transition function is
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   644
all the ``old'' transitions plus the $\epsilon$-transitions connecting
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   645
the accepting states of the first NFA to the starting states of the
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   646
first NFA (Lines 18 and 19). The $\epsilon$NFA is then immediately
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   647
translated in a NFA.
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   648
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   649
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   650
The case for the alternative regular expression $r_1 + r_2$ is
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   651
slightly different: We are given by recursion two NFAs representing
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   652
$r_1$ and $r_2$ respectively. Each NFA has some starting states and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   653
some accepting states. We obtain a NFA for the regular expression $r_1
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   654
+ r_2$ by composing the transition functions (this crucially depends
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   655
on knowing that the states of each component NFA are distinct); and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   656
also combine the starting states and accepting functions.
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   657
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   658
\begin{center}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   659
\begin{tabular}[t]{ccc}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   660
\begin{tikzpicture}[node distance=3mm,
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   661
    >=stealth',very thick,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   662
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   663
    baseline=(current bounding box.center)]
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   664
\node at (0,0)  (1)  {$\mbox{}$};
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   665
\node  (2)  [above=10mm of 1] {};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   666
\node[state, initial]  (4)  [above=1mm of 2] {$\mbox{}$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   667
\node[state, initial]  (5)  [below=1mm of 2] {$\mbox{}$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   668
\node[state, initial]  (3)  [below=10mm of 1] {$\mbox{}$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   669
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   670
\node (a)  [right=of 2] {$\ldots\,$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   671
\node  (a1)  [right=of a] {$$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   672
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   673
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   674
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   675
\node (b)  [right=of 3] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   676
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   677
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   678
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   679
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   680
\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
   681
\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
   682
\node [yshift=3mm] at (1.north) {$r_1$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   683
\node [yshift=3mm] at (2.north) {$r_2$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   684
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   685
\end{tikzpicture}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   686
&
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   687
\mbox{}\qquad\tikz{\draw[>=stealth,line width=2mm,->] (0,0) -- (1, 0)}\quad\mbox{}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   688
&
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   689
\begin{tikzpicture}[node distance=3mm,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   690
    >=stealth',very thick,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   691
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   692
    baseline=(current bounding box.center)]
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   693
\node at (0,0) (1)  {$\mbox{}$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   694
\node (2)  [above=10mm of 1] {$$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   695
\node[state, initial]  (4)  [above=1mm of 2] {$\mbox{}$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   696
\node[state, initial]  (5)  [below=1mm of 2] {$\mbox{}$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   697
\node[state, initial]  (3)  [below=10mm of 1] {$\mbox{}$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   698
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   699
\node (a)  [right=of 2] {$\ldots\,$};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   700
\node (a1)  [right=of a] {$$};
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   701
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   702
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   703
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   704
\node (b)  [right=of 3] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   705
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   706
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   707
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   708
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   709
%\path[->] (1) edge node [above]  {$\epsilon$} (2);
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   710
%\path[->] (1) edge node [below]  {$\epsilon$} (3);
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   711
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   712
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   713
\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
   714
\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
   715
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   716
\end{tikzpicture}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   717
\end{tabular}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   718
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   719
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   720
\noindent The code for this construction is in Figure~\ref{thompson2}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   721
in Lines 25--33.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   722
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   723
Finally for the $*$-case we have a NFA for $r$ and connect its
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   724
accepting states to a new starting state via
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   725
$\epsilon$-transitions. This new starting state is also an accepting
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   726
state, because $r^*$ can recognise the empty string.
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   727
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   728
\begin{center}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   729
\begin{tabular}[b]{@{\hspace{-4mm}}ccc@{}}  
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   730
\begin{tikzpicture}[node distance=3mm,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   731
    >=stealth',very thick,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   732
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   733
    baseline=(current bounding box.north)]
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   734
\node at (0,0)  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   735
\node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   736
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   737
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   738
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   739
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   740
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   741
\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
   742
\node [yshift=3mm] at (1.north) {$r$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   743
\end{pgfonlayer}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   744
\end{tikzpicture}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   745
&
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   746
\raisebox{-16mm}{\;\tikz{\draw[>=stealth,line width=2mm,->] (0,0) -- (1, 0)}}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   747
&
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   748
\begin{tikzpicture}[node distance=3mm,
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   749
    >=stealth',very thick,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   750
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   751
    baseline=(current bounding box.north)]
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   752
\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   753
\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   754
\node (a)  [right=of 2] {$\ldots$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   755
\node[state]  (a1)  [right=of a] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   756
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   757
\node[state]  (a3)  [below=of a1] {$\mbox{}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   758
\path[->] (1) edge node [above]  {$\epsilon$} (2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   759
\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
   760
\path[->] (a2) edge [bend right] node [below]  {$\epsilon$} (1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   761
\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
   762
\begin{pgfonlayer}{background}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   763
\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
   764
\node [yshift=3mm] at (2.north) {$r^*$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   765
\end{pgfonlayer}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   766
\end{tikzpicture}    
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   767
\end{tabular}
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   768
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 142
diff changeset
   769
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   770
\noindent 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   771
The corresponding code is in Figure~\ref{thompson2} in Lines 35--43)
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   772
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   773
To sum up, you can see in the sequence and star cases the need of
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   774
having silent $\epsilon$-transitions. Similarly the alternative case
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   775
shows the need of the NFA-nondeterminism. It seems awkward to form the
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   776
`alternative' composition of two DFAs, because DFA do not allow
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   777
several starting and successor states. All these constructions can now
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   778
be put together in the following recursive function:
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   779
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   780
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   781
{\small\begin{lstlisting}[language=Scala]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   782
def thompson(r: Rexp) : NFAt = r match {
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   783
  case ZERO => NFA_ZERO()
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   784
  case ONE => NFA_ONE()
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   785
  case CHAR(c) => NFA_CHAR(c)  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   786
  case ALT(r1, r2) => NFA_ALT(thompson(r1), thompson(r2))
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   787
  case SEQ(r1, r2) => NFA_SEQ(thompson(r1), thompson(r2))
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   788
  case STAR(r1) => NFA_STAR(thompson(r1))
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   789
}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   790
\end{lstlisting}}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   791
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   792
\noindent
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   793
It calculates a NFA from a regular expressions. At last we can run
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   794
NFAs for the our evil regular expression examples.  The graph on the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   795
left shows that when translating a regular expression such as
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   796
$a^{\{n\}}$ into a NFA, the size can blow up and then even the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   797
relative fast (on small examples) breadth-first search can be
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   798
slow. The graph on the right shows that with `evil' regular
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   799
expressions the depth-first search can be abysmally slow. Even if the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   800
graphs not completely overlap with the curves of Python, Ruby and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   801
Java, they are similar enough. OK\ldots now you know why regular
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   802
expression matchers in those languages are so slow. 
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   803
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   804
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   805
\begin{center}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   806
\begin{tabular}{@{\hspace{-1mm}}c@{\hspace{1mm}}c@{}}  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   807
\begin{tikzpicture}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   808
\begin{axis}[
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   809
    title={Graph: $a^{?\{n\}} \cdot a^{\{n\}}$ and strings 
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   810
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   811
    title style={yshift=-2ex},
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   812
    xlabel={$n$},
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   813
    x label style={at={(1.05,0.0)}},
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   814
    ylabel={time in secs},
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   815
    enlargelimits=false,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   816
    xtick={0,5,...,30},
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   817
    xmax=33,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   818
    ymax=35,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   819
    ytick={0,5,...,30},
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   820
    scaled ticks=false,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   821
    axis lines=left,
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   822
    width=5.5cm,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   823
    height=4cm, 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   824
    legend entries={Python,Ruby, breadth-first NFA},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   825
    legend style={at={(0.5,-0.25)},anchor=north,font=\small},
489
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   826
    legend cell align=left]
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   827
  \addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   828
  \addplot[brown,mark=triangle*, mark options={fill=white}] table {re-ruby.data};
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   829
  % breath-first search in NFAs
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   830
  \addplot[red,mark=*, mark options={fill=white}] table {
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   831
    1 0.00586
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   832
    2 0.01209
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   833
    3 0.03076
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   834
    4 0.08269
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   835
    5 0.12881
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   836
    6 0.25146
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   837
    7 0.51377
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   838
    8 0.89079
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   839
    9 1.62802
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   840
    10 3.05326
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   841
    11 5.92437
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   842
    12 11.67863
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   843
    13 24.00568
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   844
  };
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   845
\end{axis}
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   846
\end{tikzpicture}
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   847
&
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   848
\begin{tikzpicture}
e28d7a327870 updated
Christian Urban <urbanc@in.tum.de>
parents: 488
diff changeset
   849
\begin{axis}[
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   850
    title={Graph: $(a^*)^* \cdot b$ and strings 
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   851
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   852
    title style={yshift=-2ex},
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   853
    xlabel={$n$},
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   854
    x label style={at={(1.05,0.0)}},
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   855
    ylabel={time in secs},
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   856
    enlargelimits=false,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   857
    xtick={0,5,...,30},
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   858
    xmax=33,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   859
    ymax=35,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   860
    ytick={0,5,...,30},
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   861
    scaled ticks=false,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   862
    axis lines=left,
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   863
    width=5.5cm,
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   864
    height=4cm, 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   865
    legend entries={Python, Java, depth-first NFA},
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   866
    legend style={at={(0.5,-0.25)},anchor=north,font=\small},
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   867
    legend cell align=left]
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   868
  \addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   869
  \addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};  
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   870
  % depth-first search in NFAs
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   871
  \addplot[red,mark=*, mark options={fill=white}] table {
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   872
    1 0.00605
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   873
    2 0.03086
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   874
    3 0.11994
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   875
    4 0.45389
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   876
    5 2.06192
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   877
    6 8.04894
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   878
    7 32.63549
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   879
  };
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   880
\end{axis}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   881
\end{tikzpicture}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   882
\end{tabular}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   883
\end{center}
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   884
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   885
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   886
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   887
\subsection*{Subset Construction}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   888
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   889
Of course, some developers of regular expression matchers are aware
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   890
of these problems with sluggish NFAs and try to address them. One
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   891
common technique for this I like to show you in this section. It will
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   892
also explain why we insisted on polymorphic types in our DFA code
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   893
(remember I used \texttt{A} and \texttt{C} for the types of states and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   894
the input, see Figure~\ref{dfa} on Page~\pageref{dfa}).\bigskip
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   895
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   896
\noindent
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   897
To start, remember that we did not bother with defining and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   898
implementing $\epsilon$NFA; we immediately translated them into
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   899
equivalent NFAs. Equivalent in the sense of accepting the same
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   900
language (though we only claimed this and did not prove it
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   901
rigorously). Remember also that NFAs have non-deterministic
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   902
transitions defined as a relation or implemented as function returning
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   903
sets of states.  This non-determinism is crucial for the Thompson
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   904
Construction to work (recall the cases for $\cdot$, $+$ and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   905
${}^*$). But this non-determinism makes it harder with NFAs to decide
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   906
when a string is accepted or not; such a decision is rather
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   907
straightforward with DFAs: recall their transition function is a
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   908
\emph{function} that returns a single state. So we do not have to
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   909
search at all.  What is perhaps interesting is the fact that for every
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   910
NFA we can find a DFA that also recognises the same language. This
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   911
might sound a bit paradoxical: NFA $\rightarrow$ decision of
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   912
acceptance hard; DFA $\rightarrow$ decision easy. But this \emph{is}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   913
true\ldots but of course there is always a caveat---nothing is ever
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   914
for free in life.
488
598741d39d21 updated
Christian Urban <urbanc@in.tum.de>
parents: 487
diff changeset
   915
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   916
There are a number of techniques for transforming a NFA into an
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   917
equivalent DFA, but the most famous one is the \emph{subset
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   918
  construction}. Consider the following NFA where the states are
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   919
labelled with, say, $0$, $1$ and $2$.
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   920
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   921
\begin{center}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   922
\begin{tabular}{c@{\hspace{10mm}}c}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   923
\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
   924
                    every state/.style={minimum size=0pt,
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   925
                    draw=blue!50,very thick,fill=blue!20},
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   926
                    baseline=(current bounding box.center)]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
   927
\node[state,initial]  (Q_0)  {$0$};
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   928
\node[state] (Q_1) [below=of Q_0] {$1$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   929
\node[state, accepting] (Q_2) [below=of Q_1] {$2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   930
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   931
\path[->] (Q_0) edge node [right]  {$b$} (Q_1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   932
\path[->] (Q_1) edge node [right]  {$a,b$} (Q_2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   933
\path[->] (Q_0) edge [loop above] node  {$a, b$} ();
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   934
\end{tikzpicture}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   935
&
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   936
\begin{tabular}{r|ll}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   937
states & $a$ & $b$\\
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   938
\hline
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   939
$\{\}\phantom{\star}$ & $\{\}$ & $\{\}$\\
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   940
start: $\{0\}\phantom{\star}$       & $\{0\}$   & $\{0,1\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   941
$\{1\}\phantom{\star}$       & $\{2\}$       & $\{2\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   942
$\{2\}\star$  & $\{\}$ & $\{\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   943
$\{0,1\}\phantom{\star}$     & $\{0,2\}$   & $\{0,1,2\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   944
$\{0,2\}\star$ & $\{0\}$   & $\{0,1\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   945
$\{1,2\}\star$ & $\{2\}$       & $\{2\}$\\
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   946
$\{0,1,2\}\star$ & $\{0,2\}$ & $\{0,1,2\}$\\
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   947
\end{tabular}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   948
\end{tabular}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   949
\end{center}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   950
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   951
\noindent The states of the corresponding DFA are given by generating
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   952
all subsets of the set of states of the NFA (seen in the states column
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   953
in the table on the right). The other columns define the transition
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   954
function for the DFA for input $a$ and $b$. The first row states that
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   955
$\{\}$ is the sink state which has transitions for $a$ and $b$ to
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   956
itself.  The next three lines are calculated as follows:
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   957
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   958
\begin{itemize}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   959
\item Suppose you calculate the entry for the $a$-transition for state
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   960
  $\{0\}$. Look for all states in the NFA that can be reached by such
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   961
  a transition from this state; this is only state $0$; therefore from
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   962
  state $\{0\}$ we can go to state $\{0\}$ via an $a$-transition.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   963
\item Do the same for the $b$-transition; you can reach states $0$ and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   964
  $1$ in the NFA; therefore in the DFA we can go from state $\{0\}$ to
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   965
  state $\{0,1\}$ via an $b$-transition.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   966
\item Continue with the states $\{1\}$ and $\{2\}$.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   967
\item Once you filled in the transitions for `simple' state, you only
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   968
  have to build the union for the compound states $\{0,1\}$, $\{0,2\}$
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   969
  and so on. For example for $\{0,1\}$ you take the union of line
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   970
  $\{0\}$ and line $\{1\}$, which gives $\{0,2\}$ for $a$, and
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   971
  $\{0,1,2\}$ for $b$. And so on.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   972
\item The starting state of the DFA can be calculated from the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   973
  starting states of the NFA, that is in this case $0$. But in general
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   974
  there can be many starting states in the NFA and you would take the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   975
  corresponding subset as \emph{the} starting state of the DFA.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   976
\item The accepting states in the DFA are given by all sets that
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   977
  contain a $2$, which is the only accpting state in this NFA. But
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   978
  again in general if the subset contains an accepting state from the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   979
  NFA, then the corresponding state in the DFA is accepting as well.
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   980
\end{itemize}
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
   981
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   982
\noindent This completes the subset construction. The corresponding
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   983
DFA for the NFA shown above is:
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   984
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   985
\begin{center}
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   986
\begin{tikzpicture}[scale=0.8,>=stealth',very thick,
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   987
                    every state/.style={minimum size=0pt,
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   988
                    draw=blue!50,very thick,fill=blue!20},
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
   989
                    baseline=0mm]
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   990
\node[state,initial]  (q0)  {$0$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   991
\node[state] (q01) [right=of q0] {$0,1$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   992
\node[state,accepting] (q02) [below=of q01] {$0,2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   993
\node[state,accepting] (q012) [right=of q02] {$0,1,2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   994
\node[state] (q1) [below=0.5cm of q0] {$1$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   995
\node[state,accepting] (q2) [below=1cm of q1] {$2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   996
\node[state] (qn) [below left=1cm of q2] {$\{\}$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   997
\node[state,accepting] (q12) [below right=1cm of q2] {$1,2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   998
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
   999
\path[->] (q0) edge node [above] {$b$} (q01);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1000
\path[->] (q01) edge node [above] {$b$} (q012);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1001
\path[->] (q0) edge [loop above] node  {$a$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1002
\path[->] (q012) edge [loop right] node  {$b$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1003
\path[->] (q012) edge node [below] {$a$} (q02);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1004
\path[->] (q02) edge node [below] {$a$} (q0);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1005
\path[->] (q01) edge [bend left] node [left]  {$a$} (q02);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1006
\path[->] (q02) edge [bend left] node [right]  {$b$} (q01);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1007
\path[->] (q1) edge node [left] {$a,b$} (q2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1008
\path[->] (q12) edge node [right] {$a, b$} (q2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1009
\path[->] (q2) edge node [right] {$a, b$} (qn);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1010
\path[->] (qn) edge [loop left] node  {$a,b$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1011
\end{tikzpicture}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1012
\end{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1013
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1014
\noindent
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1015
Please check that this is indeed a DFA. The big question is whether
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1016
this DFA can recognise the same language as the NFA we started with.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1017
I let you ponder about this question.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1018
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1019
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1020
There are also two points to note: One is that very often the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1021
resulting DFA contains a number of ``dead'' states that are never
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1022
reachable from the starting state. This is obvious in this case, where
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1023
state $\{1\}$, $\{2\}$, $\{1,2\}$ and $\{\}$ can never be reached from
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1024
the starting state.  In effect the DFA in this example is not a
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1025
\emph{minimal} DFA (more about this in a minute). Such dead states can
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1026
be safely removed without changing the language that is recognised by
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1027
the DFA. Another point is that in some cases, however, the subset
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1028
construction produces a DFA that does \emph{not} contain any dead
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1029
states\ldots{}and further calculates a minimal DFA. Which in turn
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1030
means that in some cases the number of states can by going from NFAs
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1031
to DFAs exponentially increase, namely by $2^n$ (which is the number
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1032
of subsets you can form for $n$ states).  This blow up the number of
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1033
states in the DFA is again bad news for how quickly you can decide
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1034
whether a string is accepted by a DFA or not. So the caveat with DFAs
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1035
is that they might make the task of finding the next state trival, but
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1036
might require $2^n$ times as many states as a NFA.\bigskip
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1037
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1038
Lastly, can we 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1039
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1040
{\small\begin{lstlisting}[language=Scala]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1041
def subset[A, C](nfa: NFA[A, C]) : DFA[Set[A], C] = {
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1042
  DFA(nfa.starts, 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1043
      { case (qs, c) => nfa.nexts(qs, c) }, 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1044
      _.exists(nfa.fins))
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1045
}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1046
\end{lstlisting}}  
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1047
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1048
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1049
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1050
\subsection*{DFA Minimisation}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1051
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1052
As seen in the subset construction, the translation 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1053
of a NFA to a DFA can result in a rather ``inefficient'' 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1054
DFA. Meaning there are states that are not needed. A
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1055
DFA can be \emph{minimised} by the following algorithm:
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1056
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1057
\begin{enumerate}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1058
\item Take all pairs $(q, p)$ with $q \not= p$
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1059
\item Mark all pairs that accepting and non-accepting states
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1060
\item For all unmarked pairs $(q, p)$ and all characters $c$
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1061
      test whether 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1062
      
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1063
      \begin{center} 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1064
      $(\delta(q, c), \delta(p,c))$ 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1065
      \end{center} 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1066
      
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1067
      are marked. If there is one, then also mark $(q, p)$.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1068
\item Repeat last step until no change.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1069
\item All unmarked pairs can be merged.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1070
\end{enumerate}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1071
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1072
\noindent To illustrate this algorithm, consider the following 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1073
DFA.
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1074
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1075
\begin{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1076
\begin{tikzpicture}[>=stealth',very thick,auto,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1077
                    every state/.style={minimum size=0pt,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1078
                    inner sep=2pt,draw=blue!50,very thick,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1079
                    fill=blue!20}]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1080
\node[state,initial]  (Q_0)  {$Q_0$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1081
\node[state] (Q_1) [right=of Q_0] {$Q_1$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1082
\node[state] (Q_2) [below right=of Q_0] {$Q_2$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1083
\node[state] (Q_3) [right=of Q_2] {$Q_3$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1084
\node[state, accepting] (Q_4) [right=of Q_1] {$Q_4$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1085
\path[->] (Q_0) edge node [above]  {$a$} (Q_1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1086
\path[->] (Q_1) edge node [above]  {$a$} (Q_4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1087
\path[->] (Q_4) edge [loop right] node  {$a, b$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1088
\path[->] (Q_3) edge node [right]  {$a$} (Q_4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1089
\path[->] (Q_2) edge node [above]  {$a$} (Q_3);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1090
\path[->] (Q_1) edge node [right]  {$b$} (Q_2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1091
\path[->] (Q_0) edge node [above]  {$b$} (Q_2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1092
\path[->] (Q_2) edge [loop left] node  {$b$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1093
\path[->] (Q_3) edge [bend left=95, looseness=1.3] node 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1094
  [below]  {$b$} (Q_0);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1095
\end{tikzpicture}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1096
\end{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1097
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1098
\noindent In Step 1 and 2 we consider essentially a triangle
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1099
of the form
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1100
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1101
\begin{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1102
\begin{tikzpicture}[scale=0.6,line width=0.8mm]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1103
\draw (0,0) -- (4,0);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1104
\draw (0,1) -- (4,1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1105
\draw (0,2) -- (3,2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1106
\draw (0,3) -- (2,3);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1107
\draw (0,4) -- (1,4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1108
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1109
\draw (0,0) -- (0, 4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1110
\draw (1,0) -- (1, 4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1111
\draw (2,0) -- (2, 3);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1112
\draw (3,0) -- (3, 2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1113
\draw (4,0) -- (4, 1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1114
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1115
\draw (0.5,-0.5) node {$Q_0$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1116
\draw (1.5,-0.5) node {$Q_1$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1117
\draw (2.5,-0.5) node {$Q_2$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1118
\draw (3.5,-0.5) node {$Q_3$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1119
 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1120
\draw (-0.5, 3.5) node {$Q_1$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1121
\draw (-0.5, 2.5) node {$Q_2$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1122
\draw (-0.5, 1.5) node {$Q_3$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1123
\draw (-0.5, 0.5) node {$Q_4$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1124
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1125
\draw (0.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1126
\draw (1.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1127
\draw (2.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1128
\draw (3.5,0.5) node {\large$\star$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1129
\end{tikzpicture}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1130
\end{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1131
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1132
\noindent where the lower row is filled with stars, because in
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1133
the corresponding pairs there is always one state that is
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1134
accepting ($Q_4$) and a state that is non-accepting (the other
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1135
states).
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1136
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1137
Now in Step 3 we need to fill in more stars according whether 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1138
one of the next-state pairs are marked. We have to do this 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1139
for every unmarked field until there is no change anymore.
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1140
This gives the triangle
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1141
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1142
\begin{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1143
\begin{tikzpicture}[scale=0.6,line width=0.8mm]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1144
\draw (0,0) -- (4,0);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1145
\draw (0,1) -- (4,1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1146
\draw (0,2) -- (3,2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1147
\draw (0,3) -- (2,3);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1148
\draw (0,4) -- (1,4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1149
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1150
\draw (0,0) -- (0, 4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1151
\draw (1,0) -- (1, 4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1152
\draw (2,0) -- (2, 3);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1153
\draw (3,0) -- (3, 2);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1154
\draw (4,0) -- (4, 1);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1155
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1156
\draw (0.5,-0.5) node {$Q_0$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1157
\draw (1.5,-0.5) node {$Q_1$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1158
\draw (2.5,-0.5) node {$Q_2$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1159
\draw (3.5,-0.5) node {$Q_3$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1160
 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1161
\draw (-0.5, 3.5) node {$Q_1$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1162
\draw (-0.5, 2.5) node {$Q_2$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1163
\draw (-0.5, 1.5) node {$Q_3$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1164
\draw (-0.5, 0.5) node {$Q_4$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1165
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1166
\draw (0.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1167
\draw (1.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1168
\draw (2.5,0.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1169
\draw (3.5,0.5) node {\large$\star$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1170
\draw (0.5,1.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1171
\draw (2.5,1.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1172
\draw (0.5,3.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1173
\draw (1.5,2.5) node {\large$\star$}; 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1174
\end{tikzpicture}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1175
\end{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1176
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1177
\noindent which means states $Q_0$ and $Q_2$, as well as $Q_1$
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1178
and $Q_3$ can be merged. This gives the following minimal DFA
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1179
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1180
\begin{center}
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1181
\begin{tikzpicture}[>=stealth',very thick,auto,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1182
                    every state/.style={minimum size=0pt,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1183
                    inner sep=2pt,draw=blue!50,very thick,
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1184
                    fill=blue!20}]
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1185
\node[state,initial]  (Q_02)  {$Q_{0, 2}$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1186
\node[state] (Q_13) [right=of Q_02] {$Q_{1, 3}$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1187
\node[state, accepting] (Q_4) [right=of Q_13] 
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1188
  {$Q_{4\phantom{,0}}$};
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1189
\path[->] (Q_02) edge [bend left] node [above]  {$a$} (Q_13);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1190
\path[->] (Q_13) edge [bend left] node [below]  {$b$} (Q_02);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1191
\path[->] (Q_02) edge [loop below] node  {$b$} ();
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1192
\path[->] (Q_13) edge node [above]  {$a$} (Q_4);
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1193
\path[->] (Q_4) edge [loop above] node  {$a, b$} ();
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1194
\end{tikzpicture}
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1195
\end{center}
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1196
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1197
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1198
\subsection*{Brzozowski's Method}
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1199
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1200
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
  1201
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
  1202
a regular expression using familiar transformations for
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1203
solving equational systems. Consider the DFA:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1204
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1205
\begin{center}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1206
\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
  1207
                    every state/.style={minimum size=0pt,
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1208
                    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
  1209
                    fill=blue!20}]
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1210
  \node[state, initial]        (q0) at ( 0,1) {$Q_0$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1211
  \node[state]                    (q1) at ( 1,1) {$Q_1$};
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1212
  \node[state, accepting] (q2) at ( 2,1) {$Q_2$};
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1213
  \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
  1214
            (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
  1215
            (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
  1216
            (q1) edge node[above] {$a$} (q2)
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1217
            (q2) edge [loop right] node {$a$} ()
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1218
            (q0) edge [loop below] node {$b$} ();
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1219
\end{tikzpicture}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1220
\end{center}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1221
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1222
\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
  1223
system
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1224
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1225
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1226
Q_0 & = & \ONE + Q_0\,b + Q_1\,b +  Q_2\,b\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1227
Q_1 & = & Q_0\,a\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1228
Q_2 & = & Q_1\,a + Q_2\,a
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1229
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1230
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1231
\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
  1232
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
  1233
constructed. First have a look at the second equation: the
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1234
left-hand side is $Q_1$ and the right-hand side $Q_0\,a$. The
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1235
right-hand side is essentially all possible ways how to end up
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1236
in node $Q_1$. There is only one incoming edge from $Q_0$ consuming
322
698ed1c96cd0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
  1237
an $a$.  Therefore the right hand side is this
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1238
state followed by character---in this case $Q_0\,a$. Now lets
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1239
have a look at the third equation: there are two incoming
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1240
edges for $Q_2$. Therefore we have two terms, namely $Q_1\,a$ and
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1241
$Q_2\,a$. These terms are separated by $+$. The first states
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1242
that if in state $Q_1$ consuming an $a$ will bring you to
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
  1243
$Q_2$, and the second that being in $Q_2$ and consuming an $a$
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1244
will make you stay in $Q_2$. The right-hand side of the
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1245
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
  1246
incoming edges, therefore there are three terms. There is
444
3056a4c071b0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 349
diff changeset
  1247
one exception in that we also ``add'' $\ONE$ to the
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1248
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
  1249
in the DFA.
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1250
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1251
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
  1252
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
  1253
solving usual linear equational systems. For example the
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1254
second equation does not contain the variable $Q_1$ on the
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1255
right-hand side of the equation. We can therefore eliminate 
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1256
$Q_1$ from the system by just substituting this equation
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1257
into the other two. This gives
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1258
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1259
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1260
Q_0 & = & \ONE + Q_0\,b + Q_0\,a\,b +  Q_2\,b\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1261
Q_2 & = & Q_0\,a\,a + Q_2\,a
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1262
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1263
485
bd6d999ab7b6 updated
Christian Urban <urbanc@in.tum.de>
parents: 484
diff changeset
  1264
\noindent where in Equation (4) we have two occurrences
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1265
of $Q_0$. Like the laws about $+$ and $\cdot$, we can simplify 
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1266
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
  1267
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1268
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1269
Q_0 & = & \ONE + Q_0\,(b + a\,b) +  Q_2\,b\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1270
Q_2 & = & Q_0\,a\,a + Q_2\,a
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1271
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1272
 
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1273
\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
  1274
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
  1275
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
  1276
Here we need to now use a law that is different from the usual
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1277
laws about linear equations. It is called \emph{Arden's rule}.
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1278
It states that if an equation is of the form $q = q\,r + s$
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1279
then it can be transformed to $q = s\, r^*$. Since we can
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1280
assume $+$ is symmetric, Equation (7) is of that form: $s$ is
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1281
$Q_0\,a\,a$ and $r$ is $a$. That means we can transform
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1282
(7) to obtain the two new equations
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1283
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1284
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1285
Q_0 & = & \ONE + Q_0\,(b + a\,b) +  Q_2\,b\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1286
Q_2 & = & Q_0\,a\,a\,(a^*)
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1287
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1288
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1289
\noindent Now again we can substitute the second equation into
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1290
the first in order to eliminate the variable $Q_2$.
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1291
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1292
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1293
Q_0 & = & \ONE + Q_0\,(b + a\,b) +  Q_0\,a\,a\,(a^*)\,b
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1294
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1295
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1296
\noindent Pulling $Q_0$ out as a single factor gives:
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1297
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1298
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1299
Q_0 & = & \ONE + Q_0\,(b + a\,b + a\,a\,(a^*)\,b)
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1300
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1301
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1302
\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
  1303
apply Arden's rule ($r$ is $b + a\,b + a\,a\,(a^*)\,b$ and $s$
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1304
is $\ONE$). This gives as solution for $Q_0$ the following
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1305
regular expression:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1306
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1307
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1308
Q_0 & = & \ONE\,(b + a\,b + a\,a\,(a^*)\,b)^*
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1309
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1310
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1311
\noindent Since this is a regular expression, we can simplify
444
3056a4c071b0 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 349
diff changeset
  1312
away the $\ONE$ to obtain the slightly simpler regular
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1313
expression
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1314
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1315
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1316
Q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1317
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1318
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1319
\noindent 
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1320
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
  1321
for the other equations. This gives:
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1322
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1323
\begin{eqnarray}
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1324
Q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1325
Q_1 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\\
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1326
Q_2 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a)^*
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1327
\end{eqnarray}
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1328
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1329
\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
  1330
which correspond to a terminal state. In our running example,
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1331
this is just $Q_2$. Consequently, a regular expression
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1332
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
  1333
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1334
\[
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1335
(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
  1336
\]
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1337
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1338
\noindent You can somewhat crosscheck your solution
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1339
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
  1340
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
  1341
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
  1342
string is also matched by the automaton.
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1343
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1344
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
  1345
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
  1346
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
  1347
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1348
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1349
\subsection*{Regular Languages}
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1350
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1351
Given the constructions in the previous sections we obtain 
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1352
the following overall picture:
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1353
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1354
\begin{center}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1355
\begin{tikzpicture}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1356
\node (rexp)  {\bf Regexps};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1357
\node (nfa) [right=of rexp] {\bf NFAs};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1358
\node (dfa) [right=of nfa] {\bf DFAs};
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1359
\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
  1360
\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
  1361
\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
  1362
\path[->,line width=1mm] (dfa) edge node [below=5mm, black] {minimisation} (mdfa);
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1363
\path[->,line width=1mm] (dfa) edge [bend left=45] node [below] {\begin{tabular}{l}Brzozowski's\\ method\end{tabular}} (rexp);
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1364
\end{tikzpicture}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1365
\end{center}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1366
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1367
\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
  1368
we can always ensure that for every regular expression there
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1369
exists a NFA and a DFA that can recognise the same language.
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1370
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
  1371
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
  1372
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
  1373
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
  1374
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1375
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
  1376
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
  1377
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1378
\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
  1379
regular expression that recognises all its strings.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1380
\end{quote}
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1381
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1382
\noindent or equivalently 
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1383
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1384
\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
  1385
automaton that recognises all its strings.
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1386
\end{quote}
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
  1387
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1388
\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
  1389
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
  1390
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
  1391
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
  1392
regular expression into a NFA gives us an automaton that has
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1393
$O(n)$ states---that means the size of the NFA grows linearly
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1394
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
  1395
is that the problem of deciding whether a string is accepted
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1396
or not is computationally not cheap. Remember with NFAs we
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1397
have potentially many next states even for the same input and
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1398
also have the silent $\epsilon$-transitions. If we want to
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
  1399
find a path from the starting state of a NFA to an accepting
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1400
state, we need to consider all possibilities. In Ruby and
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1401
Python this is done by a depth-first search, which in turn
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1402
means that if a ``wrong'' choice is made, the algorithm has to
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1403
backtrack and thus explore all potential candidates. This is
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1404
exactly the reason why Ruby and Python are so slow for evil
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1405
regular expressions. An alternative to the potentially slow
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1406
depth-first search is to explore the search space in a
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1407
breadth-first fashion, but this might incur a big memory
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1408
penalty.  
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
  1409
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1410
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
  1411
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
  1412
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
  1413
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
  1414
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
  1415
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
  1416
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
  1417
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
  1418
resulting DFAs in order to have an acceptable memory 
344
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1419
and runtime behaviour. But remember the subset construction
408fd5994288 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 333
diff changeset
  1420
in the worst case explodes the number of states by $2^n$.
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1421
Effectively also the translation to DFAs can incur a big
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1422
runtime penalty.
269
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1423
83e6cb90216d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
  1424
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
  1425
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
  1426
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
  1427
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
  1428
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
  1429
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
  1430
for this is as follows: take a regular expression, translate
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1431
it into a NFA and then a DFA that both recognise the same
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1432
language. Once you have the DFA it is very easy to construct
483
6f508bcdaa30 updated
Christian Urban <urbanc@in.tum.de>
parents: 482
diff changeset
  1433
the automaton for the language not recognised by a DFA. If
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1434
the DFA is completed (this is important!), then you just need
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1435
to exchange the accepting and non-accepting states. You can
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1436
then translate this DFA back into a regular expression and
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1437
that will be the regular expression that can match all strings
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1438
the original regular expression could \emph{not} match.
268
18bef085a7ca updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 251
diff changeset
  1439
349
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1440
It is also interesting that not all languages are regular. The
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1441
most well-known example of a language that is not regular
434891622131 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 344
diff changeset
  1442
consists of all the strings of the form
292
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1443
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1444
\[a^n\,b^n\]
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1445
7ed2a25dd115 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
  1446
\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
  1447
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
  1448
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
  1449
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
  1450
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
  1451
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
  1452
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1453
%\section*{Further Reading}
270
4dbeaf43031d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
  1454
490
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1455
%Compare what a ``human expert'' would create as an automaton for the
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1456
%regular expression $a\cdot (b + c)^*$ and what the Thomson
4fee50f38305 updated
Christian Urban <urbanc@in.tum.de>
parents: 489
diff changeset
  1457
%algorithm generates.
325
794c599cee53 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 324
diff changeset
  1458
794c599cee53 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 324
diff changeset
  1459
%http://www.inf.ed.ac.uk/teaching/courses/ct/
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1460
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1461
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1462
%%% Local Variables: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1463
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1464
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1465
%%% End: 
482
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1466
0f6e3c5a1751 updated
Christian Urban <urbanc@in.tum.de>
parents: 480
diff changeset
  1467