--- a/Paper/Paper.thy Wed Mar 27 13:24:41 2013 +0000
+++ b/Paper/Paper.thy Fri Mar 29 01:36:45 2013 +0000
@@ -3,7 +3,9 @@
imports "../thys/UTM" "../thys/Abacus_Defs"
begin
-
+(*
+value "map (steps (1,[],[Oc]) ([(L,0),(L,2),(R,2),(R,0)],0)) [0 ..< 4]"
+*)
hide_const (open) s
@@ -69,7 +71,7 @@
exponent ("_\<^bsup>_\<^esup>") and
tcopy ("copy") and
tape_of ("\<langle>_\<rangle>") and
- tm_comp ("_ \<oplus> _") and
+ tm_comp ("_ ; _") and
DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and
inv_begin0 ("I\<^isub>0") and
inv_begin1 ("I\<^isub>1") and
@@ -530,7 +532,7 @@
blank cell to the right list; otherwise we have to remove the
head from the left-list and prepend it to the right list. Similarly
in the fourth clause for a right move action. The @{term Nop} operation
- leaves the the tape unchanged.
+ leaves the tape unchanged.
%Note that our treatment of the tape is rather ``unsymmetric''---we
%have the convention that the head of the right list is where the
@@ -599,12 +601,12 @@
The @{text 0}-state is special in that it will be used as the
``halting state''. There are no instructions for the @{text
0}-state, but it will always perform a @{term Nop}-operation and
- remain in the @{text 0}-state. Unlike Asperti and Riccioti
- \cite{AspertiRicciotti12}, we have chosen a very concrete
+ remain in the @{text 0}-state.
+ We have chosen a very concrete
representation for Turing machine programs, because when constructing a universal
Turing machine, we need to define a coding function for programs.
- This can be directly done for our programs-as-lists, but is
- slightly more difficult for the functions used by Asperti and Ricciotti.
+ %This can be directly done for our programs-as-lists, but is
+ %slightly more difficult for the functions used by Asperti and Ricciotti.
Given a program @{term p}, a state
and the cell being scanned by the head, we need to fetch
@@ -639,38 +641,7 @@
state, and the third that every next-state is one of the states mentioned in
the program or being the @{text 0}-state.
- We need to be able to sequentially compose Turing machine programs. Given our
- concrete representation, this is relatively straightforward, if
- slightly fiddly. We use the following two auxiliary functions:
-
- \begin{center}
- \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
- @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
- \end{tabular}
- \end{center}
-
- \noindent
- The first adds @{text n} to all states, except the @{text 0}-state,
- thus moving all ``regular'' states to the segment starting at @{text
- n}; the second adds @{term "Suc(length p div 2)"} to the @{text
- 0}-state, thus redirecting all references to the ``halting state''
- to the first state after the program @{text p}. With these two
- functions in place, we can define the \emph{sequential composition}
- of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
-
- \begin{center}
- @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
- \end{center}
-
- \noindent
- %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
- %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
- %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
- %have been shifted in order to make sure that the states of the composed
- %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
- %an initial segment of the natural numbers.
-
+
A \emph{configuration} @{term c} of a Turing machine is a state
together with a tape. This is written as @{text "(s, (l, r))"}. We
say a configuration \emph{is final} if @{term "s = (0::nat)"} and we
@@ -714,6 +685,65 @@
actually halt, but rather transitions to the @{text 0}-state (the
final state) and remains there performing @{text Nop}-actions until
@{text n} is reached.
+
+
+ We often need to restrict tapes to be in standard form, which means
+ the left list of the tape is either empty or only contains @{text "Bk"}s, and
+ the right list contains some ``clusters'' of @{text "Oc"}s separated by single
+ blanks. To make this formal we define the following overloaded function
+ encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
+ %
+ \begin{equation}
+ \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
+ @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
+ \end{tabular}\hspace{6mm}
+ \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
+ @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
+ @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
+ \end{tabular}}\label{standard}
+ \end{equation}
+ %
+ \noindent
+ A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+ @{text l}
+ and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
+ leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
+ is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
+
+
+ We need to be able to sequentially compose Turing machine programs. Given our
+ concrete representation, this is relatively straightforward, if
+ slightly fiddly. We use the following two auxiliary functions:
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+ @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first adds @{text n} to all states, except the @{text 0}-state,
+ thus moving all ``regular'' states to the segment starting at @{text
+ n}; the second adds @{term "Suc(length p div 2)"} to the @{text
+ 0}-state, thus redirecting all references to the ``halting state''
+ to the first state after the program @{text p}. With these two
+ functions in place, we can define the \emph{sequential composition}
+ of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
+
+ \begin{center}
+ @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+ %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ %have been shifted in order to make sure that the states of the composed
+ %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ %an initial segment of the natural numbers.
\begin{figure}[t]
\begin{center}
@@ -830,30 +860,7 @@
\end{figure}
- We often need to restrict tapes to be in standard form, which means
- the left list of the tape is either empty or only contains @{text "Bk"}s, and
- the right list contains some ``clusters'' of @{text "Oc"}s separated by single
- blanks. To make this formal we define the following overloaded function
- encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
- %
- \begin{equation}
- \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
- @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
- \end{tabular}\hspace{6mm}
- \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
- @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
- @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
- \end{tabular}}\label{standard}
- \end{equation}
- %
- \noindent
- A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
- @{text l}
- and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
- leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
- is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
+
Before we can prove the undecidability of the halting problem for
our Turing machines working on standard tapes, we have to analyse
@@ -1061,7 +1068,7 @@
\end{center}
\caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of
@{term tcopy_begin}. Below, the invariants only for the starting and halting states of
- @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter
+ @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant, the parameter
@{term n} stands for the number
of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
\end{figure}
@@ -1392,7 +1399,7 @@
The main point of recursive functions is that we can relatively
easily construct a universal Turing machine via a universal
function. This is different from Norrish \cite{Norrish11} who gives a universal
- function for Church numbers, and also from Asperti and Ricciotti
+ function for the lambda-calculus, and also from Asperti and Ricciotti
\cite{AspertiRicciotti12} who construct a universal Turing machine
directly, but for simulating Turing machines with a more restricted alphabet.
Unlike Norrish \cite{Norrish11}, we need to represent recursive functions
@@ -1514,7 +1521,7 @@
containing the inconsistency was introduced in the fourth edition
\cite{BoolosFourth}). The central
idea about Turing machines is that when started with standard tapes
- they compute a partial arithmetic function. The inconsitency arises
+ they compute a partial arithmetic function. The inconsistency arises
when they define the case when this function should \emph{not} return a
result. Boolos at al write in Chapter 3, Page 32:
@@ -1538,7 +1545,7 @@
simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}
if the tape content is non-standard. If either one evaluates to
something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of
- the $+$-operation. One the same page, a function @{text "halt(m, x)"} is defined
+ the $+$-operation. On the same page, a function @{text "halt(m, x)"} is defined
in terms of @{text stdh} for computing the steps the Turing machine needs to
execute before it halts (in case it halts at all). According to this definition, the simulated
Turing machine will continue to run after entering the @{text 0}-state
@@ -1562,9 +1569,9 @@
\noindent
If started with standard tape @{term "([], [Oc])"}, it halts with the
- non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
+ non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no
result is calculated; but with the standard tape @{term "([], [Oc])"} according to the
- definition in Chapter 8.
+ definition in Chapter 8. ????
We solve this inconsistency in our formalisation by
setting up our definitions so that the @{text counter_example} Turing machine does not
produce any result by looping forever fetching @{term Nop}s in state @{text 0}.
@@ -1641,9 +1648,11 @@
\<or> \<not>P"}. For reasoning about computability we need to formalise a
concrete model of computations. We could have followed Norrish
\cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,
- but then we would have to reimplement his infrastructure for
- reducing $\lambda$-terms on the ML-level. We would still need to
- connect his work to Turing machines for proofs that make essential use of them
+ but then we would still have
+ %to reimplement his infrastructure for
+ %reducing $\lambda$-terms on the ML-level.
+ %We would still need
+ to connect his work to Turing machines for proofs that make essential use of them
(for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
We therefore have formalised Turing machines in the first place and the main
@@ -1724,7 +1733,7 @@
introduced a more primitive specification logic, on which
Hoare-rules can be provided for special cases. It remains to be
seen whether their specification logic for assembly code can make it
- easier to reason about our Turing programs. That would be an
+ easier to reason about our Turing programs. Myreen ??? That would be an
attractive result, because Turing machine programs are very much
like assembly programs and it would connect some very classic work on
Turing machines to very cutting-edge work on machine code