Outer program explanation and small fix

3 files changed, 62 insertions, 56 deletions

diff --git a/analyse.tex b/analyse.tex
index edad8e0..0021771 100644
--- a/analyse.tex
+++ b/analyse.tex
@@ -11,6 +11,7 @@ van inductie naar de lengte van de input string. We hadden hiervoor initieel een
 \begin{smurf}
 \footnotesize
 i "input" p
+"input" g
 "input" g q
 "\textbackslash{}"\textbackslash{}"\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gh\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"g+\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gt 
 
@@ -23,7 +24,7 @@ i "input" p
 +
 "input" g p
 "\textbackslash{}"\textbackslash{}"o" "" p
-"input" g g x
+g x
 \end{smurf}
 
 Het bovenstaande programma is in het format van smurf maar echter is dit programma niet zo leesbaar. 
@@ -50,55 +51,5 @@ $$\lambda^R=\lambda$$
 
 	Basisgeval: $s=\lambda$.
 
-	$$%Todo fix dit
-	\begin{prooftree}
-		\[
-			\[
-				\[
-					\[
-						\vdots %todo afmaken
-						\justifies
-						\trans
-							{\StmPut : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
-							{\Nil}{\lambda}{\st}
-						\using{\rputns}
-					\]
-					\justifies
-					\trans
-						{\StmPush~\lambda : \StmPut : ...~}{\Nil}{(["+":\Nil], \emptystore)}
-						{\Nil}{\lambda}{\st}
-					\using{\rpushns}
-				\]
-				\justifies
-				\trans
-					{\StmCat : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
-					{\Nil}{\lambda}{\st}
-				\using{\rcatns}
-			\]
-			\justifies
-			\trans
-				{\StmInput : \StmCat : ...~}{[\lambda:\Nil]}{(["+":\Nil], \emptystore)}
-				{\Nil}{\lambda}{\st}
-			\using{\rinputns}
-		\]
-		\justifies
-		\trans
-			{\StmPush~"+" : \StmInput : ...~}{[\lambda:\Nil]}{(\Nil,\emptystore)}
-			{\Nil}{\lambda}{\st}
-		\using{\rpushns}
-	\end{prooftree}
-	$$
-
-	%FIXME
-	NB: dit bewijs is overduidelijk niet af. We gaan de afleidingsboom
-	automatisch genereren, dit is nog maar een begin. Het programma, dat van de
-	Esolang wiki afkomstig is~\cite{esolang:prog}, werkt helaas niet voor strings
-	met minder dan twee karakters. In het geval van de lege string wordt geen
-	output gegeven; in het geval van een string van één karakter crasht het
-	programma. We zullen ofwel dit programma aanpassen, zodat het wel werkt,
-	ofwel een ander programma bekijken. In het laatste geval zullen we nog steeds
-	een programma nemen waar we iets inductief over kunnen bewijzen, zoals het
-	laatste voorbeeld uit \autoref{sec:intro:exmp}.
-
-	%todo afmaken
+	
 \end{proof}
diff --git a/explanation.tex b/explanation.tex
index 05f8ea4..d76108d 100644
--- a/explanation.tex
+++ b/explanation.tex
@@ -1,3 +1,58 @@
 % vim: set spelllang=nl:
-\subsection{uitleg programma}
-\label{sec:uitleg programma}
\ No newline at end of file
+\subsection{Het omdraaiprogramma uitgelegd}
+\label{sec:uitleg programma}
+
+Om uit te leggen hoe dit programma precies functioneert zullen we een programma bekijken dat identiek is aan het programma dat we analyseren, op de namen van de gebruikte variabelen na. (In de analyse zijn de namen kleiner gemaakt, zodat de bewijsbomen minder breed zouden worden)
+"program" correspondeert met "u",
+"grow" met "v" en 
+"shrink" met "w".
+Ook zullen we het programma opdelen in twee aparte programma's die elk apart bekeken kan worden zodat het geheel beter te begrijpen is.
+\medskip
+
+\subsubsection{Het buitenste programma}
+Het buitenste programma test of we te maken hebben met de lege string als inputstring. Als dit het geval is geef je de lege string als output. Anders ga je het recursieve subprogramma in, dat alleen voor strings van lengte n + 1 gedefiniëerd is.
+Omdat Smurf geen statement heeft om waarden te testen moeten we hier op een slimme manier omgaan met het feit dat waarden ook als variabelenaam kunnen worden gebruikt. Eerst schrijven we het recursieve programma dat we moeten aanroepen als de inputstring niet leeg is naar de variabele met als naam de inputstring zelf. Hierna schrijven we het programma dat moet worden uitgevoerd als de string leeg is (het outputten van de lege string) naar de variabele met als naam de lege string. Als de inputstring leeg is overschrijven we daar dus het recursieve programma dat we eerst aan die variabele hadden toegewezen. Als laatste voeren we het programma uit dat op de variabele met naam de inputstring staat.
+
+Dit buitenste programma ziet er als volgt uit:
+\begin{center}
+\makebox{
+\makebox{
+\parbox{28mm}{
+\begin{smurf}
+\footnotesize
+i "input" p\\
+"input" g\\
+"input" g q\\
+\emph{subprogramma-string}\\
++\\
+"input" g p\\
+"\textbackslash{}"\textbackslash{}"o" "" p\\
+g x
+\end{smurf}
+}}
+
+\parbox{8mm}{
+\begin{smurf}
+\footnotesize
+(1)\\
+(2)\\
+(3)\\
+.\\
+.\\
+(4)\\
+(5)\\
+(6)
+\end{smurf}
+}}
+\end{center}
+
+\textbf{(1)} Allereerst wordt de inputstring op de stack gezet en naar de variabele met naam "input" geschreven. De stack is nu weer leeg. \textbf{(2)} Nu zetten we de inputwaarde weer op de stack voor later gebruik. De reden hiervoor volgt straks.
+\textbf{(3)} Hierna halen we deze inputwaarde voor de tweede keer op, quotifyen we hem en prependen we het tot de subprogramma-string. Dit kun je zien als het doorgeven van een argument. De reden dat we de input quotifyen is dat dit ervoor zorgt dat alle karakters in de input behouden blijven (ook die met speciale betekenis zoals "\textbackslash{}") wanneer het subprogramma wordt uitgevoerd. Het subprogramma staat zelf al gequotifyed hier.
+Op dit moment staat het grote programma met de input eraan geprepend op de stack, met als element eronder de inputwaarde die we zo nodig hebben. \textbf{(4)} Nu halen we opnieuw de waarde van de input op uit de variabele waarnaar we het eerst hadden weggeschreven en gebruiken we dit als een variabelenaam om het subprogramma naar weg te schrijven. Merk op dat we onze opslag van de inputstring verliezen als die toevallig de waarde "input" had, omdat we die variabele dan overschrijven. Dit is waarom we deze waarde van tevoren een keer extra op de stack hebben gezet. Zo kunnen we hem bij (6) nog gebruiken. \textbf{(5)} Nu zetten we het gequotifyde programma "output de lege string" op het register met naam de lege string. Ongequotifyed ziet het er zo uit: \texttt{""o}
+\textbf{(6)} Als laatste halen we het programma op van de variabele met als naam de inputstring die we in (2) op de stack hadden gezet en voeren we dit programma uit.
+
+\subsubsection{Het recursieve binnenste programma}
+
+
+
+
diff --git a/reverse2.tex b/reverse2.tex
index 5f08a4f..9b888df 100644
--- a/reverse2.tex
+++ b/reverse2.tex
@@ -1,6 +1,6 @@
 \begin{smurf}
 \footnotesize
-\StmInput~: \StmPush~"input"~: \StmPut~:
+\StmInput~: \StmPush~"input"~: \StmPut~: \StmPush~"input"~: \StmGet~:
 \StmPush~"input"~: \StmGet~: \StmQuotify~:\\ \StmPush~
 "\textbackslash{}"\textbackslash{}"\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gh\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"g+\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gt
 
@@ -12,6 +12,6 @@
 \\
 \StmCat~: \StmPush~"input" \StmGet~: \StmPut
 : \StmPush~"\textbackslash{}"\textbackslash{}"o"~: \StmPush~""~: \StmPut~:
-\StmPush~"input"~: \StmGet~: \StmGet~: \StmExec~: $\lambda$
+\StmGet~: \StmExec~: $\lambda$
 
 \end{smurf}
\ No newline at end of file