% 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
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
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.

De twee compositieregels zijn als volgt:

$$
\begin{prooftree}
	\sostrans
		{\stm}{\ip}{\op}{(\stk, \str)}
		{\pgm'}{\ip'}{\op'}{(\stk', \str')}
	\justifies
	\sostrans
		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
	\using{\rcompeensos}
	\qquad
\end{prooftree}
$$

\medskip
$$
\begin{prooftree}
	\sostranseind
		{\stm}{\ip}{\op}{(\stk, \str)}
		{\ip'}{\op'}{(\stk', \str')}
	\justifies
	\sostrans
		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
		{\pgm}{\ip'}{\op'}{(\stk',\str')}
	\using{\rcomptweesos}
	\qquad
\end{prooftree}
$$

\bigskip
De regel voor $\StmTail$ zou in de structurele operationele semantiek als volgt
zijn:

$$
\begin{prooftree}
	\axjustifies
	\sostranseind
		{\StmTail}{\ip}{\op}{(\stk,\str)}
		{\ip}{\op}{(\push{s}{\stk'}, \str)}
	\using{\rtailsos}
	\qquad
	\text{met $\pop{\stk} = (c~s,\stk')$.}
\end{prooftree}
$$