--- a/handouts/ho02.tex Thu Oct 01 23:09:20 2015 +0100
+++ b/handouts/ho02.tex Thu Oct 01 23:25:11 2015 +0100
@@ -570,7 +570,69 @@
\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.
+For the programs we look at in this module, the proofs will
+mostly by some form of induction. Remember that regular
+expressions are defined as
+
+\begin{center}
+\begin{tabular}{r@{\hspace{1mm}}r@{\hspace{1mm}}l@{\hspace{13mm}}l}
+ $r$ & $::=$ & $\varnothing$ & null\\
+ & $\mid$ & $\epsilon$ & empty string / \texttt{""} / []\\
+ & $\mid$ & $c$ & single character\\
+ & $\mid$ & $r_1 + r_2$ & alternative / choice\\
+ & $\mid$ & $r_1 \cdot r_2$ & sequence\\
+ & $\mid$ & $r^*$ & star (zero or more)\\
+ \end{tabular}
+\end{center}
+
+\noindent If you want to show a property $P(r)$ for all
+regular expressions $r$, then you have to follow essentially
+the recipe:
+
+\begin{itemize}
+\item $P$ has to hold for $\varnothing$, $\epsilon$ and $c$
+ (these are the base cases).
+\item $P$ has to hold for $r_1 + r_2$ under the assumption
+ that $P$ already holds for $r_1$ and $r_2$.
+\item $P$ has to hold for $r_1 \cdot r_2$ under the
+ assumption that $P$ already holds for $r_1$ and $r_2$.
+\item $P$ has to hold for $r^*$ under the assumption
+ that $P$ already holds for $r$.
+\end{itemize}
+
+\noindent
+A simple proof is for example showing the following
+property:
+
+\[
+nullable(r) \;\;\text{if and only if}\;\; []\in L(r)
+\]
+
+\noindent
+Let us say that this property is $P(r)$, then the first case
+we need to check is whether $P(\varnothing)$ (see recipe
+above). So we have to show that
+
+\[
+nullable(\varnothing) \;\;\text{if and only if}\;\;
+[]\in L(\varnothing)
+\]
+
+\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.
+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.
\end{document}