\documentclass[landscape,a4paper,9pt]{article}

\usepackage[dutch]{babel}
\usepackage{geometry}

\author{Camil Staps}
\title{Semantiek \& Correctheid\\\Large{Leertaak 6}}

\usepackage{senc}
\usepackage{amsthm}

\begin{document}

\allowdisplaybreaks

\maketitle

\section*{Opdracht 2.16}

\def\assA{\sass{z}{z+1}}
\def\assB{\sass{x}{x-y}}
\def\whileBody{\scomp\assA\assB}
\def\whileLoop{\swhile{y\leq x}{(\whileBody)}}
\def\whileComp{\scomp\whileBody\whileLoop}
\def\ifLoop{\sifthenelse{y\leq x}{(\whileComp)}\sskip}

\def\s#1#2#3{[#1,#2,#3]}

\begin{align*}
           & \transl{\scomp{\sass{z}{0}}{\whileLoop}}{[x\mapsto17,y\mapsto5]} \\
  \dimpl\> & \transl\whileLoop{\s{17}50} \\
  \dimpl\> & \transl\ifLoop{\s{17}50} \\
  \dimpl\> & \transl\whileComp{\s{17}50} \\
  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s{17}51} \\
  \dimpl\> & \transl\whileLoop{\s{12}51} \\
  \dimpl\> & \transl\ifLoop{\s{12}51} \\
  \dimpl\> & \transl\whileComp{\s{12}51} \\
  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s{12}52} \\
  \dimpl\> & \transl\whileLoop{\s752} \\
  \dimpl\> & \transl\ifLoop{\s752} \\
  \dimpl\> & \transl\whileComp{\s752} \\
  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s753} \\
  \dimpl\> & \transl\whileLoop{\s253} \\
  \dimpl\> & \transl\ifLoop{\s253} \\
  \dimpl\> & \transl\sskip{\s253} \>\dimpl\> \s253,
\end{align*}
waar $\s{a}{b}{c}$ kort is voor $[x\mapsto a,y\mapsto b,z\mapsto c]$.

\medskip
Een toestand $s$ waarvoor de afleidingsrij van $\scomp{\sass{z}0}\whileLoop$ en $s$ oneindig is, is bijvoorbeeld $s=[x\mapsto0,y\mapsto0]$.

\section*{Opdracht 2.18}
\begin{alignat*}{3}
  [\text{for}^\text{tt}_\text{sos}]\quad & \transl{\sfor{x}{a_1}{a_2}{S}}{s} \dimpl \transl{\scomp{\sass{x}{a_1}}\scomp{S}{{\sfor{x}{a_1+1}{a_2}{S}}}}{s} && \text{~if~} a_1 \le a_2 \\
  [\text{for}^\text{ff}_\text{sos}]\quad & \transl{\sfor{x}{a_1}{a_2}{S}}{s} \dimpl \transl{S}{s} && \text{~if~} a_1 \geq a_2
\end{alignat*}

\section*{Opdracht 2.21}
\begin{proof}
  In het geval dat $k=0$ is dit overduidelijk waar.

  Stel dat voor $k\leq k_0$ geldt dat als $\transl{S_1}s\dimpl^ks'$, dan $\transl{\scomp{S_1}{S_2}}s\dimpl^k\transl{S_2}{s'}$ (inductiehypothese).

  Stel verder dat $\transl{S_1}s \dimpl^{k+1} s''$. Dan hebben we een afleiding $\transl{S_1}s \dimpl \gamma \dimpl^k s''$ met $\gamma=\transl{S_1'}{s'}$. Dus $\transl{S_1}s \dimpl \transl{S_1'}{s'} \dimpl^k s''$.

  Dan geldt volgens de inductiehypothese voor elke $S_2$ dat$\transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.

  Voor de afleiding van $\transl{\scomp{S_1}{S_2}}s$ moeten we dan $\rcompsos1$ toepassen, en dus krijgen we: $\transl{\scomp{S_1}{S_2}}s \dimpl \transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.

  Hieruit volgt dat $\transl{\scomp{S_1}{S_2}}s \dimpl^{k+1} \transl{S_2}{s''}$.

  Uit het principe van volledige inductie volgt nu dat als $\transl{S_1}s \dimpl^k s'$, dan ook $\transl{\scomp{S_1}{S_2}}s \dimpl^k \transl{S_2}{s'}$, voor alle $S_1, S_2, s$ en $k\in\mathbb N$.

\end{proof}

\section*{Semantische equivalentie}
De definitie van semantische equivalentie is beter met een conjunctie dan met een disjunctie. Anders zouden alle paren statements $S_1,S_2$ equivalent zijn terwijl er toestanden zijn waarbij de twee statements na een eindig aantal stappen in verschillende toestanden $\gamma\neq\gamma'$ terechtkomen, die beide terminaal zijn, omdat dan de tweede conditie in de definitie waar is.

\section*{Opdracht 2.32}
$$S ::= \dots \mid \sassert{b}{S}$$
$$\rassert \quad \transl{\sassert{b}{S}}{s} \dimpl \transl{\sifthenelse{b}{S}{\sabort}}{s}$$

\section*{Opdracht 2.33}
In het geval van natuurlijke semantiek kunnen we in elke toestand $s$ terechtkomen waarvoor geldt dat $s~x>0$.

In het geval van structureel operationele semantiek hebben we afleidingsrijen van de volgende vormen:

\def\orwhile{\swhile{x\leq0}{\sor{\sass{x}{x-1}}{\sass{x}{(-1)\cdot x}}}}
\begin{align*}
  \transl{\scomp{\sass{x}{-1}}\orwhile}s \dimpl^* & s \quad\text{met $s~x>0$;}\\
  \transl{\scomp{\sass{x}{-1}}\orwhile}s \dimpl^* & \transl{\orwhile}s \\
                                         \dimpl\enspace & \dots\\
\end{align*}
Volgens mij zijn de twee semantieken voor dit statement dus \emph{niet} equivalent, want natuurlijke semantiek garandeert dat het statement op elke toestand termineert, terwijl structureel operationele semantiek dit niet doet.

\end{document}