\subsection{Faculteit}
Als we de analyse op een compleet programma toepassen komt er een \textit{Piet}
-programma uit dat behoorlijk fors is maar netjes zijn werk doet. Dit programma
-berekent de faculteit van $x$ en stopt dat uiteindelijk in $y$.
+programma uit dat behoorlijk fors is maar netjes zijn werk doet. Het programma
+dat we gaan vertalen berekent de faculteit van $x$ en stopt dat uiteindelijk in
+$y$.
\begin{lstlisting}[title=Faculteit in \textit{While}]
x:=5;
y:=1;
)
\end{lstlisting}
-In \textit{Piet} ziet dit er als volgt uit...
+In \textit{Piet'} ziet dit er als volgt uit...
\begin{lstlisting}[title=Faculteit in \textit{Piet'}]
push 10 // x:=5
push 1 // y:=1
MARKERING A:
// Un(2)
- // $\neg$(x=1) $\equiv$ \neg(x-1)>0)
+ // $\neg$(x=1) $\equiv$ $\neg$(x-1)>0)
// x-1
// nu gaat het programma weer via een wit pad naar markering A
\end{lstlisting}
-Wat in piet er uit zit als in \ref{fig:img3}
+Wat in \textit{Piet} er uit ziet als in Figuur~\ref{fig:img3}
\begin{figure}[H]
- \caption{Factulteit vanuit \textit{While} naar \textit{Piet}}
+ \caption{Faculteit vanuit \textit{While} naar \textit{Piet}}
\label{fig:img3}
\centering
\fbox{\includegraphics[natheight=320px, natwidth=256px, height=320px,
width=256px]{img3.png}}
\end{figure}
+\begin{figure}[H]
+ \caption{Faculteit vanuit \textit{While} naar \textit{Piet}(geannoteerd)}
+ \label{fig:img5}
+ \centering
+ \fbox{\includegraphics[natheight=320px, natwidth=256px, height=160px,
+ width=128px]{img5.png}}
+\end{figure}
+De code blokken komen als volgt overeen met stukken\textit{While} code.\\
+\begin{tabular}{ll}
+ A & \lstinline{x:=5; y:=1}\\
+ B & \lstinline{$\neg$(x=1)}\\
+ C & \lstinline{y:=y*x}\\
+ D & \lstinline{x:=x-1}\\
+ E & het stukje achter de while loop, hierin printen we de uitkomst zodat we er ook nog wat aan hebben, \\
+ & dit gebeurt in het originele \textit{While}
+ programma niet. Het pyramidevormige stuk zorgt voor terminatie.\\
+ F & \lstinline{while$\neg$(x=1) do(y:=y*x; x:=x-1)}
+\end{tabular}
+
\begin{landscape}
De afleidingsrij voor 1! ziet er als volgt uit:\\
$
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
-\langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [0,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
\langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,1,1]\rangle \Rightarrow\\
achter elkaar uitgevoerd op de stack, waarbij het resultaat [1,1] is.\\
Bij de voorbeelden staan ook nog de programma's tweefaculteit en
vijffaculteit die respectievelijk 2! en 5! uitrekenen.
+\end{landscape}
+
+\newpage
+
+\begin{landscape}
+De afleidingsrij voor 2! ziet er als volgt uit:\\
+$
+\langle R_1; R_2; R_3; greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1;push \: 2, [\:], [\:], [\:]\rangle \Rightarrow
+\langle R_1; R_2; R_3; greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1, [\:], [\:], [2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2, [\:], [\:], [1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll, [\:], [\:], [1,2,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [2,1]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [2,2,1]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,2,2,1]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,2,2,1]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,2,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1, [\:], [\:], [0,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract;push\:1, [\:], [\:], [1,0,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater;subtract, [\:], [\:], [1,1,0,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3;greater, [\:], [\:], [0,0,1,2]\rangle \Rightarrow\\
+\langle R_1; R_2; R_3, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3; dup; pointer; not, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3; dup; pointer, [\:], [\:], [0,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3; dup, [\:], [\:], [1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2, [\:], [\:], [3,1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll, [\:], [\:], [2,3,1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup, [\:], [\:], [2,1,1]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4, [\:], [\:], [2,2,1,1]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1, [\:], [\:], [4,2,2,1,1]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll, [\:], [\:], [1,4,2,2,1,1]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul, [\:], [\:], [2,1,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1; push \: 2, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll; push \: 1, [\:], [\:], [2,2,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop; roll, [\:], [\:], [1,2,2,1,2]\rangle \Rightarrow\\
+\langle R_1;R_2; pop, [\:], [\:], [1,2,2]\rangle \Rightarrow\\
+\langle R_1;R_2, [\:], [\:], [2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3; dup; roll; push \: 1; push \: 2, [\:], [\:], [2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3; dup; roll; push \: 1, [\:], [\:], [2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3; dup; roll, [\:], [\:], [1,2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3; dup, [\:], [\:], [2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3, [\:], [\:], [2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1, [\:], [\:], [3,2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll, [\:], [\:], [1,3,2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1, [\:], [\:], [2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub, [\:], [\:], [1,2,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3, [\:], [\:], [1,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2, [\:], [\:], [3,1,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop; roll, [\:], [\:], [2,3,1,2,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2; pop, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1; push \: 2, [\:], [\:], [1,2]\rangle \Rightarrow\\
+\langle R_1; roll; push \: 1, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
+\langle R_1; roll, [\:], [\:], [1,2,1,2]\rangle \Rightarrow\\
+\langle R_1, [\:], [\:], [2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2, [\:], [\:], [2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1, [\:], [\:], [2,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll, [\:], [\:], [1,2,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [1,2]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,1,1,2]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,2]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [0,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,2,1]\rangle \Rightarrow\\
+\langle pointer; not;greater, [\:], [\:], [0,1,2,1]\rangle \Rightarrow\\
+\langle pointer; not, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
+\langle pointer [\:], [\:], [0,2,1]\rangle \Rightarrow\\
+\langle [\:], [\:], [2,1]\rangle\\
+$
+
+In deze afleidingsrij zijn de volgende afkortingen gebruikt:\\
+$
+R_1: pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2\\
+R_2: roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1; roll; push \: 1; push \: 3; dup; roll; push \: 1; push \: 2\\
+R_3: pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3; dup; pointer; not\\
+$
+
+Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,2].
+De stack in de termineerende configuratie is [y',x'] = [2,1] en 2 = 2! dus x! = y' .
+Als bewijs dat de wiskundige operaties op de stack goed zijn uitgevoerd staat in
+de appendix onder het kopje voorbeelden een stukje code. In het programma
+tweefaculteit worden alle wiskundige operaties die bij de commando's horen
+achter elkaar uitgevoerd op de stack, waarbij het resultaat [2,1] is.\\
\end{landscape}
\ No newline at end of file
repositories / sec1415.git / blobdiff