\documentclass{article}\usepackage{../style}\usepackage{../langs}\usepackage{../graphics}\begin{document}\section*{Handout 3 (Automata)}Every formal language course I know of bombards you first withautomata and then to a much, much smaller extend with regularexpressions. As you can see, this course is turned upsidedown: regular expressions come first. The reason is thatregular expressions are easier to reason about and the notionof derivatives, although already quite old, only became morewidely known rather recently. Still let us in this lecturehave a closer look at automata and their relation to regularexpressions. This will help us with understanding why theregular expression matchers in Python and Ruby are so slowwith certain regular expressions. The central definitionis:\medskip \noindent A \emph{deterministic finite automaton} (DFA), say $A$, isdefined by a four-tuple written $A(Q, q_0, F, \delta)$ where\begin{itemize}\item $Q$ is a finite set of states,\item $q_0 \in Q$ is the start state,\item $F \subseteq Q$ are the accepting states, and\item $\delta$ is the transition function.\end{itemize}\noindent The transition function determines how to``transition'' from one state to the next state with respectto a character. We have the assumption that these transitionfunctions do not need to be defined everywhere: so it can bethe case that given a character there is no next state, inwhich case we need to raise a kind of ``failure exception''. Atypical example of a DFA is\begin{center}\begin{tikzpicture}[>=stealth',very thick,auto, every state/.style={minimum size=0pt, inner sep=2pt,draw=blue!50,very thick, fill=blue!20},scale=2]\node[state,initial] (q_0) {$q_0$};\node[state] (q_1) [right=of q_0] {$q_1$};\node[state] (q_2) [below right=of q_0] {$q_2$};\node[state] (q_3) [right=of q_2] {$q_3$};\node[state, accepting] (q_4) [right=of q_1] {$q_4$};\path[->] (q_0) edge node [above] {$a$} (q_1);\path[->] (q_1) edge node [above] {$a$} (q_4);\path[->] (q_4) edge [loop right] node {$a, b$} ();\path[->] (q_3) edge node [right] {$a$} (q_4);\path[->] (q_2) edge node [above] {$a$} (q_3);\path[->] (q_1) edge node [right] {$b$} (q_2);\path[->] (q_0) edge node [above] {$b$} (q_2);\path[->] (q_2) edge [loop left] node {$b$} ();\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below] {$b$} (q_0);\end{tikzpicture}\end{center}\noindent In this graphical notation, the accepting state$q_4$ is indicated with double circles. Note that there can bemore than one accepting state. It is also possible that a DFAhas no accepting states at all, or that the starting state isalso an accepting state. In the case above the transitionfunction is defined everywhere and can be given as a table asfollows:\[\begin{array}{lcl}(q_0, a) &\rightarrow& q_1\\(q_0, b) &\rightarrow& q_2\\(q_1, a) &\rightarrow& q_4\\(q_1, b) &\rightarrow& q_2\\(q_2, a) &\rightarrow& q_3\\(q_2, b) &\rightarrow& q_2\\(q_3, a) &\rightarrow& q_4\\(q_3, b) &\rightarrow& q_0\\(q_4, a) &\rightarrow& q_4\\(q_4, b) &\rightarrow& q_4\\\end{array}\]We need to define the notion of what language is accepted byan automaton. For this we lift the transition function$\delta$ from characters to strings as follows:\[\begin{array}{lcl}\hat{\delta}(q, []) & \dn & q\\\hat{\delta}(q, c\!::\!s) & \dn & \hat{\delta}(\delta(q, c), s)\\\end{array}\]\noindent This lifted transition function is often called``delta-hat''. Given a string, we start in the starting stateand take the first character of the string, follow to the nextsate, then take the second character and so on. Once thestring is exhausted and we end up in an accepting state, thenthis string is accepted by the automaton. Otherwise it is notaccepted. So $s$ is in the \emph{language accepted by theautomaton} $A(Q, q_0, F, \delta)$ iff\[\hat{\delta}(q_0, s) \in F \]\noindent I let you think about a definition that describesthe set of strings accepted by an automaton.While with DFAs it will always be clear that given a characterwhat the next state is (potentially none), it will be usefulto relax this restriction. That means we have severalpotential successor states. We even allow ``silenttransitions'', also called epsilon-transitions. They allow usto go from one state to the next without having a characterconsumed. We label such silent transition with the letter$\epsilon$. The resulting construction is called a\emph{non-deterministic finite automaton} (NFA) given also asa four-tuple $A(Q, q_0, F, \rho)$ where\begin{itemize}\item $Q$ is a finite set of states\item $q_0$ is a start state\item $F$ are some accepting states with $F \subseteq Q$, and\item $\rho$ is a transition relation.\end{itemize}\noindentTwo typical examples of NFAs are\begin{center}\begin{tabular}[t]{c@{\hspace{9mm}}c}\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]\node[state,initial] (q_0) {$q_0$};\node[state] (q_1) [above=of q_0] {$q_1$};\node[state, accepting] (q_2) [below=of q_0] {$q_2$};\path[->] (q_0) edge node [left] {$\epsilon$} (q_1);\path[->] (q_0) edge node [left] {$\epsilon$} (q_2);\path[->] (q_0) edge [loop right] node {$a$} ();\path[->] (q_1) edge [loop above] node {$a$} ();\path[->] (q_2) edge [loop below] node {$b$} ();\end{tikzpicture} &\raisebox{20mm}{\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]\node[state,initial] (r_1) {$r_1$};\node[state] (r_2) [above=of r_1] {$r_2$};\node[state, accepting] (r_3) [right=of r_1] {$r_3$};\path[->] (r_1) edge node [below] {$b$} (r_3);\path[->] (r_2) edge [bend left] node [above] {$a$} (r_3);\path[->] (r_1) edge [bend left] node [left] {$\epsilon$} (r_2);\path[->] (r_2) edge [bend left] node [right] {$a$} (r_1);\end{tikzpicture}}\end{tabular}\end{center}\noindent There are, however, a number of points you shouldnote. Every DFA is a NFA, but not vice versa. The $\rho$ inNFAs is a transition \emph{relation} (DFAs have a transitionfunction). The difference between a function and a relation isthat a function has always a single output, while a relationgives, roughly speaking, several outputs. Look at the NFA onthe right-hand side above: if you are currently in the state$r_2$ and you read a character $a$, then you can transition toeither $r_1$ \emph{or} $r_3$. Which route you take is notdetermined. This means if we need to decide whether a stringis accepted by a NFA, we might have to explore allpossibilities. Also there is the special silent transition inNFAs. As mentioned already this transition means you do nothave to ``consume'' any part of the input string, but``silently'' change to a different state. In the left picture,for example, if you are in the starting state, you can silently move either to $q_1$ or $q_2$.\subsubsection*{Thompson Construction}The reason for introducing NFAs is that there is a relativelysimple (recursive) translation of regular expressions intoNFAs. Consider the simple regular expressions $\varnothing$,$\epsilon$ and $c$. They can be translated as follows:\begin{center}\begin{tabular}[t]{l@{\hspace{10mm}}l}\raisebox{1mm}{$\varnothing$} & \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node[state, initial] (q_0) {$\mbox{}$};\end{tikzpicture}\\\\\raisebox{1mm}{$\epsilon$} & \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node[state, initial, accepting] (q_0) {$\mbox{}$};\end{tikzpicture}\\\\\raisebox{2mm}{$c$} & \begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node[state, initial] (q_0) {$\mbox{}$};\node[state, accepting] (q_1) [right=of q_0] {$\mbox{}$};\path[->] (q_0) edge node [below] {$c$} (q_1);\end{tikzpicture}\\\\\end{tabular}\end{center}\noindent The case for the sequence regular expression $r_1\cdot r_2$ is as follows: We are given by recursion twoautomata representing $r_1$ and $r_2$ respectively. \begin{center}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node[state, initial] (q_0) {$\mbox{}$};\node (r_1) [right=of q_0] {$\ldots$};\node[state, accepting] (t_1) [right=of r_1] {$\mbox{}$};\node[state, accepting] (t_2) [above=of t_1] {$\mbox{}$};\node[state, accepting] (t_3) [below=of t_1] {$\mbox{}$};\node[state, initial] (a_0) [right=2.5cm of t_1] {$\mbox{}$};\node (b_1) [right=of a_0] {$\ldots$};\node[state, accepting] (c_1) [right=of b_1] {$\mbox{}$};\node[state, accepting] (c_2) [above=of c_1] {$\mbox{}$};\node[state, accepting] (c_3) [below=of c_1] {$\mbox{}$};\begin{pgfonlayer}{background}\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (r_1) (t_1) (t_2) (t_3)] {};\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};\node [yshift=2mm] at (1.north) {$r_1$};\node [yshift=2mm] at (2.north) {$r_2$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent The first automaton has some accepting states. Weobtain an automaton for $r_1\cdot r_2$ by connecting theseaccepting states with $\epsilon$-transitions to the startingstate of the second automaton. By doing so we make themnon-accepting like so:\begin{center}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node[state, initial] (q_0) {$\mbox{}$};\node (r_1) [right=of q_0] {$\ldots$};\node[state] (t_1) [right=of r_1] {$\mbox{}$};\node[state] (t_2) [above=of t_1] {$\mbox{}$};\node[state] (t_3) [below=of t_1] {$\mbox{}$};\node[state] (a_0) [right=2.5cm of t_1] {$\mbox{}$};\node (b_1) [right=of a_0] {$\ldots$};\node[state, accepting] (c_1) [right=of b_1] {$\mbox{}$};\node[state, accepting] (c_2) [above=of c_1] {$\mbox{}$};\node[state, accepting] (c_3) [below=of c_1] {$\mbox{}$};\path[->] (t_1) edge node [above, pos=0.3] {$\epsilon$} (a_0);\path[->] (t_2) edge node [above] {$\epsilon$} (a_0);\path[->] (t_3) edge node [below] {$\epsilon$} (a_0);\begin{pgfonlayer}{background}\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};\node [yshift=2mm] at (3.north) {$r_1\cdot r_2$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent The case for the choice regular expression $r_1 +r_2$ is slightly different: We are given by recursion twoautomata representing $r_1$ and $r_2$ respectively. \begin{center}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node at (0,0) (1) {$\mbox{}$};\node[state, initial] (2) [above right=16mm of 1] {$\mbox{}$};\node[state, initial] (3) [below right=16mm of 1] {$\mbox{}$};\node (a) [right=of 2] {$\ldots$};\node[state, accepting] (a1) [right=of a] {$\mbox{}$};\node[state, accepting] (a2) [above=of a1] {$\mbox{}$};\node[state, accepting] (a3) [below=of a1] {$\mbox{}$};\node (b) [right=of 3] {$\ldots$};\node[state, accepting] (b1) [right=of b] {$\mbox{}$};\node[state, accepting] (b2) [above=of b1] {$\mbox{}$};\node[state, accepting] (b3) [below=of b1] {$\mbox{}$};\begin{pgfonlayer}{background}\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};\node [yshift=3mm] at (1.north) {$r_1$};\node [yshift=3mm] at (2.north) {$r_2$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent Each automaton has a single start state andpotentially several accepting states. We obtain a NFA for theregular expression $r_1 + r_2$ by introducing a new startingstate and connecting it with an $\epsilon$-transition to thetwo starting states above, like so\begin{center}\hspace{2cm}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node at (0,0) [state, initial] (1) {$\mbox{}$};\node[state] (2) [above right=16mm of 1] {$\mbox{}$};\node[state] (3) [below right=16mm of 1] {$\mbox{}$};\node (a) [right=of 2] {$\ldots$};\node[state, accepting] (a1) [right=of a] {$\mbox{}$};\node[state, accepting] (a2) [above=of a1] {$\mbox{}$};\node[state, accepting] (a3) [below=of a1] {$\mbox{}$};\node (b) [right=of 3] {$\ldots$};\node[state, accepting] (b1) [right=of b] {$\mbox{}$};\node[state, accepting] (b2) [above=of b1] {$\mbox{}$};\node[state, accepting] (b3) [below=of b1] {$\mbox{}$};\path[->] (1) edge node [above] {$\epsilon$} (2);\path[->] (1) edge node [below] {$\epsilon$} (3);\begin{pgfonlayer}{background}\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};\node [yshift=3mm] at (3.north) {$r_1+ r_2$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent Finally for the $*$-case we have an automaton for $r$\begin{center}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node at (0,0) (1) {$\mbox{}$};\node[state, initial] (2) [right=16mm of 1] {$\mbox{}$};\node (a) [right=of 2] {$\ldots$};\node[state, accepting] (a1) [right=of a] {$\mbox{}$};\node[state, accepting] (a2) [above=of a1] {$\mbox{}$};\node[state, accepting] (a3) [below=of a1] {$\mbox{}$};\begin{pgfonlayer}{background}\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};\node [yshift=3mm] at (1.north) {$r$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent and connect its accepting states to a new startingstate via $\epsilon$-transitions. This new starting state isalso an accepting state, because $r^*$ can recognise theempty string. This gives the following automaton for $r^*$:\begin{center}\begin{tikzpicture}[node distance=3mm, >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]\node at (0,0) [state, initial,accepting] (1) {$\mbox{}$};\node[state] (2) [right=16mm of 1] {$\mbox{}$};\node (a) [right=of 2] {$\ldots$};\node[state] (a1) [right=of a] {$\mbox{}$};\node[state] (a2) [above=of a1] {$\mbox{}$};\node[state] (a3) [below=of a1] {$\mbox{}$};\path[->] (1) edge node [above] {$\epsilon$} (2);\path[->] (a1) edge [bend left=45] node [above] {$\epsilon$} (1);\path[->] (a2) edge [bend right] node [below] {$\epsilon$} (1);\path[->] (a3) edge [bend left=45] node [below] {$\epsilon$} (1);\begin{pgfonlayer}{background}\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};\node [yshift=3mm] at (2.north) {$r^*$};\end{pgfonlayer}\end{tikzpicture}\end{center}\noindent This construction of a NFA from a regular expressionwas invented by Ken Thompson in 1968.\subsubsection*{Subset Construction}What is interesting is that for every NFA we can find a DFAwhich recognises the same language. This can, for example, bedone by the \emph{subset construction}. Consider again the NFAon the left, consisting of nodes labeled $0$, $1$ and $2$. \begin{center}\begin{tabular}{c@{\hspace{10mm}}c}\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=0pt, draw=blue!50,very thick,fill=blue!20}, baseline=0mm]\node[state,initial] (q_0) {$0$};\node[state] (q_1) [above=of q_0] {$1$};\node[state, accepting] (q_2) [below=of q_0] {$2$};\path[->] (q_0) edge node [left] {$\epsilon$} (q_1);\path[->] (q_0) edge node [left] {$\epsilon$} (q_2);\path[->] (q_0) edge [loop right] node {$a$} ();\path[->] (q_1) edge [loop above] node {$a$} ();\path[->] (q_2) edge [loop below] node {$b$} ();\end{tikzpicture}&\begin{tabular}{r|cl}nodes & $a$ & $b$\\\hline$\varnothing\phantom{\star}$ & $\varnothing$ & $\varnothing$\\$\{0\}\phantom{\star}$ & $\{0,1,2\}$ & $\{2\}$\\$\{1\}\phantom{\star}$ & $\{1\}$ & $\varnothing$\\$\{2\}\star$ & $\varnothing$ & $\{2\}$\\$\{0,1\}\phantom{\star}$ & $\{0,1,2\}$ & $\{2\}$\\$\{0,2\}\star$ & $\{0,1,2\}$ & $\{2\}$\\$\{1,2\}\star$ & $\{1\}$ & $\{2\}$\\s: $\{0,1,2\}\star$ & $\{0,1,2\}$ & $\{2\}$\\\end{tabular}\end{tabular}\end{center}\noindent The nodes of the DFA are given by calculating allsubsets of the set of nodes of the NFA (seen in the nodescolumn on the right). The table shows the transition functionfor the DFA. The first row states that $\varnothing$ is thesink node which has transitions for $a$ and $b$ to itself.The next three lines are calculated as follows: \begin{itemize}\item suppose you calculate the entry for the transition for $a$ and the node $\{0\}$\item start from the node $0$ in the NFA\item do as many $\epsilon$-transition as you can obtaining a set of nodes, in this case $\{0,1,2\}$\item filter out all notes that do not allow an $a$-transition from this set, this excludes $2$ which does not permit a $a$-transition\item from the remaining set, do as many $\epsilon$-transition as you can, this yields $\{0,1,2\}$ \item the resulting set specifies the transition from $\{0\}$ when given an $a$ \end{itemize}\noindent Similarly for the other entries in the rows for$\{0\}$, $\{1\}$ and $\{2\}$. The other rows are calculated byjust taking the union of the single node entries. For examplefor $a$ and $\{0,1\}$ we need to take the union of $\{0,1,2\}$(for $0$) and $\{1\}$ (for $1$). The starting state of the DFAcan be calculated from the starting state of the NFA, that is$0$, and then do as many $\epsilon$-transitions as possible.This gives $\{0,1,2\}$ which is the starting state of the DFA.The terminal states in the DFA are given by all sets thatcontain a $2$, which is the terminal state of the NFA. Thiscompletes the subset construction.There are two points to note: One is that very often theresulting DFA contains a number of ``dead'' nodes that arenever reachable from the starting state (that is that thecalculated DFA in this example is not a minimal DFA). Suchdead nodes can be safely removed without changing the languagethat is recognised by the DFA. Another point is that in somecases, however, the subset construction produces a DFA thatdoes \emph{not} contain any dead nodes\ldots{}that means itcalculates a minimal DFA. Which in turn means that in somecases the number of nodes by going from NFAs to DFAsexponentially increases, namely by $2^n$ (which is the numberof subsets you can form for $n$ nodes). \subsubsection*{Brzozowski's Method}As said before, we can also go into the other direction---fromDFAs to regular expressions. Brzozowski's method calculatesa regular expression using familiar transformations forsolving equational systems. Consider the DFA:\begin{center}\begin{tikzpicture}[scale=1.5,>=stealth',very thick,auto, every state/.style={minimum size=0pt, inner sep=2pt,draw=blue!50,very thick, fill=blue!20}] \node[state, initial] (q0) at ( 0,1) {$q_0$}; \node[state] (q1) at ( 1,1) {$q_1$}; \node[state, accepting] (q2) at ( 2,1) {$q_2$}; \path[->] (q0) edge[bend left] node[above] {$a$} (q1) (q1) edge[bend left] node[above] {$b$} (q0) (q2) edge[bend left=50] node[below] {$b$} (q0) (q1) edge node[above] {$a$} (q2) (q2) edge [loop right] node {$a$} () (q0) edge [loop below] node {$b$} ();\end{tikzpicture}\end{center}\noindent for which we can set up the following equationalsystem\begin{eqnarray}q_0 & = & \epsilon + q_0\,b + q_1\,b + q_2\,b\\q_1 & = & q_0\,a\\q_2 & = & q_1\,a + q_2\,a\end{eqnarray}\noindent There is an equation for each node in the DFA. Letus have a look how the right-hand sides of the equations areconstructed. First have a look at the second equation: theleft-hand side is $q_1$ and the right-hand side $q_0\,a$. Theright-hand side is essentially all possible ways how to end upin $q_1$. There is only one incoming edge from $q_0$ consumingan $a$. Therefore the right hand side isstate followed by character---in this case $q_0\,a$. Now letshave a look at the third equation: there are two incomingedges. Therefore we have two terms, namely $q_1\,a$ and$q_2\,a$. These terms are separated by $+$. The first statesthat if in state $q_1$ consuming an $a$ will bring you to$q_2$, and the secont that being in $q_2$ and consuming an $a$will make you stay in $q_2$. The right-hand side of thefirst equation is constructed similarly: there are three incoming edges, therefore there are three terms. There isone exception in that we also ``add'' $\epsilon$ to thefirst equation, because it corresponds to the starting statein the DFA.Having constructed the equational system, the question ishow to solve it? Remarkably the rules are very similar tosolving usual linear equational systems. For example thesecond equation does not contain the variable $q_1$ on theright-hand side of the equation. We can therefore eliminate $q_1$ from the system by just substituting this equationinto the other two. This gives\begin{eqnarray}q_0 & = & \epsilon + q_0\,b + q_0\,a\,b + q_2\,b\\q_2 & = & q_0\,a\,a + q_2\,a\end{eqnarray}\noindent where in Equation (4) we have two occurencesof $q_0$. Like the laws about $+$ and $\cdot$, we can simplify Equation (4) to obtain the following two equations:\begin{eqnarray}q_0 & = & \epsilon + q_0\,(b + a\,b) + q_2\,b\\q_2 & = & q_0\,a\,a + q_2\,a\end{eqnarray}\noindent Unfortunately we cannot make any more progress withsubstituting equations, because both (6) and (7) contain thevariable on the left-hand side also on the right-hand side.Here we need to now use a law that is different from the usuallaws. It is called \emph{Arden's rule}. It states thatif an equation is of the form $q = q\,r + s$ then it can betransformed to $q = s\, r^*$. Since we can assume $+$ is symmetric, equation (7) is of that form: $s$ is $q_0\,a\,a$and $r$ is $a$. That means we can transform Equation (7)to obtain the two new equations\begin{eqnarray}q_0 & = & \epsilon + q_0\,(b + a\,b) + q_2\,b\\q_2 & = & q_0\,a\,a\,(a^*)\end{eqnarray}\noindent Now again we can substitute the second equation intothe first in order to eliminate the variable $q_2$.\begin{eqnarray}q_0 & = & \epsilon + q_0\,(b + a\,b) + q_0\,a\,a\,(a^*)\,b\end{eqnarray}\noindent Pulling $q_0$ out as a single factor gives:\begin{eqnarray}q_0 & = & \epsilon + q_0\,(b + a\,b + a\,a\,(a^*)\,b)\end{eqnarray}\noindent This equation is again of the form so that we canapply Arden's rule ($r$ is $b + a\,b + a\,a\,(a^*)\,b$ and $s$is $\epsilon$). This gives as solution for $q_0$ the followingregular expression:\begin{eqnarray}q_0 & = & \epsilon\,(b + a\,b + a\,a\,(a^*)\,b)^*\end{eqnarray}\noindent SInce this is a regular expression, we can simplifyaway the $\epsilon$ to obtain the slightly simpler regularexpression\begin{eqnarray}q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\end{eqnarray}\noindent Now we can unwind this process and obtain the solutionsfor the other equations. This gives:\begin{eqnarray}q_0 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\\q_1 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\\q_2 & = & (b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a)^*\end{eqnarray}\noindent Finally, we only need to ``add'' up the equationswhich correspond to a terminal state. In our running example,this is just $q_2$. Consequently, a regular expressionthat recognises the same language as the automaton is\[(b + a\,b + a\,a\,(a^*)\,b)^*\,a\,a\,(a)^*\]\noindent You can somewhat crosscheck your solutionby taking a string the regular expression can match andand see whether it can be matched by the automaton.One string for example is $aaa$ and \emph{voila} this string is also matched by the automaton.We should prove that Brzozowski's method really producesan equivalent regular expression for the automaton. Butfor the purposes of this module, we omit this.\subsubsection*{Automata Minimization}As seen in the subset construction, the translation of an NFA to a DFA can result in a rather ``inefficient'' DFA. Meaning there are states that are not needed. ADFA can be \emph{minimised} by the following algorithm:\begin{enumerate}\item Take all pairs $(q, p)$ with $q \not= p$\item Mark all pairs that accepting and non-accepting states\item For all unmarked pairs $(q, p)$ and all characters $c$ test whether \begin{center} $(\delta(q, c), \delta(p,c))$ \end{center} are marked. If there is one, then also mark $(q, p)$.\item Repeat last step until no change.\item All unmarked pairs can be merged.\end{enumerate}\noindent To illustrate this algorithm, consider the following DFA.\begin{center}\begin{tikzpicture}[>=stealth',very thick,auto, every state/.style={minimum size=0pt, inner sep=2pt,draw=blue!50,very thick, fill=blue!20}]\node[state,initial] (q_0) {$q_0$};\node[state] (q_1) [right=of q_0] {$q_1$};\node[state] (q_2) [below right=of q_0] {$q_2$};\node[state] (q_3) [right=of q_2] {$q_3$};\node[state, accepting] (q_4) [right=of q_1] {$q_4$};\path[->] (q_0) edge node [above] {$a$} (q_1);\path[->] (q_1) edge node [above] {$a$} (q_4);\path[->] (q_4) edge [loop right] node {$a, b$} ();\path[->] (q_3) edge node [right] {$a$} (q_4);\path[->] (q_2) edge node [above] {$a$} (q_3);\path[->] (q_1) edge node [right] {$b$} (q_2);\path[->] (q_0) edge node [above] {$b$} (q_2);\path[->] (q_2) edge [loop left] node {$b$} ();\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below] {$b$} (q_0);\end{tikzpicture}\end{center}\noindent In Step 1 and 2 we consider essentially a triangleof the form\begin{center}\begin{tikzpicture}[scale=0.6,line width=0.8mm]\draw (0,0) -- (4,0);\draw (0,1) -- (4,1);\draw (0,2) -- (3,2);\draw (0,3) -- (2,3);\draw (0,4) -- (1,4);\draw (0,0) -- (0, 4);\draw (1,0) -- (1, 4);\draw (2,0) -- (2, 3);\draw (3,0) -- (3, 2);\draw (4,0) -- (4, 1);\draw (0.5,-0.5) node {$q_0$}; \draw (1.5,-0.5) node {$q_1$}; \draw (2.5,-0.5) node {$q_2$}; \draw (3.5,-0.5) node {$q_3$};\draw (-0.5, 3.5) node {$q_1$}; \draw (-0.5, 2.5) node {$q_2$}; \draw (-0.5, 1.5) node {$q_3$}; \draw (-0.5, 0.5) node {$q_4$}; \draw (0.5,0.5) node {\large$\star$}; \draw (1.5,0.5) node {\large$\star$}; \draw (2.5,0.5) node {\large$\star$}; \draw (3.5,0.5) node {\large$\star$};\end{tikzpicture}\end{center}\noindent where the lower row is filled with stars, because inthe corresponding pairs there is always one state that isaccepting ($q_4$) and a state that is non-accepting (the otherstates).Now in Step 3 we need to fill in more stars according whether one of the next-state pairs are marked. We have to do this for every unmarked field until there is no change anymore.This gives the triangle\begin{center}\begin{tikzpicture}[scale=0.6,line width=0.8mm]\draw (0,0) -- (4,0);\draw (0,1) -- (4,1);\draw (0,2) -- (3,2);\draw (0,3) -- (2,3);\draw (0,4) -- (1,4);\draw (0,0) -- (0, 4);\draw (1,0) -- (1, 4);\draw (2,0) -- (2, 3);\draw (3,0) -- (3, 2);\draw (4,0) -- (4, 1);\draw (0.5,-0.5) node {$q_0$}; \draw (1.5,-0.5) node {$q_1$}; \draw (2.5,-0.5) node {$q_2$}; \draw (3.5,-0.5) node {$q_3$};\draw (-0.5, 3.5) node {$q_1$}; \draw (-0.5, 2.5) node {$q_2$}; \draw (-0.5, 1.5) node {$q_3$}; \draw (-0.5, 0.5) node {$q_4$}; \draw (0.5,0.5) node {\large$\star$}; \draw (1.5,0.5) node {\large$\star$}; \draw (2.5,0.5) node {\large$\star$}; \draw (3.5,0.5) node {\large$\star$};\draw (0.5,1.5) node {\large$\star$}; \draw (2.5,1.5) node {\large$\star$}; \draw (0.5,3.5) node {\large$\star$}; \draw (1.5,2.5) node {\large$\star$}; \end{tikzpicture}\end{center}\noindent which means states $q_0$ and $q_2$, as well as $q_1$and $q_3$ can be merged. This gives the following minimal DFA\begin{center}\begin{tikzpicture}[>=stealth',very thick,auto, every state/.style={minimum size=0pt, inner sep=2pt,draw=blue!50,very thick, fill=blue!20}]\node[state,initial] (q_02) {$q_{0, 2}$};\node[state] (q_13) [right=of q_02] {$q_{1, 3}$};\node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};\path[->] (q_02) edge [bend left] node [above] {$a$} (q_13);\path[->] (q_13) edge [bend left] node [below] {$b$} (q_02);\path[->] (q_02) edge [loop below] node {$b$} ();\path[->] (q_13) edge node [above] {$a$} (q_4);\path[->] (q_4) edge [loop above] node {$a, b$} ();\end{tikzpicture}\end{center}\subsubsection*{Regular Languages}Given the constructions in the previous sections we obtain the following picture:\begin{center}\begin{tikzpicture}\node (rexp) {\bf Regexps};\node (nfa) [right=of rexp] {\bf NFAs};\node (dfa) [right=of nfa] {\bf DFAs};\node (mdfa) [right=of dfa] {\bf\begin{tabular}{c}minimal\\ DFAs\end{tabular}};\path[->,line width=1mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);\path[->,line width=1mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);\path[->,line width=1mm] (dfa) edge node [below=5mm, black] {minimisation} (mdfa);\path[->,line width=1mm] (dfa) edge [bend left=45] (rexp);\end{tikzpicture}\end{center}\noindent By going from regular expressions over NFAs to DFAs,we can always ensure that for every regular expression thereexists a NFA and DFA that can recognise the same language.Although we did not prove this fact. Similarly by going fromDFAs to regular expressions, we can make sure for every DFA there exists a regular expression that can recognise the samelanguage. Again we did not prove this fact. The interesting conclusion is that automata and regular expressions can recognise the same set of languages:\begin{quote} A language is \emph{regular} iff there exists aregular expression that recognises all its strings.\end{quote}\noindent or equivalently \begin{quote} A language is \emph{regular} iff there exists anautomaton that recognises all its strings.\end{quote}\noindent So for deciding whether a string is recognised by aregular expression, we could use our algorithm based onderivatives or NFAs or DFAs. But let us quickly look at whatthe differences mean in computational terms. Translating aregular expression into a NFA gives us an automaton that has$O(n)$ nodes---that means the size of the NFA grows linearlywith the size of the regular expression. The problem with NFAsis that the problem of deciding whether a string is acceptedis computationally not cheap. Remember with NFAs we havepotentially many next states even for the same input and alsohave the silent $\epsilon$-transitions. If we want to find apath from the starting state of an NFA to an accepting state,we need to consider all possibilities. In Ruby and Python thisis done by a depth-first search, which in turn means that if a``wrong'' choice is made, the algorithm has to backtrack andthus explore all potential candidates. This is exactly thereason why Ruby and Python are so slow for evil regularexpressions. The alternative is to explore the search spacein a breadth-first fashion, but this might incur a memorypenalty. To avoid the problems with NFAs, we can translate them into DFAs. With DFAs the problem of deciding whether astring is recognised or not is much simpler, because ineach state it is completely determined what the nextstate will be for a given input. So no search is needed.The problem with this is that the translation to DFAscan explode exponentially the number of states. Therefore when this route is taken, we definitely need to minimise theresulting DFAs in order to have an acceptable memory and runtime behaviour.But this does not mean that everything is bad with automata.Recall the problem of finding a regular expressions for thelanguage that is \emph{not} recognised by a regularexpression. In our implementation we added explicitly such aregular expressions because they are useful for recognisingcomments. But in principle we did not need to. The argumentfor this is as follows: take a regular expression, translateit into a NFA and DFA that recognise the same language. Onceyou have the DFA it is very easy to construct the automatonfor the language not recognised by an DFA. If the DAF iscompleted (this is important!), then you just need to exchangethe accepting and non-accepting states. You can then translatethis DFA back into a regular expression. Not all languages are regular. The most well-known exampleof a language that is not regular consists of all the stringsof the form\[a^n\,b^n\]\noindent meaning strings that have the same number of $a$sand $b$s. You can try, but you cannot find a regularexpression for this language and also not an automaton. Onecan actually prove that there is no regular expression norautomaton for this language, but again that would lead us toofar afield for what we want to do in this module.\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: