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:\\
-$$\mathcal{D} : s \rightarrow s$$\\
-Deze neemt een stack en gooit het bovenste element weg.\\
+\subsection{Semantiekbeschrijving}
-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.\\
+Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
+functie:\\
+$$\mathcal{D} : Stack \rightarrow Stack$$
+$$\mathcal{D} [\:] = [\:]$$
+$$\mathcal{D} [a:rest] = [rest] $$
+Deze functie haalt het bovenste element van de stack en gooit deze weg.\\
-\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 een stack uit te kunnen breiden met een element gebruiken we de volgende
+functie:\\
+$$\mathcal{E} : Stack\rightarrow (\mathbb{Z} \rightarrow 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] $$\\
+Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt
+het resultaat bovenop de stack.\\
+
+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] $$\\
+Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
+waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.
+
+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] $$\\
+Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
+en stopt het resultaat bovenop de stack.\\
+
+Om de geheeltallige 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] $$\\
+Deze functie haalt de bovenste twee elementen van de stack, berekent de
+geheeltallige deling van de tweede bovenste waarde door de bovenste waarde,
+en stopt het resultaat bovenop de stack.\\
+
+Om 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] $$\\
+Deze functie haalt de bovenste twee elementen van de stack, berekent het resultaat van de tweede bovenste
+waarde modulo de bovenste waarde, en stopt dit bovenop de stack.\\
+
+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] $$\\
+Deze functie haalt stopt een kopie van de bovenste waarde bovenop de stack.\\
+
+Om de 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$$\\
+Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
+stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
+
+Om 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$$\\
+Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
+de stack als het tweede bovenste element een hogere waarde heeft als dat van het
+bovenste element. Anders word 1 bovenop de stack gestopt.\\
+
+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\\
+{[push_{sos}]} \qquad
+\langle push, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
+{[roll_{sos}]} \qquad
+\langle roll, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
+{[inchar_{sos}]} \qquad
+\langle inchar, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
+{[innum_{sos}]} \qquad
+\langle innum, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
+{[outchar_{sos}]} \qquad
+\langle outchar, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
+{[outnum_{sos}]} \qquad
+\langle outnum, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, s\rangle\\
$
-\normalsize