
diff -r 7cb94089324e -r 7f5243700f25 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 14:09:35 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 14:14:35 2013 +0000
@@ -1351,7 +1351,55 @@
   If started with @{term "([], [Oc])"} it halts with the
   non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;
   but with @{term "([], [Oc])"} according to def Chap 8
+*}
 
+section {* XYZ *}
+
+text {*
+One of the main objectives of the paper is the construction and verification of Universal Turing machine (UTM). A UTM takes the code of any Turing machine $M$ and its arguments $a_1, a_2, \ldots, a_n$ as input and computes to the same effect as $M$ does on $a_1, a_2, \ldots, a_n$. That is to say:
+\begin{enumerate}
+    \item If $M$ terminates and gives a result on $a_1, a_2, \ldots, a_n$, so does $UTM$ on input
+        $
+        code(M), a_1, a_1, a_2, \ldots, a_n
+        $.
+    \item If $M$ loops forever on $a_1, a_2, \ldots, a_n$, then $UTM$ does the same on $code (M), a_1, a_1, a_2, \ldots, a_n$.
+\end{enumerate}
+
+The existence of UTM is the cornerstone of {\em Turing Thesis}, which says: any effectively computable function can be computed by a Turing Machine. The evaluation of Turing machine is obviously effective computable (otherwise, Turing machine is not an effect computation model). So, if the evaluation function of Turing machine can not be implemented by a Turing machine, the {\em Turing Thesis} would fail. Although people believe that UTM exists, few have gave one in close form and prove its correctness with the only exception of Asperti.
+
+
+The method to obtain Universal Turing machine (UTM), as hinted by Boolos's book, is first constructing a recursive function recF (named Universal Function), which serves as an interpreter for Turing machine program, and then the UTM is obtained by $translate(recF)$. However, since any particular recursive function only takes fixed number of arguments determined by its construction,  no matter how recF is constructed, it can only server as interpret for Turing machines which take the fixed number of arguments as input. Our solution is to precede the $translate(recF)$ with a Turing machine which compacts multiple arguments into one argument using Wang's coding. Now, $recF$ is defined as a function taking two arguments, where the first is the code of Turing machine to be interpreted and the second is the packed arguments.
+
+The construction of recF roughly follows the idea in the book. Since the book gives no correctness proof of the construction (not even an informal one), we have to formulate the correctness statements and as well as their formal proofs explicitly. As an unexpected outcome of this formulation, we identified one inconsistency in Boolos' book. Every Turing machine is supposed to compute an arithmetic function which is possibly partial. When the TM is started with an argument where the function is undefined, the definition on Chapter 3 (page 32) says:
+\begin{quote}
+(e) If the function that is to be computed assigns no value to the arguments that are
+represented initially on the tape, then the machine either will never halt, or will
+halt in some nonstandard configuration such as $B_n11111$ or $B11_n111$ or $B11111_n$.
+\end{quote}
+According to this definition, a TM can signify a non-result either by looping forever or get into state 0 with a nonstandard tape. However, when we were trying to formalize the universal function in Chapter 8, we found the definition given there is not in accordance. On page 93, an recursive function $stdh$ is defined as:
+	\begin{equation}\label{stdh_def}
+stdh(m, x, t) = stat(conf(m, x, t)) + nstd(conf(m, x, t))
+\end{equation}
+Where $ stat(conf(m, x, t)) $ computes the current state of the simulated Turing machine, and the $nstd(conf(m, x, t))$ returns $1$ if the tape content is nonstandard. If either one evaluates to nonzero, stdh(m, x, t) will be nonzero, because of the $+$ operation. One the same page, a function $halt(m, x)$ is defined to in terms of $stdh$ to computes the steps the Turing machine needs to execute before halt, which stipulates the TM halts when nstd(conf(m, x, t)) returns $0$. According to this definition, the simulated Turing machine will continue to run after getting into state $0$ with a nonstandard tape. The consequence of this inconsistency is that: there exists Turing machines which computes non-value according to Chapter 3, but returns a proper result according to Chapter 8. One such Truing machine is:
+    \begin{equation}\label{contrived_tm}
+        [(L, 0), (L, 2), (R, 2), (R, 0)]
+    \end{equation}
+Starting in a standard configuration (1, [], [Oc]), it goes through the following series of configurations leading to state 0:
+\[
+(1, [], [Oc]) \rightsquigarrow (L, 2) \rightsquigarrow  (2, [], [Bk, Oc]) \rightsquigarrow (R, 2)\rightsquigarrow (2, [Bk], [Oc]) \rightsquigarrow (R, 0)\rightsquigarrow  (0, [Bk, Oc], [])
+\]
+According to Chapter 3, this Turing machine halts and gives a non-result. According to Chapter 8, it will continue to fetch and execute the next instruction. The fetching function $actn$ and $newstat$ in \eqref{fetch-def} (taken from page 92) takes $q$ as current state and $r$ as the currently scanned cell.
+\begin{equation}\label{fetch-def}
+\begin{aligned}
+	actn(m, q, r )  &= ent(m, 4(q - 1)  + 2 \cdot scan(r )) \\
+newstat(m, q, r ) & = ent(m, (4(q - 1) + 2 \cdot scan(r )) + 1)
+\end{aligned}
+\end{equation}
+For our instance, $q=0$ and $r = 1$. Because $q - 1 = 0 - 1 = 1 - 1 = 0$, the instruction fetched by \eqref{fetch-def} at state $0$ will be the same as if the machine is at state $0$. So the Turing machine will go through the follow execution and halt with a standard tape:
+\[
+(0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])
+\]
+In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. 
 *}
 
 (*




