
diff -r ffbc65112d48 -r 057b4603b940 handouts/ho02.tex
--- a/handouts/ho02.tex	Fri Apr 28 11:01:25 2017 +0100
+++ b/handouts/ho02.tex	Sun May 07 00:20:58 2017 +0100
@@ -52,16 +52,17 @@
 \begin{tikzpicture}
   \begin{axis}[
     xlabel={$n$},
-    x label style={at={(1.05,0.0)}},
+    x label style={at={(1.1,0.0)}},
+    %%xtick={0,1000000,...,5000000}, 
     ylabel={time in secs},
     enlargelimits=false,
     ymax=35,
     ytick={0,5,...,30},
     axis lines=left,
-    scaled ticks=false,
+    %scaled ticks=false,
     width=6.5cm,
     height=5cm,
-    legend entries={Scala V3},  
+    legend entries={Our matcher},  
     legend pos=north east,
     legend cell align=left]
 %\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};    
@@ -69,7 +70,7 @@
 \end{axis}
 \end{tikzpicture}
 \end{tabular}
-\end{center}
+\end{center}\bigskip
 
 \begin{center}
 Graphs: $a^{?\{n\}} \cdot a^{\{n\}}$ and strings $\underbrace{a\ldots a}_{n}$\\
@@ -110,7 +111,7 @@
     axis lines=left,
     width=6.5cm,
     height=5cm,
-    legend entries={Scala V3},  
+    legend entries={Our matcher},  
     legend pos=north east,
     legend cell align=left]
 %\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
@@ -119,14 +120,14 @@
 \end{tikzpicture}
 \end{tabular}
 \end{center}
-\medskip
+\bigskip
 
 \noindent
-We will use these regular expressions and strings as running
-examples. There will be several versions (V1, V2, V3,\ldots) of the
-algorithm.\footnote{The corresponding files are \texttt{re1.scala},
-  \texttt{re2.scala} and so on. As usual, you can find the code on
-  KEATS.}\bigskip
+In what follows we will use these regular expressions and strings as
+running examples. There will be several versions (V1, V2, V3,\ldots)
+of our matcher.\footnote{The corresponding files are
+  \texttt{re1.scala}, \texttt{re2.scala} and so on. As usual, you can
+  find the code on KEATS.}\bigskip
 
 \noindent
 Having specified in the previous lecture what
@@ -138,7 +139,7 @@
 s \in L(r)
 \]
 
-\noindent we can look at an algorithm to solve this problem. Clearly
+\noindent we can look for an algorithm to solve this problem. Clearly
 we cannot use the function $L$ directly for this, because in general
 the set of strings $L$ returns is infinite (recall what $L(a^*)$ is).
 In such cases there is no way we can implement an exhaustive test for
@@ -237,13 +238,14 @@
 \end{equation}
 
 \noindent If we can find an equivalent regular expression that is
-simpler (smaller for example), then this might potentially make our
-matching algorithm run faster. We can look for such a simpler regular
-expression $r'$ because 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 just $r_1$. You can verify this by iteratively applying the
-simplification rules from above:
+simpler (that usually means smaller), then this might potentially make
+our matching algorithm run faster. We can look for such a simpler
+regular expression $r'$ because whether a string $s$ is in $L(r)$ or
+in $L(r')$ with $r\equiv r'$ will always give the same answer. Yes?
+
+In the example above you will see that the regular expression is
+equivalent to just $r_1$. You can verify this by iteratively applying
+the simplification rules from above:
 
 \begin{center}
 \begin{tabular}{ll}
@@ -264,7 +266,7 @@
 $\ZERO$s, therefore simplifying them away will make the
 algorithm quite a bit faster.
 
-Finally here are three equivalences between regulare expressions which are
+Finally here are three equivalences between regular expressions which are
 not so obvious:
 
 \begin{center}
@@ -276,9 +278,11 @@
 \end{center}
 
 \noindent
-You can try to establish them. As an aside, there has been a lot of research
-in questions like: Can one always decide when two regular expressions are
-equivalent or not? What does an algorithm look like to decide this?
+We will not use them in our algorithm, but feel free to make sure they
+hold. As an aside, there has been a lot of research about questions
+like: Can one always decide when two regular expressions are
+equivalent or not? What does an algorithm look like to decide this
+efficiently?
 
 \subsection*{The Matching Algorithm}
 
@@ -315,10 +319,10 @@
 \emph{derivative} of a regular expression. This is a function
 which will take a regular expression, say $r$, and a
 character, say $c$, as arguments and returns a new regular
-expression. Be careful that the intuition behind this function
+expression. Be mindful that the intuition behind this function
 is not so easy to grasp on first reading. Essentially this
 function solves the following problem: if $r$ can match a
-string of the form $c\!::\!s$, what does the regular
+string of the form $c\!::\!s$, what does a regular
 expression look like that can match just $s$? The definition
 of this function is as follows:
 
@@ -372,9 +376,9 @@
 and ``append'' $r^*$ in order to match the rest of $s$. Still
 makes sense?
 
-If all this did not make sense yet, here is another way to rationalise
-the definition of $\textit{der}$ by considering the following operation
-on sets:
+If all this did not make sense yet, here is another way to explain the
+definition of $\textit{der}$ by considering the following operation on
+sets:
 
 \begin{equation}\label{Der}
 \textit{Der}\,c\,A\;\dn\;\{s\,|\,c\!::\!s \in A\}
@@ -454,7 +458,7 @@
 \end{center}
 
 \noindent This function iterates $\textit{der}$ taking one character at
-the time from the original string until it is exhausted.
+the time from the original string until the string is exhausted.
 Having $\textit{der}s$ in place, we can finally define our matching
 algorithm:
 
@@ -493,11 +497,13 @@
   \lstinputlisting[numbers=left,linebackgroundcolor=
                   {\ifodd\value{lstnumber}\color{capri!3}\fi}]
                   {../progs/app5.scala}
-\caption{Scala implementation of the \textit{nullable} and 
+\caption{A Scala implementation of the \textit{nullable} and 
   derivative functions. These functions are easy to
-  implement in functional languages, because their built-in pattern 
+  implement in functional languages. This is because pattern 
   matching and recursion allow us to mimic the mathematical
-  definitions very closely.\label{scala1}}
+  definitions very closely. Nearly all functional
+  programming languages support pattern matching and
+  recursion out of the box.\label{scala1}}
 \end{figure}
 
 
@@ -538,8 +544,8 @@
 
 For running the algorithm with our first example, the evil
 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
+the optional regular expression and the `exactly $n$-times
+regular expression'. This can be done with the translations
 
 \lstinputlisting[numbers=none]{../progs/app51.scala}
 
@@ -572,8 +578,8 @@
 \end{tikzpicture}
 \end{center}
 
-\noindent Analysing this failure we notice that for
-$a^{\{n\}}$ we generate quite big regular expressions:
+\noindent Analysing this failure we notice that for $a^{\{n\}}$, for
+example, we generate quite big regular expressions:
 
 \begin{center}
 \begin{tabular}{rl}
@@ -591,7 +597,7 @@
 large regular expressions will cause problems. This problem
 is aggravated by $a^?$ being represented as $a + \ONE$.
 
-We can however fix this by having an explicit constructor for
+We can however fix this easily by having an explicit constructor for
 $r^{\{n\}}$. In Scala we would introduce a constructor like
 
 \begin{center}
@@ -634,8 +640,8 @@
 25 seconds handle regular expressions up to $n = 1,100$ before a
 StackOverflow is raised. Recall that Python and Ruby (and our first
 version, Scala V1) could only handle $n = 27$ or so in 30
-seconds. There is no change for our second example $(a^*)^* \cdot
-b$---so this is still good.
+seconds. We have not tried our algorithm on the second example $(a^*)^* \cdot
+b$---but it is doing OK with it.
 
 
 The moral is that our algorithm is rather sensitive to the
@@ -656,9 +662,9 @@
 \end{center}
 
 \noindent 
-If we simplify them according to the simple rules from the
-beginning, we can replace the right-hand sides by the 
-smaller equivalent regular expressions
+If we simplify them according to the simplification rules from the
+beginning, we can replace the right-hand sides by the smaller
+equivalent regular expressions
 
 \begin{center}
 \begin{tabular}{l}
@@ -726,7 +732,7 @@
 up to 11,000 \texttt{a}s.  Similarly, Java and Python needed 30
 seconds to find out the regular expression $(a^*)^* \cdot b$ does not
 match the string of 28 \texttt{a}s. We can do the same in
-for strings of 6,000,000 \texttt{a}s:
+for strings composed of nearly 6,000,000 \texttt{a}s:
 
 
 \begin{center}
@@ -739,7 +745,7 @@
     ymax=35,
     ytick={0,5,...,30},
     axis lines=left,
-    scaled ticks=false,
+    %scaled ticks=false,
     x label style={at={(1.09,0.0)}},
     %xmax=7700000,
     width=9cm,
@@ -755,12 +761,11 @@
 
 \subsection*{Epilogue}
 
-(23/Aug/2016) I recently found another place where this algorithm can be 
-sped up (this idea is not integrated with what is coming next,
-but I present it nonetheless). The idea is to define \texttt{ders}
-not such that it iterates the derivative character-by-character, but
-in bigger chunks. The resulting code for \texttt{ders2} looks as
-follows:
+(23/Aug/2016) I recently found another place where this algorithm can
+be sped up (this idea is not integrated with what is coming next, but
+I present it nonetheless). The idea is to not define \texttt{ders}
+that it iterates the derivative character-by-character, but in bigger
+chunks. The resulting code for \texttt{ders2} looks as follows:
 
 \lstinputlisting[numbers=none]{../progs/app52.scala} 
 
@@ -790,7 +795,7 @@
     ymax=33,
     %scaled ticks=false,
     axis lines=left,
-    width=5.5cm,
+    width=5.3cm,
     height=5cm, 
     legend entries={Scala V3, Scala V4},
     legend style={at={(0.1,-0.2)},anchor=north}]
@@ -806,12 +811,12 @@
     x label style={at={(1.09,0.0)}},
     ylabel={time in secs},
     enlargelimits=false,
-    xmax=8100000,
+    xmax=8200000,
     ytick={0,5,...,30},
     ymax=33,
     %scaled ticks=false,
     axis lines=left,
-    width=5.5cm,
+    width=5.3cm,
     height=5cm, 
     legend entries={Scala V3, Scala V4},
     legend style={at={(0.1,-0.2)},anchor=north}]
@@ -827,7 +832,7 @@
 
 You might not like doing proofs. But they serve a very
 important purpose in Computer Science: How can we be sure that
-our algorithm matches its specification. We can try to test
+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
@@ -848,7 +853,7 @@
   \end{tabular}
 \end{center}
 
-\noindent If you want to show a property $P(r)$ for all 
+\noindent If you want to show a property $P(r)$ for \emph{all} 
 regular expressions $r$, then you have to follow essentially 
 the recipe:
 
@@ -900,8 +905,9 @@
 \label{propalt}
 \end{equation}
 
-\noindent The difference to the base cases is that in this
-case we can already assume we proved
+\noindent The difference to the base cases is that in the inductive
+cases we can already assume we proved $P$ for the components, that is
+we can assume.
 
 \begin{center}
 \begin{tabular}{l}
@@ -910,9 +916,9 @@
 \end{tabular}
 \end{center}
 
-\noindent These are the induction hypotheses. To check this 
+\noindent These are called the induction hypotheses. To check this 
 case, we can start from $\textit{nullable}(r_1 + r_2)$, which by 
-definition is
+definition of $\textit{nullable}$ is
 
 \[
 \textit{nullable}(r_1) \vee \textit{nullable}(r_2)
@@ -935,18 +941,18 @@
 [] \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 according to
+\noindent but this is by definition of $L$ exactly $[] \in L(r_1 +
+r_2)$, which we needed to establish according to statement in
 \eqref{propalt}. What we have shown is that starting from
 $\textit{nullable}(r_1 + r_2)$ we have done equivalent transformations
-to end up with $[] \in L(r_1 + r_2)$. Consequently we have
-established that $P(r_1 + r_2)$ holds.
+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 \mbox{$P(r_1\cdot r_2)$} and $P(r^*)$. Again I let you
 check the details.
 
-You might have to do induction proofs over strings. 
+You might also 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
@@ -982,8 +988,9 @@
 L(\textit{der}\,c\,r) = \textit{Der}\,c\,(L(r))
 \]
 
-\noindent holds (this would be of course a property that
-needs to be proved in a side-lemma by induction on $r$).
+\noindent holds (this would be of course another property that needs
+to be proved in a side-lemma by induction on $r$). This is a bit
+more challenging, but not impossible.
 
 To sum up, using reasoning like the one shown above allows us 
 to show the correctness of our algorithm. To see this,
@@ -1002,9 +1009,9 @@
 \label{dersstep}
 \end{equation}
 
-\noindent But we have shown above in \eqref{dersprop}, that
-the $\textit{Ders}$ can be replaced by $L(\textit{ders}\ldots)$. That means 
-\eqref{dersstep} is equivalent to 
+\noindent You agree?  But we have shown above in \eqref{dersprop},
+that the $\textit{Ders}$ can be replaced by
+$L(\textit{ders}\ldots)$. That means \eqref{dersstep} is equivalent to
 
 \begin{equation}
 [] \in L(\textit{ders}\,s\,r)
@@ -1033,11 +1040,13 @@
 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.
+\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 \emph{induction
+recipes} is already a big step in actually performing these proofs.
+If you do not believe it, proofs have helped me to make sure my code
+is correct and in several instances prevented me of letting slip
+embarassing mistakes into the `wild'.
 
 \end{document}
 




