Bewijs

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}