% vim: set spelllang=nl:
\section{Analyse}
\label{sec:analyse}

Als analyse willen we graag een stuk code dat een string omdraait bekijken aan
de hand van onze semantiekregels. Deze code ziet er als volgt uit:

\begin{smurf}
	\footnotesize
	"+"i+ ""p ""gtg ""gt "i"p\\
	"\textbackslash{}"\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gh\textbackslash{}"o\textbackslash{}"g+\textbackslash{}"o\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gt\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"tg\textbackslash{}"+\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\\
    \textbackslash{}"i\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"o\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"\textbackslash{}"gq+\textbackslash{}"\textbackslash{}"g+\textbackslash{}"\textbackslash{}"p\textbackslash{}"o\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"+\textbackslash{}"pgx"\\
	""p "\textbackslash{}"+\textbackslash{}"\textbackslash{}"\textbackslash{}"p" "i"gq+ "tg"+ "i"gq+\\
	"\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""+ ""gq+ ""g+ ""p "" "+" "i"g+ pgx
\end{smurf}

Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo
uit:

%todo leesbaarheid betekent ook witregels waar logisch
\begin{smurf}
	\footnotesize
	
	\StmPush~"+"~: 
	\StmInput~: 
	\StmCat~: 
	\StmPush~$\lambda$~: 
	\StmPut~: 
	\StmPush~$\lambda$~: 
	\StmGet~: 
	\StmTail~:\\
	\StmGet~: 
	\StmPush~$\lambda$~: 
	\StmGet~: 
	\StmTail~: 
	\StmPush~"i"~: 
	\StmPut~:\\
	\StmPush~"\textbackslash{}"\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gh\textbackslash{}"o\textbackslash{}"g+\textbackslash{}"o\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gt\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"tg\textbackslash{}"+\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\\
    \textbackslash{}"i\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"o\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"\textbackslash{}"gq+\textbackslash{}"\textbackslash{}"g+\textbackslash{}"\textbackslash{}"p\textbackslash{}"o\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"+\textbackslash{}"pgx"~:\\
	\StmPush~$\lambda$~: 
	\StmPut~: 
	\StmPush~"\textbackslash{}"+\textbackslash{}"\textbackslash{}"\textbackslash{}"p"~:\\
	\StmPush~"i"~: 
	\StmGet~: 
	\StmQuotify~: 
	\StmCat~: 
	\StmPush~"tg"~: 
	\StmCat~: 
	\StmPush~"i"~: 
	\StmGet~: 
	\StmQuotify~: 
	\StmCat~: 
	\StmPush~"\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""~: 
	\StmCat~: 
	\StmPush~$\lambda$~: 
	\StmGet~: 
	\StmQuotify~: 
	\StmCat~: 
	\StmPush~$\lambda$~: 
	\StmGet~: 
	\StmCat~: 
	\StmPush~$\lambda$~: 
	\StmPut~: 
	\StmPush~$\lambda$~: 
	\StmPush~"+"~: 
	\StmPush~"i"~: 
	\StmGet~: 
	\StmCat~: 
	\StmPut~: 
	\StmGet~: 
	\StmExec~: 
    $\lambda$

    
\end{smurf}

Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait,
oftewel: er is een afleidingsboom voor
$$
\trans
	{Programma}{[s:\Nil]}{(\Nil,\emptystore)}
	{\Nil}{s^R}{\st}
$$
voor alle s, waar
$$(c~s)^R=s^R c$$
$$\lambda^R=\lambda$$

\begin{proof}[Bewijs]
	Met inductie naar de lengte van $s$.

	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}
	$$

	%todo afmaken
\end{proof}