1354 

  1354 *}

  1355 

  1356 section {* XYZ *}

  1357 

  1358 text {*

  1359 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:

  1360 \begin{enumerate}

  1361     \item If $M$ terminates and gives a result on $a_1, a_2, \ldots, a_n$, so does $UTM$ on input

  1362         $

  1363         code(M), a_1, a_1, a_2, \ldots, a_n

  1364         $.

  1365     \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$.

  1366 \end{enumerate}

  1367 

  1368 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.

  1369 

  1370 

  1371 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.

  1372 

  1373 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:

  1374 \begin{quote}

  1375 (e) If the function that is to be computed assigns no value to the arguments that are

  1376 represented initially on the tape, then the machine either will never halt, or will

  1377 halt in some nonstandard configuration such as $B_n11111$ or $B11_n111$ or $B11111_n$.

  1378 \end{quote}

  1379 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:

  1380 	\begin{equation}\label{stdh_def}

  1381 stdh(m, x, t) = stat(conf(m, x, t)) + nstd(conf(m, x, t))

  1382 \end{equation}

  1383 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:

  1384     \begin{equation}\label{contrived_tm}

  1385         [(L, 0), (L, 2), (R, 2), (R, 0)]

  1386     \end{equation}

  1387 Starting in a standard configuration (1, [], [Oc]), it goes through the following series of configurations leading to state 0:

  1388 \[

  1389 (1, [], [Oc]) \rightsquigarrow (L, 2) \rightsquigarrow  (2, [], [Bk, Oc]) \rightsquigarrow (R, 2)\rightsquigarrow (2, [Bk], [Oc]) \rightsquigarrow (R, 0)\rightsquigarrow  (0, [Bk, Oc], [])

  1390 \]

  1391 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.

  1392 \begin{equation}\label{fetch-def}

  1393 \begin{aligned}

  1394 	actn(m, q, r )  &= ent(m, 4(q - 1)  + 2 \cdot scan(r )) \\

  1395 newstat(m, q, r ) & = ent(m, (4(q - 1) + 2 \cdot scan(r )) + 1)

  1396 \end{aligned}

  1397 \end{equation}

  1398 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:

  1399 \[

  1400 (0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])

  1401 \]

  1402 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.