diff options
| -rw-r--r-- | analyse.tex | 89 | ||||
| -rw-r--r-- | app-trees.tex | 5 | ||||
| -rw-r--r-- | explanation.tex | 3 | ||||
| -rw-r--r-- | reverse2.tex | 17 | ||||
| -rw-r--r-- | smurf.sty | 1 | ||||
| -rw-r--r-- | smurfreverser.txt | 4 | ||||
| -rw-r--r-- | sosexamp.tex | 14 |
7 files changed, 54 insertions, 79 deletions
diff --git a/analyse.tex b/analyse.tex index 4d4a48d..edad8e0 100644 --- a/analyse.tex +++ b/analyse.tex @@ -6,79 +6,34 @@ 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}: - +te leveren over een programma met een willekeurige input string, door gebruik te maken +van inductie naar de lengte van de input string. We hadden hiervoor initieel een programma op het internet \cite{esolang:prog} gevonden welke een string zou moeten omdraaien. Echter werkte dit programma niet naar behoren. Het werkte namelijk niet voor strings met lengte een. Daarom hebben we zelf een programma geschreven voor het omdraaien van een string. Dit programma 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} +\footnotesize +i "input" p +"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 -Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo -uit: +\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"g\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"gq++\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"g+ -%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$ +\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gp\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"pgx\textbackslash{}"\textbackslash{}"u\textbackslash{}"p\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gh\textbackslash{}"v\textbackslash{}"g+\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gt\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"g\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+ - +\textbackslash{}"w\textbackslash{}"gq\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"u\textbackslash{}"gq++\textbackslash{}"u\textbackslash{}"g+\textbackslash{}"w\textbackslash{}"gp\textbackslash{}"\textbackslash{}"pgx" +\\ ++ +"input" g p +"\textbackslash{}"\textbackslash{}"o" "" p +"input" g g x \end{smurf} +Het bovenstaande programma is in het format van smurf maar echter is dit programma niet zo leesbaar. +Daarom hebben we getracht het programma iets leesbaardere te maken: + +\input{reverse2} + +\input{explanation} + +\subsection{bewijs} Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait, oftewel: er is een afleidingsboom voor $$ diff --git a/app-trees.tex b/app-trees.tex index c91c8ef..52509d0 100644 --- a/app-trees.tex +++ b/app-trees.tex @@ -7,6 +7,7 @@ \begin{prooftree} \input{tree-gen-leeg} \end{prooftree} - $$ - } + $$} + + \end{landscape} diff --git a/explanation.tex b/explanation.tex new file mode 100644 index 0000000..05f8ea4 --- /dev/null +++ b/explanation.tex @@ -0,0 +1,3 @@ +% vim: set spelllang=nl: +\subsection{uitleg programma} +\label{sec:uitleg programma}
\ No newline at end of file diff --git a/reverse2.tex b/reverse2.tex new file mode 100644 index 0000000..5f08a4f --- /dev/null +++ b/reverse2.tex @@ -0,0 +1,17 @@ +\begin{smurf} +\footnotesize +\StmInput~: \StmPush~"input"~: \StmPut~: +\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 + +\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"g\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"gq++\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"g+ + +\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gp\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"pgx\textbackslash{}"\textbackslash{}"u\textbackslash{}"p\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gh\textbackslash{}"v\textbackslash{}"g+\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gt\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"g\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+ + +\textbackslash{}"w\textbackslash{}"gq\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"u\textbackslash{}"gq++\textbackslash{}"u\textbackslash{}"g+\textbackslash{}"w\textbackslash{}"gp\textbackslash{}"\textbackslash{}"pgx"~: +\\ +\StmCat~: \StmPush~"input" \StmGet~: \StmPut +: \StmPush~"\textbackslash{}"\textbackslash{}"o"~: \StmPush~""~: \StmPut~: +\StmPush~"input"~: \StmGet~: \StmGet~: \StmExec~: $\lambda$ + +\end{smurf}
\ No newline at end of file @@ -60,6 +60,7 @@ \def\sostrans#1#2#3#4#5#6#7#8{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7,#8\right)} \def\sostranseind#1#2#3#4#5#6#7{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7\right)} +\def\sostransgamma#1#2#3#4#5{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow#5} % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} diff --git a/smurfreverser.txt b/smurfreverser.txt index f08b69e..d217460 100644 --- a/smurfreverser.txt +++ b/smurfreverser.txt @@ -3,8 +3,8 @@ i "input" p "input" g q " -\"\"\"\\\"program\\\"p\\\"grow\\\"p\\\"shrink\\\"p\\\"shrink\\\"gh\\\"grow\\\"g+\\\"grow\\\"p\\\"shrink\\\"gt\\\"shrink\\\"p\\\"shrink\\\"g\\\"grow\\\"gq\\\"o\\\"+\\\"shrink\\\"gq\\\"grow\\\"gq\\\"program\\\"gq++\\\"program\\\"g+\\\"shrink\\\"gp\\\"\\\"pgx\"\"program\"p\"grow\"p\"shrink\"p\"shrink\"gh\"grow\"g+\"grow\"p\"shrink\"gt\"shrink\"p\"shrink\"g\"grow\"gq\"o\"+\"shrink\"gq\"grow\"gq\"program\"gq++\"program\"g+\"shrink\"gp\"\"pgx +\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\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"g\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"gq++\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"g+\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gp\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"pgx\textbackslash{}"\textbackslash{}"u\textbackslash{}"p\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gh\textbackslash{}"v\textbackslash{}"g+\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gt\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"g\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"w\textbackslash{}"gq\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"u\textbackslash{}"gq++\textbackslash{}"u\textbackslash{}"g+\textbackslash{}"w\textbackslash{}"gp\textbackslash{}"\textbackslash{}"pgx " + "input" g p -"\"Leeg\"o" "" p +"\textbackslash{}"\textbackslash{}"o" "" p "input" g g x
\ No newline at end of file diff --git a/sosexamp.tex b/sosexamp.tex index e3926e8..45c8a2e 100644 --- a/sosexamp.tex +++ b/sosexamp.tex @@ -10,15 +10,13 @@ eruit zou zien als je structurele operationele semantiek zou gebruiken. Bij het definiëren van de structurele operationele semantiek van Smurf zullen we de verzameling van transities als een relatie $\Rightarrow$ tussen -$\Pgm\times\Input\times\Output\times\State$ en $\Pgm\times\Input\times\Output\times\State$ beschouwen. +$\Pgm\times\Input\times\Output\times\State$ en $\Gamma$ beschouwen. Waarbij $\Gamma$ óf $\Pgm\times\Input\times\Output\times\State$ óf $\Input\times\Output\times\State$ is. Dit schrijven we als -$$\sostrans{\stm:\pgm}{\ip}{\op}{\st}{\pgm}{\ip'}{\op'}{\st'}$$ -en lezen we als -\begin{quote} - ``het programma $\stm:\pgm$ zal in toestand $\st$ gegeven input $\ip$ en output $\op$ leiden tot - toestand $\st'$, met output $\op'$ waarbij $\ip'$ gelijk is aan $\ip$ zonder - de geconsumeerde input.'' -\end{quote} +$$\sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma} \qquad \text{met\enspace + \parbox{36mm}{ $\gamma = (\pgm',\ip',\op',\st')$ of \\ $\gamma = (\ip', \op',\st' )$}}$$ + +De reden dat we hier spreken over $\pgm'$ is omdat de exec regel het programma dat je gaat uitvoeren verandert. In de meeste gevallen zal $\pgm$ = $\pgm'$ gelden maar dat hoeft dus niet. +\medskip Je kunt de structurele operationele semantiek zoals bij de natuurlijke semantiek definiëren aan de hand van de $\lambda$-regel maar om juist het verschil aan te geven met als je gebruik maakt van compositieregels, hebben wij ervoor gekozen om de structurele operationele semantiek te definiëren gebruik makende van compositieregels. |