summaryrefslogtreecommitdiff
path: root/analyse-proof.tex
diff options
context:
space:
mode:
authorCamil Staps2016-06-15 16:10:02 +0200
committerCamil Staps2016-06-15 16:10:02 +0200
commitf54b8382e965660668bba4ed94e19d07e9456f2d (patch)
treedaeeb6bc276c9b60cdc6e9e45a4f0636307d72b0 /analyse-proof.tex
parentAlle bomen toegevoegd (diff)
Bewijs
Diffstat (limited to 'analyse-proof.tex')
-rw-r--r--analyse-proof.tex122
1 files changed, 122 insertions, 0 deletions
diff --git a/analyse-proof.tex b/analyse-proof.tex
new file mode 100644
index 0000000..5cc8e6a
--- /dev/null
+++ b/analyse-proof.tex
@@ -0,0 +1,122 @@
+% vim: spelllang=nl:
+\subsection{Bewijs}
+\label{sec:analyse:proof}
+
+We zullen het buitenste programma als beschreven op~\pageref{pgm:reverse} met
+$P_1$ aanduiden, en het recursieve binnenste programma met $P_2$.
+
+Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait,
+oftewel: er is een afleidingsboom voor
+$$
+\trans
+ {P_1}{[s:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[s^R:\Nil]}{\emptystore}
+$$
+
+voor alle $s\in\String$, met
+\begin{align*}
+ \lambda^R &= \lambda, \\
+ (c~s)^R &= s^R c.
+\end{align*}
+
+Het bewijs gaat in twee stappen. Eerst bewijzen we dat $P_2$ de eerste string
+op de stack achter de omgedraaide versie van de tweede string op de stack
+plaatst, en dat output. Dit wordt bewezen in \autoref{thm:p2}. Hiermee kunnen
+we van $P_1$ bewijzen dat het de eerste string op de stack omgedraaid output.
+Dit doen we in \autoref{thm:p1}.
+
+\begin{thm}
+ {
+ Voor alle $s,t\in\String$ met $t\ne\lambda$ hebben we een afleidingsboom
+ voor
+ \normalfont
+ \belowdisplayskip=-1em
+ $$
+ \trans
+ {P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[t^R~s:\Nil]}{\emptystore}.
+ $$
+ }
+ \label{thm:p2}
+ \begin{proof}[Bewijs]
+ Met inductie naar de lengte van $t$.
+
+ Inductiebasis: stel $t=c$, met $c$ een willekeurig karakter. In dit geval
+ krijgen we de boom in \autoref{fig:tree:bootstrap-base}. Hier is $c$ geen
+ variabele maar het werkelijke karakter \lit{c}. We kunnen \emph{CleanSmurf}
+ namelijk helaas nog niet vertellen dat een bepaalde variabele lengte $1$
+ heeft. Uit de afleidingsboom blijkt dat $c$ niet gebruikt wordt als naam in
+ de variable store, waardoor we ons geen zorgen hoeven te maken over
+ situaties waar $c$ gelijk is aan \'e\'en van de variabelenamen die we
+ gebruiken. Uit de boom in \autoref{fig:tree:bootstrap-base} volgt dus dat
+ bovenstaande stelling geldt voor $t$ van lengte $1$.
+
+ \medskip
+ Inductiestap: we nemen aan dat we een afleidingsboom hebben voor
+ \begin{equation}\tag{IH}\label{eq:p2:ih}
+ \trans
+ {P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[t^R:s:\Nil]}{\emptystore}
+ \end{equation}
+
+ Vervolgens laten we zien dat we voor elke $c\in\Char$ ook een
+ afleidingsboom hebben voor
+ $$
+ \trans
+ {P_2}{[s:c~t:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[t^R~c~s:\Nil]}{\emptystore}.
+ $$
+
+ Ook hiervoor kunnen we \emph{CleanSmurf} gebruiken. Geven
+ we~\eqref{eq:p2:ih} mee als aanname, dan krijgen we de boom
+ in~\autoref{fig:tree:bootstrap-step}. Net zoals bij de inductiebasis moeten
+ we $c$ als letterlijk \lit{c} meegeven. Eenzelfde inspectie van de
+ boom wijst uit dat dit geen problemen oplevert met andere waarden voor $c$.
+
+ \medskip
+ Uit het principe van inductie naar de structuur van de string $t$ volgt nu
+ voor alle $s,t\in\String$ met $t\ne\lambda$ dat we een afleidingsboom
+ hebben voor
+
+ $$
+ \trans
+ {P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[t^R~s:\Nil]}{\emptystore}.
+ $$
+ \end{proof}
+\end{thm}
+
+\begin{thm}
+ {
+ Voor alle $s\in\String$ hebben we een afleidingsboom voor
+ \normalfont
+ \belowdisplayskip=-1em
+ $$
+ \trans
+ {P_1}{[s:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[s^R:\Nil]}{\emptystore}.
+ $$
+ }
+ \label{thm:p1}
+ \begin{proof}[Bewijs]
+ We maken een gevalsonderscheiding over de structuur van $s$.
+
+ \begin{enumerate}[label={Geval \arabic*.},itemindent=1.5\parindent]
+ \item Stel $s=\lambda$. In dit geval hebben we geen enkele variabele. We
+ kunnen dus simpelweg een boom maken. Dit geeft de boom in
+ \autoref{fig:tree:lambda}, waaruit blijkt dat de stelling inderdaad
+ geldt voor $s=\lambda$:
+ $$
+ \trans
+ {P_1}{[\lambda:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{[\lambda:\Nil]}{\emptystore}.
+ $$
+
+ \item Stel $s=c~t$. In dit geval gaat $P_1$ het recursieve binnenste
+ programma gebruiken. We maken dus een boom die het resultaat van
+ \autoref{thm:p2} als aanname mag gebruiken. Dit geeft de afleidingsboom
+ in \autoref{fig:tree:bootstrap}, waaruit blijkt dat de bovenstaande
+ stelling geldt voor alle $s\ne\lambda$.
+ \end{enumerate}
+ \end{proof}
+\end{thm}