From d76dbfdcae8e0885e8379da3e4db99f33dfc56cb Mon Sep 17 00:00:00 2001
From: Evi
Date: Fri, 10 Jun 2016 10:08:42 +0200
Subject: aanpassing sos + kleine fix ns trans

---
 sosexamp.tex | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

(limited to 'sosexamp.tex')

diff --git a/sosexamp.tex b/sosexamp.tex
index 641acb4..0fe065a 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -1,17 +1,26 @@
 % vim:set spelllang=nl:
 \section{Smurf in structurele operationele semantiek}
 \label{sec:sos}
-We willen ook nog graag laten zien hoe de definities van Smurf eruit zien als
+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. Omdat natuurlijke semantiek en structurele
-operationele semantiek equivalent zijn wanneer de regels goed gedefinieerd
-zijn. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we
+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 gebruiken hier in plaats van de $\lambda$-regel twee compositieregels om
-hiervan ook het verschil aan te geven.
+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.
+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}
+
+ 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. 
 
 De twee compositieregels zijn als volgt:
 
@@ -59,3 +68,5 @@ $$
 	\text{met $\pop{\stk} = (c~s,\stk')$.}
 \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
-- 
cgit v1.2.3


From cdb22510a8640a4a12a4e797dcb9d880226c3157 Mon Sep 17 00:00:00 2001
From: Evi
Date: Fri, 10 Jun 2016 10:26:53 +0200
Subject: exec ipv tweede compositie regel

---
 sosexamp.tex | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'sosexamp.tex')

diff --git a/sosexamp.tex b/sosexamp.tex
index 0fe065a..e3926e8 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -22,34 +22,34 @@ en lezen we als
 
  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. 
 
-De twee compositieregels zijn als volgt:
+De compositieregel is dan als volgt:
 
 $$
 \begin{prooftree}
-	\sostrans
+	\sostranseind
 		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\pgm'}{\ip'}{\op'}{(\stk', \str')}
+		{\ip'}{\op'}{(\stk', \str')}
 	\justifies
 	\sostrans
 		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+		{\pgm}{\ip'}{\op'}{(\stk',\str')}
 	\using{\rcompeensos}
 	\qquad
 \end{prooftree}
 $$
 
-\medskip
+\bigskip
+
+De regel voor $\StmExec$ zou in de structurele operationele semantiek als volgt zijn: 
 $$
 \begin{prooftree}
-	\sostranseind
-		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\ip'}{\op'}{(\stk', \str')}
-	\justifies
+\axjustifies
 	\sostrans
-		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm}{\ip'}{\op'}{(\stk',\str')}
-	\using{\rcomptweesos}
+		{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
+		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+	\using{\rexecsos}
 	\qquad
+		\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
 \end{prooftree}
 $$
 
-- 
cgit v1.2.3

