
diff -r c235e0aeb8df -r 539b2e88f5b9 handouts/ho02.tex
--- 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}
 
 




