You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
\item Infinitely many registers, each storing a natural number ($\mathbb{N} \triangleq\{0, 1, 2, \dots\}$)
43
43
\item Each instruction has a label associated with it.
44
-
\end{itemize}
45
-
There are 3 instructions:
46
-
\begin{center}
47
-
\begin{tabular}{l l}
48
-
$\inc{i}{m}$ & Add 1 to register $\reglabel{i}$ and then jump to the instruction at $\instrlabel{m}$ \\
49
-
$\dec{i}{n}{m}$ & If $\reglabel{i} > 0$ then decrement it and jump to $\instrlabel{n}$, else jump to $\instrlabel{m}$ \\
50
-
$\halt$ & Halt the program.
51
-
\end{tabular}
52
-
\end{center}
44
+
\end{itemize}
45
+
There are 3 instructions:
46
+
\begin{center}
47
+
\begin{tabular}{l l}
48
+
$\inc{i}{m}$ & Add 1 to register $\reglabel{i}$ and then jump to the instruction at $\instrlabel{m}$ \\
49
+
$\dec{i}{n}{m}$ & If $\reglabel{i} > 0$ then decrement it and jump to $\instrlabel{n}$, else jump to $\instrlabel{m}$ \\
50
+
$\halt$ & Halt the program.
51
+
\end{tabular}
52
+
\end{center}
53
53
At each point in a program the registers are in a configuration $c = (l, r_0, \dots, r_n)$ (where $r_i$ is the value of $\reglabel{i}$ and $l$ is the instruction label $\instrlabel{l}$ that is about to be run).
54
54
\begin{itemize}
55
55
\item$c_0$ is the initial configuration, next configurations are $c_1, c_2, \dots$.
56
56
\item In a finite computation, the final configuration is the \textbf{halting configuration}.
57
57
\item In a \textbf{proper halt} the program ends on a $\halt$.
58
58
\item In an \textbf{erroneous halt} the program jumps to a non-existent instruction, the \textbf{halting configuration} is for the instruction immediately before this jump.
@@ -315,12 +315,12 @@ \section{Encoding Programs as Numbers}
315
315
Hence using $H$ on any $B(p)$ we can determine if $p(p)$ halts ($H(B(p)) \Rightarrow\neg H(p(p))$).
316
316
\\
317
317
\\ Now we consider the case when $p = B$.
318
-
\begin{center}
319
-
\begin{tabular}{l p{.8\textwidth}}
320
-
\textbf{$B(B)$ halts} & Hence $B(B)$ does not halt. Contradiction! \\
321
-
\textbf{$B(B)$ does not halt} & Hence $B(B)$ halts. Contradiction! \\
322
-
\end{tabular}
323
-
\end{center}
318
+
\begin{center}
319
+
\begin{tabular}{l p{.8\textwidth}}
320
+
\textbf{$B(B)$ halts} & Hence $B(B)$ does not halt. Contradiction! \\
321
+
\textbf{$B(B)$ does not halt} & Hence $B(B)$ halts. Contradiction! \\
322
+
\end{tabular}
323
+
\end{center}
324
324
Hence by contradiction there is not such algorithm $H$.
325
325
\end{definitionbox}
326
326
In order to reason about programs consuming/running programs (as in the halting problem), we need a way to encode programs as data. Register machines use natural numbers as values for input, and hence we need a way to encode any register machine as a natural number.
@@ -338,15 +338,15 @@ \subsection{Pairs}
338
338
pair, the list, and the Register Machine (RM) instruction it represents, i.e. for
339
339
which pair $x, y$ do we have $\langle\langle x, y \rangle\rangle = B$, for which list $\ell$ of numbers do we get
340
340
$\ulcorner\ell\urcorner = B$, and for which Register Machine instruction $I$ do we have that
341
-
$\ulcorner I \urcorner = B$?
341
+
$\ulcorner I \urcorner = B$?
342
342
\\
343
343
\\ Show your work, e.g. binary representation of your $B$, etc.
344
344
\end{exambox}
345
345
\begin{exambox}{2a}{2020/21}
346
346
State your $CID$ and determine the pair, the list, and the Register Machine (RM)
347
347
instruction it represents, i.e. for which pair $x, y$ do we have $\langle\langle x, y \rangle\rangle = $ CID, for
348
348
which list $\ell$ of numbers do we get $\ulcorner ell \urcorner = CID$, and for which register-machine
349
-
instructions $I$ do we have that $\ulcorner I \urcorner = CID$?
349
+
instructions $I$ do we have that $\ulcorner I \urcorner = CID$?
350
350
\\
351
351
\\ Show your work, e.g. binary representation of your $CID$, etc.
352
352
\\
@@ -396,11 +396,11 @@ \section{Gadgets}
396
396
\item Operates on registers specified in the name of the gadget (e.g \textit{"Add $\reglabel{1}$ to $\reglabel{2}$"}).
397
397
\item Can use scratch registers (assumed to be zero prior to gadget and set to zero by the gadget before it exits - allows usage in loops)
398
398
\item We can rename the registers used in gadgets (simply change the registers used in the name (\textit{push $\reglabel{0}$ to $\reglabel{1}$$\to$ push $\regtemp{X}$ to $\regtemp{Y}$}), and have all scratch registers renamed to registers unused by other parts of the program)
399
-
\end{itemize}
399
+
\end{itemize}
400
400
For example we can create several gadgets in terms of registers that we can rename.
\\ We could attach invariants to every instruction, however it is usually only necessary to use them at the start, end and for loops (preconditions/postconditions).
Next we can use the instructions between invariant to find the states under which the invariants must hold.
471
471
\begin{center}
472
-
\begin{tabular}{l l p{0.7\textwidth}}
473
-
\textbf{1.} & $P[Z-1/Z] \Rightarrow I_1$ & After incrementing $Z$ needs to go to the start of the first loop. \\
474
-
\hline
475
-
\textbf{2.} & $I_1[L + 1/L, Z - 2/Z] \Rightarrow I_1$ & The loop decrements $L$ and increases $Z$ by two. After each loop iteration, $I_1$ must still hold. \\
476
-
\hline
477
-
\textbf{3.} & $I_1\land L = 0\Rightarrow I_2$ & If $L = 0$ the loop is escaped, and we move to $I_2$. \\
478
-
\hline
479
-
\textbf{4.} & $I_2[Z+1/Z,L-1/L] \Rightarrow I_2$ & Loop increments $L$ and decrements $Z$ on each iteration, after this, $I_2$ must still hold. \\
480
-
\hline
481
-
\textbf{5.} & $I_2\land Z = 0\Rightarrow I_3$ & Loop ends when $Z = 0$, moves to $I_3$. \\
482
-
\hline
483
-
\textbf{6.} & $I_3[X+1/X] \Rightarrow I_1$ & Large loop decrements $X$ on each iteration, invariant must hold with the new/decremented $X$. \\
484
-
\hline
485
-
\textbf{7.} & $I_3\land X = 0\Rightarrow Q$ & When the main $X$-decrementing loop is escaped, we move to exit, so $Q$ must hold.
486
-
\end{tabular}
472
+
\begin{tabular}{l l p{0.7\textwidth}}
473
+
\textbf{1.} & $P[Z-1/Z] \Rightarrow I_1$ & After incrementing $Z$ needs to go to the start of the first loop. \\
474
+
\hline
475
+
\textbf{2.} & $I_1[L + 1/L, Z - 2/Z] \Rightarrow I_1$ & The loop decrements $L$ and increases $Z$ by two. After each loop iteration, $I_1$ must still hold. \\
476
+
\hline
477
+
\textbf{3.} & $I_1\land L = 0\Rightarrow I_2$ & If $L = 0$ the loop is escaped, and we move to $I_2$. \\
478
+
\hline
479
+
\textbf{4.} & $I_2[Z+1/Z,L-1/L] \Rightarrow I_2$ & Loop increments $L$ and decrements $Z$ on each iteration, after this, $I_2$ must still hold. \\
480
+
\hline
481
+
\textbf{5.} & $I_2\land Z = 0\Rightarrow I_3$ & Loop ends when $Z = 0$, moves to $I_3$. \\
482
+
\hline
483
+
\textbf{6.} & $I_3[X+1/X] \Rightarrow I_1$ & Large loop decrements $X$ on each iteration, invariant must hold with the new/decremented $X$. \\
484
+
\hline
485
+
\textbf{7.} & $I_3\land X = 0\Rightarrow Q$ & When the main $X$-decrementing loop is escaped, we move to exit, so $Q$ must hold.
486
+
\end{tabular}
487
487
\end{center}
488
488
We can now use these constraints (also called \textit{verification conditions}) to determine an invariant.
489
489
\\
490
490
\\
491
491
\\ For each constraint we do:
492
492
\begin{enumerate}
493
-
\item Get the basic for (potentially one already derived) for the invariant in question.
494
-
\item If there is iteration, iterate to build up a disjunction.
495
-
\item Find the pattern, and then re-form the invariant based on it.
493
+
\item Get the basic for (potentially one already derived) for the invariant in question.
494
+
\item If there is iteration, iterate to build up a disjunction.
495
+
\item Find the pattern, and then re-form the invariant based on it.
0 commit comments