\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\\
\langle pointer; not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
\langle pointer [\:], [\:], [0,1,1]\rangle \Rightarrow\\
\langle [\:], [\:], [1,1]\rangle\\
-\
+\\
$
-Eerst worden x en y op de stack gepusht zodat de stack [y,x] = [1,1].
+Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,1].
Deze stack is gelijk aan de stack in de termineerende configuratie: 1 = 1! dus y = x!.
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
eenfaculteit worden alle wiskundige operaties die bij de commando's horen
-achter elkaar uitgevoerd op de stack, waarbij het resultaat [1,1] is.
+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