theory UTM

imports Main recursive abacus UF GCD turing_hoare

begin

section {* Wang coding of input arguments *}

text {*

  The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,

  where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. 

  (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may

  very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 

  composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple 

  input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second

  argument. 

  However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 

  function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 

  Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.

\newlength{\basewidth}

\settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}

\newlength{\baseheight}

\settoheight{\baseheight}{$B:R$}

\newcommand{\vsep}{5\baseheight}

The TM used to generate the Wang's code of input arguments is divided into three TMs

 executed sequentially, namely $prepare$, $mainwork$ and $adjust$\<exclamdown>\<pounds>According to the

 convention, start state of ever TM is fixed to state $1$ while the final state is

 fixed to $0$.

The input and output of $prepare$ are illustrated respectively by Figure

\ref{prepare_input} and \ref{prepare_output}.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  [tbox/.style = {draw, thick, inner sep = 5pt}]

  \node (0) {};

  \node (1) [tbox, text height = 3.5pt, right = -0.9pt of 0] {\wuhao $m$};

  \node (2) [tbox, right = -0.9pt of 1] {\wuhao $0$};

  \node (3) [tbox, right = -0.9pt of 2] {\wuhao $a_1$};

  \node (4) [tbox, right = -0.9pt of 3] {\wuhao $0$};

  \node (5) [tbox, right = -0.9pt of 4] {\wuhao $a_2$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [tbox, right = -0.9pt of 6] {\wuhao $a_n$};

  \draw [->, >=latex, thick] (1)+(0, -4\baseheight) -- (1);

\end{tikzpicture}}

\caption{The input of TM $prepare$} \label{prepare_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.5pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_n$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $0$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $1$};

  \draw [->, >=latex, thick] (10)+(0, -4\baseheight) -- (10);

\end{tikzpicture}}

\caption{The output of TM $prepare$} \label{prepare_output}

\end{figure}

As shown in Figure \ref{prepare_input}, the input of $prepare$ is the same as the the input

of UTM, where $m$ is the Godel coding of the TM being interpreted and $a_1$ through $a_n$ are the $n$ input arguments of the TM under interpretation. The purpose of $purpose$ is to transform this initial tape layout to the one shown in Figure \ref{prepare_output},

which is convenient for the generation of Wang's codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ and ends after $a_1$ is encoded. The coding result is stored in an accumulator at the end of the tape (initially represented by the $1$ two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by two blanks on both ends with the rest so that movement conditions can be implemented conveniently in subsequent TMs, because, by convention,

two consecutive blanks are usually used to signal the end or start of a large chunk of data. The diagram of $prepare$ is given in Figure \ref{prepare_diag}.

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(6)+(0.3\basewidth, 0)$) {$7$};

     \node[circle,draw] (8) at ($(7)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) edge [loop above] node[above] {$S_1:L$} (1)

     ;

     \draw [->, >=latex] (1) -- node[above] {$S_0:S_1$} (2)

     ;

     \draw [->, >=latex] (2) edge [loop above] node[above] {$S_1:R$} (2)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_0:L$} (3)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_1:S_0$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) edge[loop above] node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_0:R$} (5)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:R$} (6)

     ;

     \draw [->, >=latex] (6) edge[bend left = 50] node[below] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_0:R$} (7)

     ;

     \draw [->, >=latex] (7) edge[loop above] node[above] {$S_0:S_1$} (7)

     ;

     \draw [->, >=latex] (7) -- node[above] {$S_1:L$} (8)

     ;

 \end{tikzpicture}}

\caption{The diagram of TM $prepare$} \label{prepare_diag}

\end{figure}

The purpose of TM $mainwork$ is to compute the Wang's encoding of $a_1, \ldots, a_n$. Every bit of $a_1, \ldots, a_n$, including the separating bits, is processed from left to right.

In order to detect the termination condition when the left most bit of $a_1$ is reached,

TM $mainwork$ needs to look ahead and consider three different situations at the start of

every iteration:

\begin{enumerate}

    \item The TM configuration for the first situation is shown in Figure \ref{mainwork_case_one_input},

        where the accumulator is stored in $r$, both of the next two bits

        to be encoded are $1$. The configuration at the end of the iteration

        is shown in Figure \ref{mainwork_case_one_output}, where the first 1-bit has been

        encoded and cleared. Notice that the accumulator has been changed to

        $(r+1) \times 2$ to reflect the encoded bit.

    \item The TM configuration for the second situation is shown in Figure

        \ref{mainwork_case_two_input},

        where the accumulator is stored in $r$, the next two bits

        to be encoded are $1$ and $0$. After the first

        $1$-bit was encoded and cleared, the second $0$-bit is difficult to detect

        and process. To solve this problem, these two consecutive bits are

        encoded in one iteration.  In this situation, only the first $1$-bit needs

        to be cleared since the second one is cleared by definition.

        The configuration at the end of the iteration

        is shown in Figure \ref{mainwork_case_two_output}.

        Notice that the accumulator has been changed to

        $(r+1) \times 4$ to reflect the two encoded bits.

    \item The third situation corresponds to the case when the last bit of $a_1$ is reached.

        The TM configurations at the start and end of the iteration are shown in

        Figure \ref{mainwork_case_three_input} and \ref{mainwork_case_three_output}

        respectively. For this situation, only the read write head needs to be moved to

        the left to prepare a initial configuration for TM $adjust$ to start with.

\end{enumerate}

The diagram of $mainwork$ is given in Figure \ref{mainwork_diag}. The two rectangular nodes

labeled with $2 \times x$ and $4 \times x$ are two TMs compiling from recursive functions

so that we do not have to design and verify two quite complicated TMs.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $1$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [right = -0.9pt of 11] {\ldots \ldots};

  \node (13) [draw, right = -0.9pt of 12, thick, inner sep = 5pt] {\wuhao $0$};

  \node (14) [draw, text height = 3.9pt, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (13)+(0, -4\baseheight) -- (13);

\end{tikzpicture}}

\caption{The first situation for TM $mainwork$ to consider} \label{mainwork_case_one_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [right = -0.9pt of 11] {\ldots \ldots};

  \node (13) [draw, right = -0.9pt of 12, thick, inner sep = 5pt] {\wuhao $0$};

  \node (14) [draw, text height = 2.7pt, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $(r+1) \times 2$};

  \draw [->, >=latex, thick] (13)+(0, -4\baseheight) -- (13);

\end{tikzpicture}}

\caption{The output for the first case of TM $mainwork$'s processing}

\label{mainwork_case_one_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $1$};

  \node (12) [draw, right = -0.9pt of 11, thick, inner sep = 5pt] {\wuhao $0$};

  \node (13) [right = -0.9pt of 12] {\ldots \ldots};

  \node (14) [draw, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $0$};

  \node (15) [draw, text height = 3.9pt, right = -0.9pt of 14, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (14)+(0, -4\baseheight) -- (14);

\end{tikzpicture}}

\caption{The second situation for TM $mainwork$ to consider} \label{mainwork_case_two_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $a_1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [draw, right = -0.9pt of 5, thick, inner sep = 5pt] {\wuhao $a_2$};

  \node (7) [right = -0.9pt of 6] {\ldots \ldots};

  \node (8) [draw, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $a_i$};

  \node (9) [draw, right = -0.9pt of 8, thick, inner sep = 5pt] {\wuhao $1$};

  \node (10) [draw, right = -0.9pt of 9, thick, inner sep = 5pt] {\wuhao $0$};

  \node (11) [draw, right = -0.9pt of 10, thick, inner sep = 5pt] {\wuhao $0$};

  \node (12) [draw, right = -0.9pt of 11, thick, inner sep = 5pt] {\wuhao $0$};

  \node (13) [right = -0.9pt of 12] {\ldots \ldots};

  \node (14) [draw, right = -0.9pt of 13, thick, inner sep = 5pt] {\wuhao $0$};

  \node (15) [draw, text height = 2.7pt, right = -0.9pt of 14, thick, inner sep = 5pt] {\wuhao $(r+1) \times 4$};

  \draw [->, >=latex, thick] (14)+(0, -4\baseheight) -- (14);

\end{tikzpicture}}

\caption{The output for the second case of TM $mainwork$'s processing}

\label{mainwork_case_two_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (7)+(0, -4\baseheight) -- (7);

\end{tikzpicture}}

\caption{The third situation for TM $mainwork$ to consider} \label{mainwork_case_three_input}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (3)+(0, -4\baseheight) -- (3);

\end{tikzpicture}}

\caption{The output for the third case of TM $mainwork$'s processing}

\label{mainwork_case_three_output}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(2)+(0, -7\baseheight)$) {$7$};

     \node[circle,draw] (8) at ($(7)+(0, -7\baseheight)$) {$8$};

     \node[circle,draw] (9) at ($(8)+(0.3\basewidth, 0)$) {$9$};

     \node[circle,draw] (10) at ($(9)+(0.3\basewidth, 0)$) {$10$};

     \node[circle,draw] (11) at ($(10)+(0.3\basewidth, 0)$) {$11$};

     \node[circle,draw] (12) at ($(11)+(0.3\basewidth, 0)$) {$12$};

     \node[draw] (13) at ($(6)+(0.3\basewidth, 0)$) {$2 \times x$};

     \node[circle,draw] (14) at ($(13)+(0.3\basewidth, 0)$) {$j_1$};

     \node[draw] (15) at ($(12)+(0.3\basewidth, 0)$) {$4 \times x$};

     \node[draw] (16) at ($(15)+(0.3\basewidth, 0)$) {$j_2$};

     \node[draw] (17) at ($(7)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) edge[loop left] node[above] {$S_0:L$} (1)

     ;

     \draw [->, >=latex] (1) -- node[above] {$S_1:L$} (2)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_1:R$} (3)

     ;

     \draw [->, >=latex] (2) -- node[left] {$S_1:L$} (7)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_1:S_0$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) edge[loop above] node[above] {$S_0:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:R$} (5)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:S_1$} (6)

     ;

     \draw [->, >=latex] (6) edge[loop above] node[above] {$S_1:L$} (6)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_0:R$} (13)

     ;

     \draw [->, >=latex] (13) -- (14)

     ;

     \draw (14) -- ($(14)+(0, 6\baseheight)$) -- ($(1) + (0, 6\baseheight)$) node [above,midway] {$S_1:L$}

     ;

     \draw [->, >=latex] ($(1) + (0, 6\baseheight)$) -- (1)

     ;

     \draw [->, >=latex] (7) -- node[above] {$S_0:R$} (17)

     ;

     \draw [->, >=latex] (7) -- node[left] {$S_1:R$} (8)

     ;

     \draw [->, >=latex] (8) -- node[above] {$S_0:R$} (9)

     ;

     \draw [->, >=latex] (9) -- node[above] {$S_0:R$} (10)

     ;

     \draw [->, >=latex] (10) -- node[above] {$S_1:R$} (11)

     ;

     \draw [->, >=latex] (10) edge[loop above] node[above] {$S_0:R$} (10)

     ;

     \draw [->, >=latex] (11) edge[loop above] node[above] {$S_1:R$} (11)

     ;

     \draw [->, >=latex] (11) -- node[above] {$S_0:S_1$} (12)

     ;

     \draw [->, >=latex] (12) -- node[above] {$S_0:R$} (15)

     ;

     \draw [->, >=latex] (12) edge[loop above] node[above] {$S_1:L$} (12)

     ;

     \draw [->, >=latex] (15) -- (16)

     ;

     \draw (16) -- ($(16)+(0, -4\baseheight)$) -- ($(1) + (0, -18\baseheight)$) node [below,midway] {$S_1:L$}

     ;

     \draw [->, >=latex] ($(1) + (0, -18\baseheight)$) -- (1)

     ;

 \end{tikzpicture}}

\caption{The diagram of TM $mainwork$} \label{mainwork_diag}

\end{figure}

The purpose of TM $adjust$ is to encode the last bit of $a_1$. The initial and final configuration

of this TM are shown in Figure \ref{adjust_initial} and \ref{adjust_final} respectively.

The diagram of TM $adjust$ is shown in Figure \ref{adjust_diag}.

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $0$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $1$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \node (7) [draw, right = -0.9pt of 6, thick, inner sep = 5pt] {\wuhao $0$};

  \node (8) [draw, text height = 3.9pt, right = -0.9pt of 7, thick, inner sep = 5pt] {\wuhao $r$};

  \draw [->, >=latex, thick] (3)+(0, -4\baseheight) -- (3);

\end{tikzpicture}}

\caption{Initial configuration of TM $adjust$} \label{adjust_initial}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{1.2}{

\begin{tikzpicture}

  \node (0) {};

  \node (1) [draw, text height = 3.9pt, right = -0.9pt of 0, thick, inner sep = 5pt] {\wuhao $m$};

  \node (2) [draw, right = -0.9pt of 1, thick, inner sep = 5pt] {\wuhao $0$};

  \node (3) [draw, text height = 2.9pt, right = -0.9pt of 2, thick, inner sep = 5pt] {\wuhao $r+1$};

  \node (4) [draw, right = -0.9pt of 3, thick, inner sep = 5pt] {\wuhao $0$};

  \node (5) [draw, right = -0.9pt of 4, thick, inner sep = 5pt] {\wuhao $0$};

  \node (6) [right = -0.9pt of 5] {\ldots \ldots};

  \draw [->, >=latex, thick] (1)+(0, -4\baseheight) -- (1);

\end{tikzpicture}}

\caption{Final configuration of TM $adjust$} \label{adjust_final}

\end{figure}

\begin{figure}[h!]

\centering

\scalebox{0.9}{

\begin{tikzpicture}

     \node[circle,draw] (1) {$1$};

     \node[circle,draw] (2) at ($(1)+(0.3\basewidth, 0)$) {$2$};

     \node[circle,draw] (3) at ($(2)+(0.3\basewidth, 0)$) {$3$};

     \node[circle,draw] (4) at ($(3)+(0.3\basewidth, 0)$) {$4$};

     \node[circle,draw] (5) at ($(4)+(0.3\basewidth, 0)$) {$5$};

     \node[circle,draw] (6) at ($(5)+(0.3\basewidth, 0)$) {$6$};

     \node[circle,draw] (7) at ($(6)+(0.3\basewidth, 0)$) {$7$};

     \node[circle,draw] (8) at ($(4)+(0, -7\baseheight)$) {$8$};

     \node[circle,draw] (9) at ($(8)+(0.3\basewidth, 0)$) {$9$};

     \node[circle,draw] (10) at ($(9)+(0.3\basewidth, 0)$) {$10$};

     \node[circle,draw] (11) at ($(10)+(0.3\basewidth, 0)$) {$11$};

     \node[circle,draw] (12) at ($(11)+(0.3\basewidth, 0)$) {$0$};

     \draw [->, >=latex] (1) -- node[above] {$S_1:R$} (2)

     ;

     \draw [->, >=latex] (1) edge[loop above] node[above] {$S_0:S_1$} (1)

     ;

     \draw [->, >=latex] (2) -- node[above] {$S_1:R$} (3)

     ;

     \draw [->, >=latex] (3) edge[loop above] node[above] {$S_0:R$} (3)

     ;

     \draw [->, >=latex] (3) -- node[above] {$S_1:R$} (4)

     ;

     \draw [->, >=latex] (4) -- node[above] {$S_1:L$} (5)

     ;

     \draw [->, >=latex] (4) -- node[right] {$S_0:L$} (8)

     ;

     \draw [->, >=latex] (5) -- node[above] {$S_0:L$} (6)

     ;

     \draw [->, >=latex] (5) edge[loop above] node[above] {$S_1:S_0$} (5)

     ;

     \draw [->, >=latex] (6) -- node[above] {$S_1:R$} (7)

     ;

     \draw [->, >=latex] (6) edge[loop above] node[above] {$S_0:L$} (6)

     ;

     \draw (7) -- ($(7)+(0, 6\baseheight)$) -- ($(2) + (0, 6\baseheight)$) node [above,midway] {$S_0:S_1$}

     ;

     \draw [->, >=latex] ($(2) + (0, 6\baseheight)$) -- (2)

     ;

     \draw [->, >=latex] (8) edge[loop left] node[left] {$S_1:S_0$} (8)

     ;

     \draw [->, >=latex] (8) -- node[above] {$S_0:L$} (9)

     ;

     \draw [->, >=latex] (9) edge[loop above] node[above] {$S_0:L$} (9)

     ;

     \draw [->, >=latex] (9) -- node[above] {$S_1:L$} (10)

     ;

     \draw [->, >=latex] (10) edge[loop above] node[above] {$S_0:L$} (10)

     ;

     \draw [->, >=latex] (10) -- node[above] {$S_0:L$} (11)

     ;

     \draw [->, >=latex] (11) edge[loop above] node[above] {$S_1:L$} (11)

     ;

     \draw [->, >=latex] (11) -- node[above] {$S_0:R$} (12)

     ;

 \end{tikzpicture}}

\caption{Diagram of TM $adjust$} \label{adjust_diag}

\end{figure}

*}

definition rec_twice :: "recf"

  where

  "rec_twice = Cn 1 rec_mult [id 1 0, constn 2]"

definition rec_fourtimes  :: "recf"

  where

  "rec_fourtimes = Cn 1 rec_mult [id 1 0, constn 4]"

definition abc_twice :: "abc_prog"

  where

  "abc_twice = (let (aprog, ary, fp) = rec_ci rec_twice in 

                       aprog [+] dummy_abc ((Suc 0)))"

definition abc_fourtimes :: "abc_prog"

  where

  "abc_fourtimes = (let (aprog, ary, fp) = rec_ci rec_fourtimes in 

                       aprog [+] dummy_abc ((Suc 0)))"

definition twice_ly :: "nat list"

  where

  "twice_ly = layout_of abc_twice"

definition fourtimes_ly :: "nat list"

  where

  "fourtimes_ly = layout_of abc_fourtimes"

definition t_twice_compile :: "instr list"

where

  "t_twice_compile= (tm_of abc_twice @ (shift (mopup 1) (length (tm_of abc_twice) div 2)))"

definition t_twice :: "instr list"

  where

  "t_twice = adjust t_twice_compile"

definition t_fourtimes_compile :: "instr list"

where

  "t_fourtimes_compile= (tm_of abc_fourtimes @ (shift (mopup 1) (length (tm_of abc_fourtimes) div 2)))"

definition t_fourtimes :: "instr list"

  where

  "t_fourtimes = adjust t_fourtimes_compile"