# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1443738311 -3600
# Node ID bc395ccfba7f076dc28df4df3b3f4ef1ca72cca7
# Parent  f16120cb4e194693319ce021a4da0bd7f8779b6d
updated

diff -r f16120cb4e19 -r bc395ccfba7f handouts/ho02.pdf
Binary file handouts/ho02.pdf has changed
diff -r f16120cb4e19 -r bc395ccfba7f handouts/ho02.tex
--- 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}