--- a/handouts/ho02.tex Fri Oct 02 08:48:46 2015 +0100
+++ b/handouts/ho02.tex Fri Oct 02 23:44:14 2015 +0100
@@ -14,7 +14,7 @@
than the matchers from regular expression libraries in Ruby
and Python (the plots on the left). These plots show the
running time for the evil regular expression
-$a?^{\{n\}}a^{\{n\}}$ and string composed of $n$ \pcode{a}s.
+$a^?^{\{n\}}\cdot a^{\{n\}}$ and strings composed of $n$ \pcode{a}s.
We will use this regular expression and strings as running
example. To see the substantial differences in the two plots
below, note the different scales of the $x$-axes.
@@ -158,7 +158,7 @@
unchanged. Be careful to fully comprehend the fifth and sixth
equivalence: if you concatenate two sets of strings and one is
the empty set, then the concatenation will also be the empty
-set. To see this, check the definition of \pcode{_ @ _}. The
+set. To see this, check the definition of $\_ @ \_$. The
last equivalence is again trivial.
What will be important later on is that we can orient these
@@ -176,7 +176,7 @@
make our matching algorithm run faster. The reason is that
whether a string $s$ is in $L(r)$ or in $L(r')$ with $r\equiv
r'$ will always give the same answer. In the example above you
-will see that the regular expression is equivalent to $r_1$.
+will see that the regular expression is equivalent to just $r_1$.
You can verify this by iteratively applying the simplification
rules from above:
@@ -300,8 +300,11 @@
strings $A$ by filtering out all strings that do not start
with $c$ and then strips off the $c$ from all the remaining
strings. For example suppose $A = \{f\!oo, bar, f\!rak\}$ then
-\[ Der\,f\,A = \{oo, rak\}\quad,\quad Der\,b\,A = \{ar\} \quad
-\text{and} \quad Der\,a\,A = \varnothing \]
+
+\[ Der\,f\,A = \{oo, rak\}\quad,\quad
+ Der\,b\,A = \{ar\} \quad \text{and} \quad
+ Der\,a\,A = \{\}
+\]
\noindent
Note that in the last case $Der$ is empty, because no string in $A$
@@ -410,7 +413,7 @@
\end{figure}
For running the algorithm with our favourite example, the evil
-regular expression $a?^{\{n\}}a^{\{n\}}$, we need to implement
+regular expression $a^?^{\{n\}}a^{\{n\}}$, we need to implement
the optional regular expression and the exactly $n$-times
regular expression. This can be done with the translations
@@ -457,7 +460,7 @@
\noindent Our algorithm traverses such regular expressions at
least once every time a derivative is calculated. So having
large regular expressions will cause problems. This problem
-is aggravated by $a?$ being represented as $a + \epsilon$.
+is aggravated by $a^?$ being represented as $a + \epsilon$.
We can however fix this by having an explicit constructor for
$r^{\{n\}}$. In Scala we would introduce a constructor like
@@ -495,7 +498,9 @@
\noindent Now we are talking business! The modified matcher
can within 30 seconds handle regular expressions up to
-$n = 950$ before a StackOverflow is raised.
+$n = 950$ before a StackOverflow is raised. Python and Ruby
+(and our first version) could only handle $n = 27$ or so in 30
+second.
The moral is that our algorithm is rather sensitive to the
size of regular expressions it needs to handle. This is of
@@ -546,7 +551,8 @@
\caption{The simplification function and modified
\texttt{ders}-function; this function now
calls \texttt{der} first, but then simplifies
-the resulting derivative regular expressions, see
+the resulting derivative regular expressions before
+building the next derivative, see
Line~28.\label{scala2}}
\end{figure}
@@ -560,7 +566,7 @@
scaled ticks=false,
axis lines=left,
width=9cm,
- height=4cm,
+ height=5cm,
legend entries={Scala V2,Scala V3}]
\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
@@ -571,12 +577,12 @@
\section*{Proofs}
You might not like doing proofs. But they serve a very
-important purpose in Computer Science: When can we be sure
-that our algorithms match their specification. We can try to
-test the algorithms, but that often overlooks corner cases and
-also often an exhaustive testing is impossible (since there
-are often infinitely many inputs). Proofs allow us to ensure
-that an algorithm meets its specification.
+important purpose in Computer Science: How can we be sure that
+our algorithm matches its specification. We can try to test
+the algorithm, but that often overlooks corner cases and an
+exhaustive testing is impossible (since there are infinitely
+many inputs). Proofs allow us to ensure that an algorithm
+really meets its specification.
For the programs we look at in this module, the proofs will
mostly by some form of induction. Remember that regular
@@ -612,9 +618,10 @@
A simple proof is for example showing the following
property:
-\[
+\begin{equation}
nullable(r) \;\;\text{if and only if}\;\; []\in L(r)
-\]
+\label{nullableprop}
+\end{equation}
\noindent
Let us say that this property is $P(r)$, then the first case
@@ -627,41 +634,43 @@
\]
\noindent whereby $nullable(\varnothing)$ is by definition of
-the function $nullable$ always $\textit{false}$. We also
-have that $L(\varnothing)$ is by definition $\{\}$. It is
-impossible that the empty string $[]$ is in the empty set.
+the function $nullable$ always $\textit{false}$. We also have
+that $L(\varnothing)$ is by definition $\{\}$. It is
+impossible that the empty string $[]$ is in the empty set.
Therefore also the right-hand side is false. Consequently we
-verified this case. We would still need to do this for
-$P(\varepsilon)$ and $P(c)$. I leave this to you to check.
+verified this case: both sides are false. We would still need
+to do this for $P(\varepsilon)$ and $P(c)$. I leave this to
+you to verify.
Next we need to check the inductive cases, for example
$P(r_1 + r_2)$, which is
-\[
+\begin{equation}
nullable(r_1 + r_2) \;\;\text{if and only if}\;\;
[]\in L(r_1 + r_2)
-\]
+\label{propalt}
+\end{equation}
\noindent The difference to the base cases is that in this
case we can already assume we proved
\begin{center}
\begin{tabular}{l}
-$nullable(r_1) \;\;\text{if and only if}\;\; []\in L(r_1)$\\
+$nullable(r_1) \;\;\text{if and only if}\;\; []\in L(r_1)$ and\\
$nullable(r_2) \;\;\text{if and only if}\;\; []\in L(r_2)$\\
\end{tabular}
\end{center}
\noindent These are the induction hypotheses. To check this
-case we can start from $nullable(r_1 + r_2)$, which by
+case, we can start from $nullable(r_1 + r_2)$, which by
definition is
\[
nullable(r_1) \vee nullable(r_2)
\]
-\noindent Using the induction hypotheses we can transform
-this into
+\noindent Using the two induction hypotheses from above,
+we can transform this into
\[
[] \in L(r_1) \vee []\in(r_2)
@@ -670,25 +679,25 @@
\noindent We just replaced the $nullable(\ldots)$ parts by
the equivalent $[] \in L(\ldots)$ from the induction
hypotheses. A bit of thinking convinces you that if
-$[] \in L(r_1) \vee []\in(r_2)$ then the empty string
+$[] \in L(r_1) \vee []\in L(r_2)$ then the empty string
must be in the union $L(r_1)\cup L(r_2)$, that is
\[
[] \in L(r_1)\cup L(r_2)
\]
-\noindent but this is by definition of $L$ exactly
-$[] \in L(r_1 + r_2)$, which we needed to establish.
-What we have shown is that starting from
+\noindent but this is by definition of $L$ exactly $[] \in
+L(r_1 + r_2)$, which we needed to establish according to
+\eqref{propalt}. What we have shown is that starting from
$nullable(r_1 + r_2)$ we have done equivalent transformations
-to end up with $[] \in L(r_1 + r_2)$. Consequently we have
+to end up with $[] \in L(r_1 + r_2)$. Consequently we have
established that $P(r_1 + r_2)$ holds.
In order to complete the proof we would now need to look
-at the cases $P(r_1\cdot r_2)$ and $P(r^*)$. Again I let you
+at the cases \mbox{$P(r_1\cdot r_2)$} and $P(r^*)$. Again I let you
check the details.
-Finally, you might have to do induction proofs over strings.
+You might have to do induction proofs over strings.
That means you want to establish a property $P(s)$ for all
strings $s$. For this remember strings are lists of
characters. These lists can be either the empty list or a
@@ -704,12 +713,13 @@
\noindent
Given this recipe, I let you show
-\[
+\begin{equation}
Ders\,s\,(L(r)) = L(ders\,s\,r)
-\]
+\label{dersprop}
+\end{equation}
-\noindent by induction on $s$. In this proof you can
-assume the property for $der$ and $Der$ has already been
+\noindent by induction on $s$. In this proof you can assume
+the following property for $der$ and $Der$ has already been
proved, that is you can assume
\[
@@ -719,6 +729,60 @@
\noindent holds (this would be of course a property that
needs to be proved in a side-lemma by induction on $r$).
+To sum up, using reasoning like the one shown above allows us
+to show the correctness of our algorithm. To see this,
+start from the specification
+
+\[
+s \in L(r)
+\]
+
+\noindent That is the problem we want to solve. Thinking a
+little, you will see that this problem is equivalent to the
+following problem
+
+\begin{equation}
+[] \in Ders\,s\,(L(r))
+\label{dersstep}
+\end{equation}
+
+\noindent But we have shown above in \eqref{dersprop}, that
+the $Ders$ can be replaced by $L(ders\ldots)$. That means
+\eqref{dersstep} is equivalent to
+
+\begin{equation}
+[] \in L(ders\,s\,r)
+\label{prefinalstep}
+\end{equation}
+
+\noindent We have also shown that testing whether the empty
+string is in a language is equivalent to the $nullable$
+function; see \eqref{nullableprop}. That means
+\eqref{prefinalstep} is equivalent with
+
+\[
+nullable(ders\,s\,r)
+\]
+
+\noindent But this is just the definition of $matches$
+
+\[
+matches\,s\,r \dn nullable(ders\,s\,r)
+\]
+
+\noindent In effect we have shown
+
+\[
+matches\,s\,r\;\;\text{if and only if}\;\;
+s\in L(r)
+\]
+
+\noindent which is the property we set out to prove:
+our algorithm meets its specification. To have done
+so, requires a few induction proofs about strings and
+regular expressions. Following the recipes is already a big
+step in performing these proofs.
+
\end{document}