Enumerate; kleine aanpassingen aan het Nederlands

3 files changed, 175 insertions, 151 deletions

diff --git a/explanation-inner.tex b/explanation-inner.tex
index 54398df..503cae6 100644
--- a/explanation-inner.tex
+++ b/explanation-inner.tex
@@ -1,29 +1,31 @@
 % vim: set spelllang=nl:
 \subsubsection{Het recursieve binnenste programma}
-Het binnenste programma draait strings van lengte n + 1 om. Hiervoor krijgt het
-twee "argumenten" geprepend mee. Het eerste argument is een string in zijn
+Het binnenste programma draait strings van lengte $n\ge1$ om. Hiervoor krijgt het
+twee ``argumenten'' mee als $\StmPush$-commando's. Het eerste argument is een string in zijn
 oorspronkelijke volgorde, die elke recursieve aanroep \'{e}\'{e}n karakter
-kleiner wordt. Het tweede argument is een string die initi\"{e}el de lege
+kleiner wordt. Het tweede argument is een string die initieel de lege
 string is, maar bij elke recursieve aanroep \'{e}\'{e}n karakter groter wordt
-en de omgekeerde string voorstelt. De reden dat dit programma alleen voor
-strings van lengte n + 1 werkt is als volgt: het testen van waarden kost zoals
-we eerder hadden gezien een programma-aanroep. Wij hebben ervoor gekozen om
-eerst de string te verkleinen en daarna te kijken of we de lege string hebben
-bereikt (de hele string is omgedraaid) om te bepalen of we dit programma nog
-eens moeten uitvoeren met nieuwe argumenten. Als je zou willen bepalen of je
-inputstring leeg was voordat je deze verkleint zou je 2 recursieve programma's
-nodig hebben die elkaar telkens aanroepen: \'{e}\'{e}n die als eerste test of
-de input leeg en daarop gebaseerd \'{o}f het andere programma aanroept \'{o}f
-output geeft en eindigt en een ander programma dat de string verkleint en dan
-het eerste programma aanroept om weer de waarde te testen. Het leek ons dus
-beter om aan het einde te testen of we door moeten gaan en het geval van de
-lege string op te vangen in het buitenste programma.
+en de omgekeerde string voorstelt.
+
+De reden dat dit programma niet voor de lege string werkt is de volgende: het
+testen van waarden kost zoals we eerder hebben gezien een programma-aanroep. We
+hebben ervoor gekozen om eerst de string te verkleinen en daarna te kijken of
+we de lege string hebben bereikt (de hele string is omgedraaid) om te bepalen
+of we dit programma nog eens moeten uitvoeren met nieuwe argumenten. Als je zou
+willen bepalen of je inputstring leeg was voordat je deze verkleint zou je twee
+recursieve programma's nodig hebben die elkaar telkens aanroepen: \'{e}\'{e}n
+die als eerste test of de input leeg en op basis daarvan \'{o}f het andere
+programma aanroept \'{o}f output geeft en eindigt, en een ander programma dat
+de string verkleint en dan het eerste programma aanroept om weer de waarde te
+testen. Dit is echter onnodig complex. Het leek ons beter om aan het einde te
+testen of we door moeten gaan en het geval van de lege string op te vangen in
+het buitenste programma.
 
 Het recursieve omdraaiprogramma ziet er zo uit:
 
 \begin{center}
 \makebox{
-\parbox{48mm}{
+\parbox{60mm}{
 \begin{smurf}
 \footnotesize
 \emph{x-string} \emph{y-string}\\
@@ -63,85 +65,88 @@ g x
 \footnotesize
 (1)\\
 (2)\\
-.\\
-.\\
-.\\
-.\\
-.\\
-.\\
+~\\
+~\\
+~\\
+~\\
+~\\
+~\\
 (3)\\
-.\\
-.\\
-.\\
+~\\
+~\\
+~\\
 (4)\\
-.\\
+~\\
 (5)\\
-.\\
+~\\
 (6)\\
-.\\
+~\\
 (7)\\
-.\\
+~\\
 (8)\\
-.\\
-.\\
-.\\
+~\\
+~\\
+~\\
 (9)\\
-.\\
+~\\
 (10)\\
-.\\
+~\\
 (11)
 \end{smurf}
 }}
 \end{center}
 
-\begin{description}
-\item \textbf{(1)} De argumenten worden er de eerste keer opgezet door het buitenste
-programma. Merk op dat het y-argument in het buitenste programma
-\texttt{"\textbackslash"\textbackslash""} is, wat de gequotifyde versie is van
-\texttt{""}, oftewel de lege string. Het x-argument is dan de niet-lege input.
-\item \textbf{(2)} Hierna wordt de een string van de rest van het programma (vanaf
-(3)) op de stack gezet. Dit zorgt ervoor dat recursie mogelijk is.
-\item \textbf{(3)} Het programma en de argumenten worden in variabelen opgeslagen.
-"program" voor het programma, "grow" voor het rechterargument, "shrink" voor
-het linkerargument.
-\item \textbf{(4)} De waarde van "shrink" wordt opgehaald en
-vervangen door zijn eerste karakter. Daarna wordt "grow" opgehaald en het
-eerste karakter van "shrink" wordt eraan geappend. Het resultaat hiervan wordt
-weggeschreven naar "grow".
-\item \textbf{(5)} Nu wordt de waarde van "shrink" nog
-eens opgehaald, vervangen door zijn tail en weer teruggeschreven naar "shrink".
-Nu is het eerste karakter van shrink dus naar achter "grow" verplaatst.
-\item \textbf{(6)} De nieuwe waarde van "shrink" wordt nu al vast op de stack gezet,
-voor dezelfde reden dat dit in het buitenste programma met "input" gebeurde.
-Wanneer we hem later nodig hebben hebben we niet de garantie dat de
-variabelenaam niet overschreven is, dus we zetten hem er nu al op.
-\item \textbf{(7)} De nieuwe waarde van "grow" wordt opgehaald en gequotifyed. Ook
-appenden we "o" eraan. Zo vormt het een programmastring die die waarde zou
-outputten wanneer uitgevoerd. Dit moeten we doen als "shrink" leeg is geworden.
-Merk op dat het programma dat moet worden uitgevoerd wanneer de string leeg is
-geworden in tegenstelling tot in het buitenste programma hier v\'{o}\'{o}r het
-andere programma wordt aangemaakt. Dit doen we omdat we hier een waarde van een
-variabele gebruiken en we niet weten of de variabele straks overschreven wordt.
-We bouwen deze programmastring dus al vast, maar laten hem nog gewoon op de
-stack staan.
-\item \textbf{(8)} "shrink" en "grow" worden opgehaald en gequotifyed.
-Ook "program" wordt opgehaald en gequotifyed. Dit alles appenden we aan elkaar.
-Nu wordt "program" nog eens opgehaald, niet gequotifyed en aan de eerdere sting
-geappend. Nu is deze hele string gelijk aan het hele programma, maar met de
-nieuwe waarden van "grow" en "shrink" als argumenten.
-\item \textbf{(9)} Nu komt het
-deel waar we de waarde van shrink testen om te kiezen of we output moeten
-geven, of nog een recursiestap moeten uitvoeren. De waarde van "shrink" wordt
-opgehaald en gebruikt als variabelenaam om het programma dat we in (8) hadden
-gebouwd naar weg te schrijven. Vanaf dit punt kunnen we geen van onze
-variabelen meer gebruiken, omdat de waarde van "shrink" toevallig gelijk zou
-kunnen zijn geweest aan de naam van een van onze variabelen
-\item \textbf{(10)} Nu
-schrijven we het programma dat we in (7) hadden gebouwd en nog op de stack
-stond weg naar de variabele met naam de lege string.
-\item \textbf{(11)} Nu halen we
-de waarde op van de variabele met als naam de waarde van "shrink" die we in (6)
-al op de stack hadden gezet. Als "shrink" leeg was vinden we het programma uit
-(7). Anders vinden we het programma uit (8). We voeren het gevonden programma
-uit.
-\end{description}
\ No newline at end of file
+De programmaonderdelen worden hieronder toegelicht.
+
+\begin{enumerate}
+	\item De argumenten worden er de eerste keer opgezet door het buitenste
+		programma. Merk op dat het y-argument in het buitenste programma
+		\smurfinline{"\textbackslash"\textbackslash""} is, wat de gequotifyde
+		versie is van de lege string. Het x-argument is dan de niet-lege input.
+	\item Hierna wordt de string van de rest van het programma (vanaf (3)) op de
+		stack gezet. Dit zorgt ervoor dat recursie mogelijk is.
+	\item Het programma en de argumenten worden in variabelen opgeslagen:
+		\smurfinline{program} voor het programma, \smurfinline{grow} voor het
+		rechterargument en \smurfinline{shrink} voor het linkerargument.
+	\item De waarde van \smurfinline{shrink} wordt opgehaald en vervangen door
+		zijn eerste karakter. Daarna wordt \smurfinline{grow} opgehaald en het
+		eerste karakter van \smurfinline{shrink} wordt eraan toegevoegd. Het
+		resultaat hiervan wordt weggeschreven naar \smurfinline{grow}.
+	\item Hier wordt \smurfinline{shrink} vervangen door alles behalve zijn
+		eerste karakter. Het eerste karakter van \smurfinline{shrink} is dus
+		verplaatst naar het einde van \smurfinline{grow}.
+	\item De nieuwe waarde van \smurfinline{shrink} wordt nu alvast op de stack
+		gezet, voor dezelfde reden dat dit in het buitenste programma met
+		\smurfinline{input} gebeurde.  Wanneer we hem later nodig hebben hebben we
+		niet de garantie dat de variabelenaam niet overschreven is, dus we zetten
+		hem er nu al op.
+	\item De nieuwe waarde van \smurfinline{grow} wordt opgehaald en gequotifyed.
+		Ook voegen we \smurfinline{o} er aan toe. Zo vormt het een programmastring
+		die die waarde zou outputten wanneer uitgevoerd. Dit moeten we doen als
+		\smurfinline{shrink} leeg is geworden. Merk op dat het programma dat moet
+		worden uitgevoerd wanneer de string leeg is geworden in tegenstelling tot
+		in het buitenste programma hier v\'{o}\'{o}r het andere programma wordt
+		aangemaakt. Dit doen we omdat we hier een waarde van een variabele
+		gebruiken en we niet weten of de variabele straks overschreven wordt.  We
+		bouwen deze programmastring dus alvast, maar laten hem nog gewoon op de
+		stack staan.
+	\item \smurfinline{shrink} en \smurfinline{grow} worden opgehaald en
+		gequotifyed. Ook \smurfinline{program} wordt opgehaald en gequotifyed. Dit
+		alles concateneren we. De variabele \smurfinline{program} wordt nog eens
+		opgehaald, niet gequotifyed en aan de eerdere string toegevoegd. Nu is deze
+		hele string gelijk aan het hele programma, maar met de nieuwe waarden van
+		\smurfinline{grow} en \smurfinline{shrink} als argumenten.
+	\item Nu komt het deel waar we de waarde van \smurfinline{shrink} testen om
+		te kiezen of we output moeten geven, of nog een recursiestap moeten
+		uitvoeren. De waarde van \smurfinline{shrink} wordt opgehaald en gebruikt
+		als variabelenaam om het programma dat we in (8) hadden gebouwd naar weg te
+		schrijven. Vanaf dit punt kunnen we geen van onze variabelen meer
+		gebruiken, omdat de waarde van \smurfinline{shrink} toevallig gelijk zou
+		kunnen zijn geweest aan de naam van een van onze variabelen
+	\item Nu schrijven we het programma dat we in (7) hadden gebouwd en nog op de
+		stack stond weg naar de variabele $lambda$.
+	\item We halen de waarde op van de variabele met als naam de waarde van
+		\smurfinline{shrink} die we in (6) al op de stack hadden gezet. Als
+		\smurfinline{shrink} leeg was vinden we het programma uit (7). Anders
+		vinden we het programma uit (8). We voeren het gevonden programma uit.
+\end{enumerate}
diff --git a/explanation-outer.tex b/explanation-outer.tex
index 25001e1..763a046 100644
--- a/explanation-outer.tex
+++ b/explanation-outer.tex
@@ -3,7 +3,7 @@
 Het buitenste programma controleert of we te maken hebben met de lege string
 als inputstring. Als dit het geval is geeft het de lege string als output.
 Anders wordt het recursieve subprogramma gebruikt, dat alleen voor strings van
-lengtes groter dan nul gedefini\"{e}erd is.
+lengtes groter dan nul gedefinieerd is.
 
 Omdat Smurf geen conditionals kent, moeten we hier op een slimme manier omgaan
 met het feit dat waarden ook als variabelenaam kunnen worden gebruikt. Dit is
@@ -19,7 +19,7 @@ variabele met naam de inputstring staat.
 Het buitenste programma ziet er als volgt uit:
 \begin{center}
 \makebox{
-\parbox{35mm}{
+\parbox{45mm}{
 \begin{smurf}
 \footnotesize
 i "input" p\\
@@ -39,8 +39,8 @@ g x
 (1)\\
 (2)\\
 (3)\\
-.\\
-.\\
+~\\
+~\\
 (4)\\
 (5)\\
 (6)
@@ -48,32 +48,30 @@ g x
 }}
 \end{center}
 
-\begin{description}
-\item \textbf{(1)} Allereerst wordt de inputstring op de stack gezet en naar de
-variabele met naam "input" geschreven. De stack is nu weer leeg.
-\item \textbf{(2)}
-Nu zetten we de inputwaarde weer op de stack voor later gebruik. De reden
-hiervoor volgt straks.
-\item \textbf{(3)} Hierna halen we deze inputwaarde voor de
-tweede keer op, quotifyen we hem en voegen we het toe aan het begin van 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 voorgevoegd op de stack, met als element eronder de inputwaarde die
-we zo nodig hebben.
-\item \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.
-\item \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}
-\item \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.
-\end{description}
\ No newline at end of file
+\begin{enumerate}
+	\item Allereerst wordt de inputstring op de stack gezet en naar de variabele
+		met naam \smurfinline{input} geschreven. De stack is nu weer leeg.
+	\item We zetten de inputwaarde weer op de stack voor later gebruik. Waarom
+		dit nodig is wordt uitgelegd in punt 4.
+	\item Hierna halen we deze inputwaarde voor de tweede keer op, quotifyen we
+		hem en voegen we het toe aan het begin van de subprogramma-string. Dit is
+		vergelijkbaar met het doorgeven van een functieargument. 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
+		\lit{\textbackslash{}}) wanneer het subprogramma wordt uitgevoerd. Het
+		subprogramma staat zelf al gequotifyed hier. Op dit moment staat het grote
+		programma met de input eraan voorgevoegd op de stack, met als element
+		eronder de inputwaarde die we zo nodig hebben.
+	\item 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 \smurfinline{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.
+	\item Nu zetten we het gequotifyde programma "output de lege string" in de
+		variabele $\lambda$. Ongequotifyed ziet het uit als \smurfinline{""o}.
+	\item 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.
+\end{enumerate}
diff --git a/sosexamp.tex b/sosexamp.tex
index 45c8a2e..32e4f2c 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -1,24 +1,36 @@
 % vim:set spelllang=nl:
 \section{Smurf in structurele operationele semantiek}
 \label{sec:sos}
-We willen ook laten zien hoe de definities van Smurf eruit zien als
-je de structurele operationele semantiek gebruikt. In principe maakt het voor
-de analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of
-structurele operationele semantiek. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we
-hier meer bekend mee zijn. Echter willen we ook nog graag laten zien hoe het
-eruit zou zien als je structurele operationele semantiek zou gebruiken.
+We willen ook laten zien hoe de definities van Smurf eruit zien als je de
+structurele operationele semantiek gebruikt. In principe maakt het voor de
+analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of structurele
+operationele semantiek. Wij hadden een voorkeur om natuurlijke semantiek te
+gebruiken omdat we hier meer bekend mee zijn. Echter willen we ook nog graag
+laten zien hoe het 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 $\Gamma$ beschouwen. Waarbij $\Gamma$ óf  $\Pgm\times\Input\times\Output\times\State$ óf $\Input\times\Output\times\State$ is. 
-Dit schrijven we als
-$$\sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma}	\qquad \text{met\enspace
-	\parbox{36mm}{ $\gamma = (\pgm',\ip',\op',\st')$ of \\  $\gamma = (\ip', \op',\st' )$}}$$
+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 $\Gamma$ beschouwen, waarbij
+$\Gamma$ óf  $\Pgm\times\Input\times\Output\times\State$ óf
+$\Input\times\Output\times\State$ is. Dit schrijven we als
 
-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
+$$\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 $\StmExec$-regel het programma
+dat je gaat uitvoeren verandert. In de meeste gevallen zal $\pgm$ = $\pgm'$
+gelden maar dat hoeft dus niet.
 
- 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. 
+\medskip
+Het is mogelijk om in de structurele operationele semantiek, zoals bij de
+natuurlijke semantiek, compositie in te bouwen in iedere regel en een
+$\lambda$-regel toe te voegen. In dit geval kiezen we er echter voor om gebruik
+te maken van een aparte regel voor compositie. We blijven hiermee in zekere zin
+dichter bij de specificatie, omdat we regels per commando kunnen beschrijven in
+plaats van voor een heel programma.
 
 De compositieregel is dan als volgt:
 
@@ -32,29 +44,18 @@ $$
 		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
 		{\pgm}{\ip'}{\op'}{(\stk',\str')}
 	\using{\rcompeensos}
-	\qquad
 \end{prooftree}
 $$
 
 \bigskip
+We geven twee voorbeelden van regels in de structurele operationele semantiek.
+Het doel is hier niet om een precieze beschrijving van de semantiek te geven
+zoals we dat in \autoref{sec:rules} voor natuurlijke semantiek hebben gedaan,
+maar enkel om aan te geven dat de twee in het geval van Smurf erg op elkaar
+lijken.
 
-De regel voor $\StmExec$ zou in de structurele operationele semantiek als volgt zijn: 
-$$
-\begin{prooftree}
-\axjustifies
-	\sostrans
-		{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
-	\using{\rexecsos}
-	\qquad
-		\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
-\end{prooftree}
-$$
-
-\bigskip
 De regel voor $\StmTail$ zou in de structurele operationele semantiek als volgt
 zijn:
-
 $$
 \begin{prooftree}
 	\axjustifies
@@ -67,4 +68,24 @@ $$
 \end{prooftree}
 $$
 
-De andere regels zoals head en exec zullen we hier niet verder uitwerken omdat deze op een soortgelijke wijzen worden gemaakt. 
\ No newline at end of file
+Afgezien van de compositie, die bij de natuurlijke semantiek in iedere regel is
+ingebouwd, verschilt dit niet erg van $\rtailns$ in \autoref{sec:rules:tail}.
+
+Dit geldt voor bijna alle andere commando's net zo. Een apart geval is
+$\StmExec$, omdat we hier de compositieregel niet kunnen gebruiken. Wat na het
+$\StmExec$-commando volgt wordt immers niet uitgevoerd. We definiëren deze
+regels als volgt:
+$$
+\begin{prooftree}
+\axjustifies
+	\sostrans
+		{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
+		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+	\using{\rexecsos}
+	\qquad
+		\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
+\end{prooftree}
+$$
+Hier wordt gebruik gemaakt van een ander soort transitie, waarbij een programma
+aan de rechterkant voorkomt. Hierdoor is $\rexecsos$ niet te gebruiken als
+premisse voor $\rcompeensos$, wat precies is wat we wilden.