semantiek en syntax aangepast

wiskundige operaties op stacks toegevoegd, semantiekregels aangepast,
argumenten voor tussentaal weggehaalt

diff --git a/semantics.tex b/semantics.tex
index fb4c747..eb7922e 100644 (file)
--- a/semantics.tex
+++ b/semantics.tex
@@ -17,107 +17,102 @@ Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
 op een niet terminerende transitie.\\ 
 
 \subsection{Semantiek beschrijving}
-Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
+
+Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende 
+functie:\\
 $$\mathcal{D} : s \rightarrow s$$\\
 Deze neemt een stack en gooit het bovenste element weg.\\
 
-Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
+Om een stack uit te kunnen breiden met een element gebruiken we de volgende 
+functie:\\
 $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
-Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
+Deze functie neemt een stack en een integer en voegt de integer toe bovenop de 
+stack.\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende 
+functie:\\
+$$\mathcal{ADD} : Stack \rightarrow Stack$$
+$$\mathcal{ADD} [\:] = [\:]$$
+$$\mathcal{ADD} [a] = [a] $$
+$$\mathcal{ADD} [a:b:rest] = [b+a:rest] $$\\
+
+Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we 
+de volgende functie:\\
+$$\mathcal{SUB} : Stack \rightarrow Stack$$
+$$\mathcal{SUB} [\:] = [\:]$$
+$$\mathcal{SUB} [a] = [a] $$
+$$\mathcal{SUB} [a:b:rest] = [b-a:rest] $$\\
+
+Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de 
+volgende functie:\\
+$$\mathcal{MUL} : Stack \rightarrow Stack$$
+$$\mathcal{MUL} [\:] = [\:]$$
+$$\mathcal{MUL} [a] = [a] $$
+$$\mathcal{MUL} [a:b:rest] = [b*a:rest] $$\\
+
+Om de integer deling van de bovenste twee elementen van de stack bovenop de 
+stack te krijgen gebruiken we de volgende functie:\\
+$$\mathcal{DIV} : Stack \rightarrow Stack$$
+$$\mathcal{DIV} [\:] = [\:]$$
+$$\mathcal{DIV} [a] = [a] $$
+$$\mathcal{DIV} [a:b:rest] = [b/a:rest] $$\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de 
+volgende functie:\\
+$$\mathcal{MOD} : Stack \rightarrow Stack$$
+$$\mathcal{MOD} [\:] = [\:]$$
+$$\mathcal{MOD} [a] = [a] $$
+$$\mathcal{MOD} [a:b:rest] = [b \: mod \: a:rest] $$\\
 
-\footnotesize
-$\infer        [{[}delete_{sos}{]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\
-\infer [{[}extend_{sos}{]}]
-               {       \langle extend \: z, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\
-\infer [{[}pop_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle}
-               {       \langle pop, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle}\\
-\infer [{[}add_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad
-                       \langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle add \: x,y, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}\\
-\infer [{[}subtract_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad
-                       \langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}\\
-\infer [{[}multiply_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad
-                       \langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}\\
-\infer [{[}divide_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad
-                       \langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}\\
-\infer [{[}mod_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad
-                       \langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'''\rangle}\\
-\infer [{[}duplicate_{sos} {]}]
-               {       \langle extend\: x, s_i, s_o, s\rangle \Rightarrow
-                       \langle s_i, s_o, s'\rangle}
-               {       \langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle}\\
-\infer [{[}not^0_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad
-                       \langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle}
-               {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle}$ if $x = 0\\
-\infer [{[}not^*_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad 
-                       \langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle}
-               {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle}$ if $x\neq 0\\
-\infer [{[}greater^<_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad 
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad 
-                       \langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow 
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
-                       \langle s_i, s_o, s'''\rangle}$ if $x>y\\
-\infer [{[}greater^>_{sos} {]}]
-               {       \langle delete, s_i, s_o, s\rangle \Rightarrow
-                               \langle s_i, s_o, s'\rangle \quad 
-                       \langle delete, s_i, s_o, s'\rangle \Rightarrow
-                               \langle s_i, s_o, s''\rangle \quad 
-                       \langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow 
-                               \langle s_i, s_o, s'''\rangle}
-               {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow 
-                               \langle s_i, s_o, s'''\rangle}$ if $x<y
+Om het bovenste element van een stack te dupliceren gebruiken we de 
+volgende functie:\\
+$$\mathcal{DUP} : Stack \rightarrow Stack$$
+$$\mathcal{DUP} [\:] = [\:]$$
+$$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de 
+volgende functie:\\
+$$\mathcal{NOT} : Stack \rightarrow Stack$$
+$$\mathcal{NOT} [\:] = [\:]$$
+$$\mathcal{NOT} [a:rest] = [0:rest] \: \text{if} \:  a \neq 0$$
+$$\mathcal{NOT} [a:rest] = [1:rest] \: \text{if} \: a = 0$$\\
+
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de 
+volgende functie:\\
+$$\mathcal{GRE} : Stack \rightarrow Stack$$
+$$\mathcal{GRE} [\:] = [\:]$$
+$$\mathcal{GRE} [a] = [a] $$
+$$\mathcal{GRE} [a:b:rest] = [0:rest] \: \text{if} \: a \geq b$$
+$$\mathcal{GRE} [a:b:rest] = [1:rest] \: \text{if} \: a < b$$\\
+
+Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\
+
+$
+{[pop_{sos}]}\qquad
+\langle pop, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o,\mathcal{D}(s)\rangle\\
+{[add_{sos}]}\qquad
+\langle add, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
+{[subtract_{sos} ]}\qquad
+\langle subtract, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
+{[multiply_{sos}]}\qquad
+\langle multiply, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
+{[divide_{sos}]} \qquad
+\langle divide, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
+{[mod_{sos}]} \qquad\qquad
+\langle mod, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
+{[duplicate_{sos}]} \qquad
+\langle duplicate, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
+{[not_{sos}]}\qquad\qquad
+\langle not, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
+{[greater_{sos}]} \qquad
+\langle greater, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{GRE}(s)\rangle \qquad \\
 $
-\normalsize

diff --git a/syntax.tex b/syntax.tex
index 8f8c696..080721a 100644 (file)
--- a/syntax.tex
+++ b/syntax.tex
@@ -36,13 +36,7 @@ die gedeeltelijk beschreven is in tabel \ref{tab:sy1}.
 Om de notatie leesbaar en overzichtelijk te houden beschrijven we de syntax
 niet in de oorspronkelijke kleuren notatie maar gebruiken we een woordelijke
 notatie. Dan ziet de grammatica er als volgt uit:\\
-$S ::= S1 ; S2\ |\ push\  n1\ |\ pop\ z\ |\ add\ z1\ z2\ |\ subtract\ z1\ z2\
-|\ multiply\ z1\ z2\ |\ divide\ z1\ z2\ |\\ mod\ z1\ z2\ |\ not\ z\ |\ greater\
-z1\ z2\ |\ pointer\ z\ |\ switch\ z\ |\ duplicate\ z\ |\ roll\ z1\ z2\ |\\
-in(char)\ c\ |\ in(number)\ z\ |\ out(char)\ z\ |\ out(number)\ z$\\ waarbij
-$n\in\mathbb{N}, z\in\mathbb{Z}$ en $c\in\{1, 2, ..., m$ waar $m$ het nummer is
-van het hoogste unicode karakter.\\ 
-
-Een probleem dat we verwachten is dat we op
-met deze beschrijving zeer grote bewijs-bomen/rijen krijgen vanwege het grote
-aantal composities, hier moeten we misschien nog iets anders op verzinnen.
+$S ::= S_1 ; S_2\ |\ push\ |\ pop\ |\ add\ |\ subtract\
+|\ multiply\ |\ divide\ |\\mod\ |\ not\ |\ greater\
+|\ pointer\ |\ switch\ |\ duplicate\ |\ roll\ |\\
+inchar\ |\ innum\ |\ outchar\ |\ outnum$\\