an_faculteit.tex

   1 \subsection{Faculteit}
   2 Als we de analyse op een compleet programma toepassen komt er een \textit{Piet}
   3 programma uit dat behoorlijk fors is maar netjes zijn werk doet. Het programma
   4 dat we gaan vertalen berekent de faculteit van $x$ en stopt dat uiteindelijk in
   5 $y$.
   6 \begin{lstlisting}[title=Faculteit in \textit{While}]
   7 x:=5;
   8 y:=1;
   9 while $\neg$(x=1)
  10 do (
  11     y:=y*x;
  12     x:=x-1
  13 )
  14 \end{lstlisting}
  15
  16 In \textit{Piet'} ziet dit er als volgt uit...
  17 \begin{lstlisting}[title=Faculteit in \textit{Piet'}]
  18 push 10     // x:=5
  19 push 1      // y:=1
  20
  21 MARKERING A:
  22             // Un(2)
  23             // $\neg$(x=1) $\equiv$ $\neg$(x-1)>0)
  24
  25
  26             // x-1
  27             // Un(2)
  28 push 2      //
  29 push 1      //
  30 roll        //
  31 dup         //
  32 push 3      //
  33 push 1      //
  34 roll        //
  35 push 1      //
  36 sub         //
  37 not         // $\neg(x-1)$
  38
  39 push 1      // zet $0$ op de stack
  40 push 1
  41 sub
  42
  43 gre         // $\neg(x-1)>0$ oftewel x=1
  44
  45 pointer     // als x=0 dan draait de DP niet en gaat het programma naar pad B
  46             // als x$\neq$ dan draait de DP en gaat het programma naar pad A
  47
  48 PAD A:
  49 skip        // een oneindig aantal witte blokken, y is nu x!
  50             // evt een outchar om $y$ naar standardout te printen
  51
  52 PAD B:
  53             // y:=y*x
  54             // Bin(1, 2)
  55 dup         // Un(1)
  56 push 3      // Un(2+1)
  57 push 2      //
  58 roll        //
  59 dup         //
  60 push 4      //
  61 push 1      //
  62 roll        //
  63 mul         // x*y
  64 push 2      // Ass(1)
  65 push 1
  66 roll
  67 pop
  68
  69             // x:=x-1
  70 push 2      // Un(2)
  71 push 1
  72 roll
  73 dup
  74 push 3
  75 push 1
  76 roll
  77
  78
  79 push 1      //
  80 sub         // x-1
  81 push 3      // Ass(2)
  82 push 2
  83 roll
  84 pop
  85 push 2
  86 push 1
  87 roll
  88             // nu gaat het programma weer via een wit pad naar markering A
  89 \end{lstlisting}
  90
  91 Wat in \textit{Piet} er uit ziet als in Figuur~\ref{fig:img3}
  92 \begin{figure}[H]
  93         \caption{Faculteit vanuit \textit{While} naar \textit{Piet}}
  94         \label{fig:img3}
  95         \centering
  96         \fbox{\includegraphics[natheight=320px, natwidth=256px, height=320px,
  97         width=256px]{img3.png}}
  98 \end{figure}
  99
 100 \begin{figure}[H]
 101         \caption{Faculteit vanuit \textit{While} naar \textit{Piet}(geannoteerd)}
 102         \label{fig:img5}
 103         \centering
 104         \fbox{\includegraphics[natheight=320px, natwidth=256px, height=160px,
 105         width=128px]{img5.png}}
 106 \end{figure}
 107 De code blokken komen als volgt overeen met stukken\textit{While} code.\\
 108 \begin{tabular}{ll}
 109         A & \lstinline{x:=5; y:=1}\\
 110         B & \lstinline{$\neg$(x=1)}\\
 111         C & \lstinline{y:=y*x}\\
 112         D & \lstinline{x:=x-1}\\
 113         E & het stukje achter de while loop, hierin printen we de uitkomst zodat we er ook nog wat aan hebben, \\
 114          & dit gebeurt in het originele \textit{While}
 115         programma niet. Het pyramidevormige stuk zorgt voor terminatie.\\
 116         F & \lstinline{while$\neg$(x=1) do(y:=y*x; x:=x-1)}
 117 \end{tabular}
 118
 119 \begin{landscape}
 120 De afleidingsrij voor 1! ziet er als volgt uit:\\
 121 $
 122 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1;push \: 1, [\:], [\:], [\:]\rangle \Rightarrow\\
 123 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2;push \: 1, [\:], [\:], [1]\rangle \Rightarrow\\
 124 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1;push \: 2, [\:], [\:], [1,1]\rangle \Rightarrow\\
 125 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll;push \: 1, [\:], [\:], [2,1,1]\rangle \Rightarrow\\
 126 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup;roll, [\:], [\:], [1,2,1,1]\rangle \Rightarrow\\
 127 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [1,1]\rangle \Rightarrow\\
 128 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
 129 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,1,1,1]\rangle \Rightarrow\\
 130 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,1]\rangle \Rightarrow\\
 131 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
 132 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
 133 \langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [0,1,1]\rangle \Rightarrow\\
 134 \langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
 135 \langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,1,1]\rangle \Rightarrow\\
 136 \langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,1,1]\rangle \Rightarrow\\
 137 \langle pointer; not;greater, [\:], [\:], [0,1,1,1]\rangle \Rightarrow\\
 138 \langle pointer; not, [\:], [\:], [1,1,1]\rangle \Rightarrow\\
 139 \langle pointer [\:], [\:], [0,1,1]\rangle \Rightarrow\\
 140 \langle [\:], [\:], [1,1]\rangle\\
 141 \\
 142 $
 143 Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,1].
 144 Deze stack is gelijk aan de stack in de termineerende configuratie: 1 = 1! dus y = x!.
 145 Als bewijs dat de wiskundige operaties op de stack goed zijn uitgevoerd staat in
 146 de appendix onder het kopje voorbeelden een stukje code.  In het programma
 147 eenfaculteit worden alle wiskundige operaties die bij de commando's horen
 148 achter elkaar uitgevoerd op de stack, waarbij het resultaat [1,1] is.\\
 149 Bij de voorbeelden staan ook nog de programma's tweefaculteit en
 150 vijffaculteit die respectievelijk 2! en 5! uitrekenen.
 151 \end{landscape}
 152
 153 \newpage
 154
 155 \begin{landscape}
 156 De afleidingsrij voor 2! ziet er als volgt uit:\\
 157 $
 158 \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
 159 \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\\
 160 \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\\
 161 \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\\
 162 \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\\
 163 \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\\
 164 \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\\
 165 \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\\
 166 \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\\
 167 \langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
 168 \langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,2,1,2]\rangle \Rightarrow\\
 169 \langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
 170 \langle R_1; R_2; R_3;greater;subtract;push\:1;push \: 1, [\:], [\:], [0,1,2]\rangle \Rightarrow\\
 171 \langle R_1; R_2; R_3;greater;subtract;push\:1, [\:], [\:], [1,0,1,2]\rangle \Rightarrow\\
 172 \langle R_1; R_2; R_3;greater;subtract, [\:], [\:], [1,1,0,1,2]\rangle \Rightarrow\\
 173 \langle R_1; R_2; R_3;greater, [\:], [\:], [0,0,1,2]\rangle \Rightarrow\\
 174 \langle R_1; R_2; R_3, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
 175 \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\\
 176 \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\\
 177 \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\\
 178 \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\\
 179 \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\\
 180 \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\\
 181 \langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup, [\:], [\:], [2,1,1]\rangle \Rightarrow\\
 182 \langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4, [\:], [\:], [2,2,1,1]\rangle \Rightarrow\\
 183 \langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll; push \: 1, [\:], [\:], [4,2,2,1,1]\rangle \Rightarrow\\
 184 \langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul; roll, [\:], [\:], [1,4,2,2,1,1]\rangle \Rightarrow\\
 185 \langle R_1;R_2; pop; roll; push \: 1; push \: 2; mul, [\:], [\:], [2,1,1,2]\rangle \Rightarrow\\
 186 \langle R_1;R_2; pop; roll; push \: 1; push \: 2, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
 187 \langle R_1;R_2; pop; roll; push \: 1, [\:], [\:], [2,2,1,2]\rangle \Rightarrow\\
 188 \langle R_1;R_2; pop; roll, [\:], [\:], [1,2,2,1,2]\rangle \Rightarrow\\
 189 \langle R_1;R_2; pop, [\:], [\:], [1,2,2]\rangle \Rightarrow\\
 190 \langle R_1;R_2, [\:], [\:], [2,2]\rangle \Rightarrow\\
 191 \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\\
 192 \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\\
 193 \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\\
 194 \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\\
 195 \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\\
 196 \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\\
 197 \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\\
 198 \langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub; push \: 1, [\:], [\:], [2,2,2]\rangle \Rightarrow\\
 199 \langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3; sub, [\:], [\:], [1,2,2,2]\rangle \Rightarrow\\
 200 \langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2; push \: 3, [\:], [\:], [1,2,2]\rangle \Rightarrow\\
 201 \langle R_1; roll; push \: 1; push \: 2; pop; roll; push \: 2, [\:], [\:], [3,1,2,2]\rangle \Rightarrow\\
 202 \langle R_1; roll; push \: 1; push \: 2; pop; roll, [\:], [\:], [2,3,1,2,2]\rangle \Rightarrow\\
 203 \langle R_1; roll; push \: 1; push \: 2; pop, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
 204 \langle R_1; roll; push \: 1; push \: 2, [\:], [\:], [1,2]\rangle \Rightarrow\\
 205 \langle R_1; roll; push \: 1, [\:], [\:], [2,1,2]\rangle \Rightarrow\\
 206 \langle R_1; roll, [\:], [\:], [1,2,1,2]\rangle \Rightarrow\\
 207 \langle R_1, [\:], [\:], [2,1]\rangle \Rightarrow\\
 208 \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\\
 209 \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\\
 210 \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\\
 211 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3;dup, [\:], [\:], [1,2]\rangle \Rightarrow\\
 212 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1;push \: 3, [\:], [\:], [1,1,2]\rangle \Rightarrow\\
 213 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll;push \: 1, [\:], [\:], [3,1,1,2]\rangle \Rightarrow\\
 214 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1;roll, [\:], [\:], [1,3,1,1,2]\rangle \Rightarrow\\
 215 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;push \: 1, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
 216 \langle pointer; not;greater;subtract;push\:1;push \: 1;not;subtract;, [\:], [\:], [1,1,2,1]\rangle \Rightarrow\\
 217 \langle pointer; not;greater;subtract;push\:1;push \: 1;not, [\:], [\:], [0,2,1]\rangle \Rightarrow\\
 218 \langle pointer; not;greater;subtract;push\:1;push \: 1, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
 219 \langle pointer; not;greater;subtract;push\:1, [\:], [\:], [1,1,2,1]\rangle \Rightarrow\\
 220 \langle pointer; not;greater;subtract, [\:], [\:], [1,1,1,2,1]\rangle \Rightarrow\\
 221 \langle pointer; not;greater, [\:], [\:], [0,1,2,1]\rangle \Rightarrow\\
 222 \langle pointer; not, [\:], [\:], [1,2,1]\rangle \Rightarrow\\
 223 \langle pointer [\:], [\:], [0,2,1]\rangle \Rightarrow\\
 224 \langle [\:], [\:], [2,1]\rangle\\
 225 $
 226
 227 In deze afleidingsrij zijn de volgende afkortingen gebruikt:\\
 228 $
 229 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\\
 230 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\\
 231 R_3: pop; roll; push \: 1; push \: 2; mul; roll; push \: 1; push \: 4; dup; roll; push \: 2; push \: 3; dup; pointer; not\\
 232 $
 233
 234 Eerst worden x en y op de stack gestopt zodat de stack [y,x] = [1,2].
 235 De stack in de termineerende configuratie is [y',x'] = [2,1] en 2 = 2! dus x! = y' .
 236 Als bewijs dat de wiskundige operaties op de stack goed zijn uitgevoerd staat in
 237 de appendix onder het kopje voorbeelden een stukje code.  In het programma
 238 tweefaculteit worden alle wiskundige operaties die bij de commando's horen
 239 achter elkaar uitgevoerd op de stack, waarbij het resultaat [2,1] is.\\
 240 \end{landscape}