--- a/Paper.thy Fri Jan 11 13:18:33 2013 +0000
+++ b/Paper.thy Sat Jan 12 01:05:01 2013 +0000
@@ -46,15 +46,32 @@
by (auto split: if_splits prod.split list.split simp add: tstep.simps)
abbreviation
- "halt p inp out == \<exists>n. steps (1, inp) p n = (0, out)"
+ "run p inp out == \<exists>n. steps (1, inp) p n = (0, out)"
lemma haltP_def2:
"haltP p n = (\<exists>k l m.
- halt p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
+ run p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
unfolding haltP_def
apply(auto)
done
+lemma tape_of_nat_list_def2:
+ shows "tape_of_nat_list [] = []"
+ and "tape_of_nat_list [n] = exponent Oc (n+1)"
+ and "ns\<noteq> [] ==> tape_of_nat_list (n#ns) = (exponent Oc (n+1)) @ [Bk] @ (tape_of_nat_list ns)"
+apply(auto simp add: tape_of_nat_list.simps)
+apply(case_tac ns)
+apply(auto simp add: tape_of_nat_list.simps)
+done
+
+lemma tshift_def2:
+ fixes p::"tprog"
+ shows "tshift p n == (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
+apply(rule eq_reflection)
+apply(auto simp add: tshift.simps)
+done
+
+
consts DUMMY::'a
notation (latex output)
@@ -68,6 +85,8 @@
abc_lm_v ("lookup") and
abc_lm_s ("set") and
haltP ("stdhalt") and
+ change-termi-state ("adjust") and
+ tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
DUMMY ("\<^raw:\mbox{$\_$}>")
declare [[show_question_marks = false]]
@@ -130,8 +149,8 @@
with convenient reasoning infrastructures (for example induction
principles, recursion combinators and so on). But this is \emph{not}
the case with Turing machines (and also not with register machines):
-underlying their definition is a set of states together with a
-transition function, both of which are not structurally defined. This
+underlying their definitions are sets of states together with
+transition functions, all of which are not structurally defined. This
means we have to implement our own reasoning infrastructure in order
to prove properties about them. This leads to annoyingly fiddly
formalisations. We noticed first the difference between both,
@@ -149,7 +168,7 @@
\cite{AspertiRicciotti12}. They describe a complete formalisation of
Turing machines in the Matita theorem prover, including a universal
Turing machine. They report that the informal proofs from which they
-started are not ``sufficiently accurate to be directly useable as a
+started are \emph{not} ``sufficiently accurate to be directly useable as a
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
our formalisation we followed mainly the proofs from the textbook
\cite{Boolos87} and found that the description there is quite
@@ -186,11 +205,12 @@
character from a finite alphabet. Although computationally equivalent,
the more restrictive notion of Turing machines in \cite{Boolos87} makes
the reasoning more uniform. In addition some proofs \emph{about} Turing
-machines will be simpler. The reason is that one often needs to encode
+machines are simpler. The reason is that one often needs to encode
Turing machines---consequently if the Turing machines are simpler, then the coding
functions are simpler too. Unfortunately, the restrictiveness also makes
-it harder to design programs for these Turing machines. Therefore in order
-to construct a \emph{universal Turing machine} we follow the proof in
+it harder to design programs for these Turing machines. In order
+to construct a \emph{universal Turing machine} we therefore do not follow
+\cite{AspertiRicciotti12}, instead follow the proof in
\cite{Boolos87} by relating abacus machines to Turing machines and in
turn recursive functions to abacus machines. The universal Turing
machine can then be constructed as a recursive function.
@@ -245,8 +265,8 @@
\noindent
Note that by using lists each side of the tape is only finite. The
- potential infinity is achieved by adding an appropriate blank cell
- whenever the read-write unit goes over the ``edge'' of the tape. To
+ potential infinity is achieved by adding an appropriate blank or occupied cell
+ whenever the head goes over the ``edge'' of the tape. To
make this formal we define five possible \emph{actions}
the Turing machine can perform:
@@ -263,8 +283,8 @@
\noindent
We slightly deviate
from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
- will become important when we formalise universal Turing
- machines later. Given a tape and an action, we can define the
+ will become important when we formalise halting computations and also universal Turing
+ machines. Given a tape and an action, we can define the
following tape updating function:
\begin{center}
@@ -290,8 +310,8 @@
to test if the left-list @{term l} is empty; if yes, then we just prepend a
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 clause for a right move action. The @{term Nop} operation
- leaves the the tape unchanged.
+ in the fourth clause for a right move action. The @{term Nop} operation
+ leaves the the tape unchanged (last clause).
Note that our treatment of the tape is rather ``unsymmetric''---we
have the convention that the head of the right-list is where the
@@ -313,27 +333,28 @@
Next we need to define the \emph{states} of a Turing machine. Given
how little is usually said about how to represent them in informal
- presentations, it might be surprising that in a theorem prover we have
- to select carfully a representation. If we use the naive representation
- where a Turing machine consists of a finite set of states, then we
- will have difficulties composing two Turing machines: we
- would need to combine two finite sets of states, possibly
- renaming states apart whenever both machines share
- states.\footnote{The usual disjoint union operation does not preserve types, unfortunately.} This
- renaming can be quite cumbersome to reason about. Therefore we made
- the choice of representing a state by a natural number and the states
- of a Turing machine will always consist of the initial segment
- of natural numbers starting from @{text 0} up to the number of states
- of the machine. In doing so we can compose
- two Turing machine by ``shifting'' the states of one by an appropriate
- amount to a higher segment and adjust some ``next states'' in the other.
+ presentations, it might be surprising that in a theorem prover we
+ have to select carfully a representation. If we use the naive
+ representation where a Turing machine consists of a finite set of
+ states, then we will have difficulties composing two Turing
+ machines: we would need to combine two finite sets of states,
+ possibly renaming states apart whenever both machines share
+ states.\footnote{The usual disjoint union operation in Isabelle/HOL
+ cannot be used as it does not preserve types.} This renaming can be
+ quite cumbersome to reason about. Therefore we made the choice of
+ representing a state by a natural number and the states of a Turing
+ machine will always consist of the initial segment of natural
+ numbers starting from @{text 0} up to the number of states of the
+ machine. In doing so we can compose two Turing machine by
+ shifting the states of one by an appropriate amount to a higher
+ segment and adjusting some ``next states'' in the other.
An \emph{instruction} @{term i} of a Turing machine is a pair consisting of
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
- machine is then a list of such pairs. Using the following Turing machine
- program (consisting of four instructions) as an example
+ machine is then a list of such pairs. Using as an example the following Turing machine
+ program, which consists of four instructions
- \begin{center}
+ \begin{equation}
\begin{tikzpicture}
\node [anchor=base] at (0,0) {@{thm dither_def}};
\node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
@@ -341,20 +362,27 @@
\node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
\node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
\end{tikzpicture}
- \end{center}
+ \label{dither}
+ \end{equation}
\noindent
- the reader can see we have organised our Turing machine programs so
- that segments of two belong to a state. The first component
- of the segment determines what action should be taken and which next
- state should be transitioned to in case the head reads a @{term Bk};
+ the reader can see we have organised our Turing machine programs so
+ that segments of two belong to a state. The first component of the
+ segment determines what action should be taken and which next state
+ should be transitioned to in case the head reads a @{term Bk};
similarly the second component determines what should be done in
- case of reading @{term Oc}. We have the convention that the
- first state is always the \emph{starting state} of the Turing machine.
- The 0-state is special in that it will be used as the \emph{halting state}.
- There are no instructions for the 0-state, but it will always
- perform a @{term Nop}-operation and remain in the 0-state.
-
+ case of reading @{term Oc}. We have the convention that the first
+ state is always the \emph{starting state} of the Turing machine.
+ The zeroth 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
+ representation for programs, because when constructing a universal
+ Turing machine, we need to define a coding function for programs.
+ This can be easily done for our programs-as-lists, but is more
+ difficult for the functions used by Asperti and Ricciotti.
+
Given a program @{term p}, a state
and the cell being read by the head, we need to fetch
the corresponding instruction from the program. For this we define
@@ -376,15 +404,16 @@
\noindent
In this definition the function @{term nth_of} returns the @{text n}th element
- from a list, if it exists (@{term Some}-case), or if it does not, it
- returns the default action @{term Nop} and the default state 0
+ from a list, provided it exists (@{term Some}-case), or if it does not, it
+ returns the default action @{term Nop} and the default state @{text 0}
(@{term None}-case). In doing so we slightly deviate from the description
in \cite{Boolos87}: if their Turing machines transition to a non-existing
state, then the computation is halted. We will transition in such cases
- to the 0th state with the @{term Nop}-action. However, with introducing the
- notion of \emph{well-formed} Turing machine programs we will exclude such
- cases. A program @{term p} is said to be well-formed if it satisfies
- the following three properties
+ to the @{text 0}-state. However, with introducing the
+ notion of \emph{well-formed} Turing machine programs we will later exclude such
+ cases and make the @{text 0}-state the only ``halting state''. A program
+ @{term p} is said to be well-formed if it satisfies
+ the following three properties:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -398,14 +427,14 @@
The first says that @{text p} must have at least an instruction for the starting
state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
state, and the third that every next-state is one of the states mentioned in
- the program or being the 0-state.
+ the program or being the @{text 0}-state.
A \emph{configuration} @{term c} of a Turing machine is a state together with
a tape. This is written as @{text "(s, (l, r))"}. If we have a
configuration and a program, we can calculate
- what the next configuration is by fetching the appropriate next state
- and action from the program, and updating the state and tape accordingly.
- This single step of execution is defined as the function @{term tstep}:
+ what the next configuration is by fetching the appropriate action and next state
+ from the program, and by updating the state and tape accordingly.
+ This single step of execution is defined as the function @{term tstep}
\begin{center}
\begin{tabular}{l}
@@ -416,10 +445,12 @@
\end{center}
\noindent
- It is impossible in Isabelle/HOL to lift this function realising
+ where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
+ empty it returns @{term Bk}.
+ It is impossible in Isabelle/HOL to lift the @{term step}-function realising
a general evaluation function for Turing machines. The reason is that functions in HOL-based
provers need to be terminating, and clearly there are Turing machine
- programs which are not. We can however define an evaluation
+ programs that are not. We can however define an evaluation
function so that it performs exactly @{text n} steps:
\begin{center}
@@ -431,27 +462,50 @@
\noindent
Recall our definition of @{term fetch} with the default value for
- the 0th state. In case a Turing program takes in \cite{Boolos87} less
- then @{text n} steps before it halts, then in our setting the evaluation
- does not halt, but rather transitions to the 0th state and remain there
- performing @{text Nop}-actions.
+ the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less
+ then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
+ does not actually halt, but rather transitions to the @{text 0}-state and
+ remains there performing @{text Nop}-actions until @{text n} is reached.
Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
- @{term p} halts generating an output tape @{text "(l\<^isub>o,r\<^isub>o)"}:
+ @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
\begin{center}
\begin{tabular}{l}
- @{term "halt p (l\<^isub>i,r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
+ @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
\hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
\end{tabular}
\end{center}
\noindent
- where 1 stands for the starting state and 0 for the halting state, or
- in our settin it should better be called the final state.
+ where @{text 1} stands for the starting state and @{text 0} for our final state.
+ A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
+
+ \begin{center}
+ @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
+ \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
+ \end{center}
+
+ \noindent
Later on we need to consider specific Turing machines that
start with a tape in standard form and halt the computation
- in standard form. By this we mean
+ in standard form. To define a tape in standard form, it is
+ useful to have an operation @{term "tape_of_nat_list DUMMY"} that
+ translates
+ lists of natural numbers into tapes.
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(1)}\\
+ @{thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(2)}\\
+ @{thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(3)}\\
+ \end{tabular}
+ \end{center}
+
+
+
+
+ By this we mean
\begin{center}
@{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
@@ -469,8 +523,14 @@
clustered on the output tape).
Before we can prove the undecidability of the halting problem for Turing machines,
- we have to define how to compose them. Given our setup, this is relatively straightforward,
- if slightly fiddly.
+ we have to define how to compose Turing machines. Given our setup, this is relatively
+ straightforward, if slightly fiddly.
+
+ \begin{center}
+ @{thm tshift_def2}
+ \end{center}
+
+ (* HERE *)
shift and change of a p
--- a/abacus.thy Fri Jan 11 13:18:33 2013 +0000
+++ b/abacus.thy Sat Jan 12 01:05:01 2013 +0000
@@ -177,6 +177,7 @@
(L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
(L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]"
+(* FIXME: doubly defined
text {*
@{text "tshift tm off"} shifts @{text "tm"} by offset @{text "off"}, leaving
instructions concerning state @{text "0"} unchanged, because state @{text "0"}
@@ -188,6 +189,7 @@
"tshift tp off = (map (\<lambda> (action, state).
(action, (if state = 0 then 0
else state + off))) tp)"
+*)
text {*
@{text "tinc ss n"} returns the TM which simulates the execution of