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

Omdat de transities van onze natuurlijke semantiek input meenemen, kunnen we
alleen een afleidingsboom maken voor een programma \emph{met} een bepaalde
input. Het is dus niet triviaal mogelijk een afleidingsboom te maken voor willekeurige
input. In deze sectie willen we laten zien hoe het toch mogelijk is een bewijs
te leveren over een programma met een willekeurige input, door gebruik te maken
van inductie naar de lengte van de input. We doen dit aan de hand van een
programma dat een string omdraait~\cite{esolang:prog}:

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