# HG changeset patch # User Christian Urban # Date 1443825854 -3600 # Node ID 539b2e88f5b9a07a57b08429e6a804892fceae74 # Parent c235e0aeb8df11fe89056b34799b16cdaef66f89 updated diff -r c235e0aeb8df -r 539b2e88f5b9 handouts/ho02.pdf Binary file handouts/ho02.pdf has changed 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} diff -r c235e0aeb8df -r 539b2e88f5b9 progs/app6.scala --- a/progs/app6.scala Fri Oct 02 08:48:46 2015 +0100 +++ b/progs/app6.scala Fri Oct 02 23:44:14 2015 +0100 @@ -1,22 +1,18 @@ def simp(r: Rexp): Rexp = r match { case ALT(r1, r2) => { - val r1s = simp(r1) - val r2s = simp(r2) - (r1s, r2s) match { - case (NULL, _) => r2s - case (_, NULL) => r1s - case _ => if (r1s == r2s) r1s else ALT(r1s, r2s) + (simp(r1), simp(r2)) match { + case (NULL, r2s) => r2s + case (r1s, NULL) => r1s + case (r1s, r2s) => if (r1s == r2s) r1s else ALT(r1s, r2s) } } case SEQ(r1, r2) => { - val r1s = simp(r1) - val r2s = simp(r2) - (r1s, r2s) match { + (simp(r1), simp(r2)) match { case (NULL, _) => NULL case (_, NULL) => NULL - case (EMPTY, _) => r2s - case (_, EMPTY) => r1s - case _ => SEQ(r1s, r2s) + case (EMPTY, r2s) => r2s + case (r1s, EMPTY) => r1s + case (r1s, r2s) => SEQ(r1s, r2s) } } case NTIMES(r, n) => NTIMES(simp(r), n) diff -r c235e0aeb8df -r 539b2e88f5b9 progs/re1.scala --- a/progs/re1.scala Fri Oct 02 08:48:46 2015 +0100 +++ b/progs/re1.scala Fri Oct 02 23:44:14 2015 +0100 @@ -39,10 +39,10 @@ def matches(r: Rexp, s: String) : Boolean = nullable(ders(s.toList, r)) //example from the homework -//val r = STAR(ALT(SEQ(CHAR('a'), CHAR('b')), CHAR('b'))) -//der('a', r) -//der('b', r) -//der('c', r) +val r = STAR(ALT(SEQ(CHAR('a'), CHAR('b')), CHAR('b'))) +der('a', r) +der('b', r) +der('c', r) //optional: one or zero times def OPT(r: Rexp) = ALT(r, EMPTY) diff -r c235e0aeb8df -r 539b2e88f5b9 progs/re2.scala --- a/progs/re2.scala Fri Oct 02 08:48:46 2015 +0100 +++ b/progs/re2.scala Fri Oct 02 23:44:14 2015 +0100 @@ -50,9 +50,9 @@ (end - start)/(i * 1.0e9) } -for (i <- 1 to 100) { - println(i + ": " + "%.5f".format(time_needed(1, matches(EVIL(i), "a" * i)))) -} +//for (i <- 1 to 100) { +// println(i + ": " + "%.5f".format(time_needed(1, matches(EVIL(i), "a" * i)))) +//} //a bit bolder test for (i <- 1 to 1000 by 50) {