--- a/Paper.thy Fri Jan 11 05:49:25 2013 +0000
+++ b/Paper.thy Fri Jan 11 08:47:02 2013 +0000
@@ -8,7 +8,6 @@
abbreviation
"update p a == new_tape a p"
-
lemma fetch_def2:
shows "fetch p 0 b == (Nop, 0)"
and "fetch p (Suc s) Bk ==
@@ -46,16 +45,29 @@
apply(rule_tac [!] eq_reflection)
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)"
+
+lemma haltP_def2:
+ "haltP p n = (\<exists>k l m.
+ halt p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
+unfolding haltP_def
+apply(auto)
+done
+
consts DUMMY::'a
notation (latex output)
Cons ("_::_" [78,77] 73) and
+ set ("") and
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
+ t_correct ("twf") and
tstep ("step") and
steps ("nsteps") and
abc_lm_v ("lookup") and
abc_lm_s ("set") and
+ haltP ("stdhalt") and
DUMMY ("\<^raw:\mbox{$\_$}>")
declare [[show_question_marks = false]]
@@ -271,8 +283,8 @@
The first two clauses replace the head of the right-list
with a new @{term Bk} or @{term Oc}, repsectively. To see that
these two clauses make sense in case where @{text r} is the empty
- list, one has to know that the tail function, @{term tl}, is in
- Isabelle/HOL defined
+ list, one has to know that the tail function, @{term tl}, is defined in
+ Isabelle/HOL
such that @{term "tl [] == []"} holds. The third clause
implements the move of the head one step to the left: we need
to test if the left-list @{term l} is empty; if yes, then we just prepend a
@@ -304,14 +316,15 @@
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. In this case we
- would need to combine two finite sets of states, possibly requiring
- renaming states apart whenever both machines share states. This
+ 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 number of states
- of the machine minus @{text 1}. In doing so we can compose
+ 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''.
@@ -334,14 +347,30 @@
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 read a @{term Bk};
+ 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 \emph{halting state}.
+ 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.
+ A \emph{well-formed} Turing machine program @{term p} is one that satisfies
+ the following three properties
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
+ & @{text "\<and>"} & @{term "iseven (length p)"}\\
+ & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ 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.
+
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
@@ -362,23 +391,35 @@
\end{center}
\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
+ (@{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.
A \emph{configuration} @{term c} of a Turing machine is a state together with
- a tape. This is written as the triple @{term "(s, l, r)"}. If we have a
+ 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. Such a single step of execution can be defined as
+ and action from the program, and updating the state and tape accordingly.
+ This single step of execution is defined as the function @{term tstep}:
\begin{center}
\begin{tabular}{l}
- @{thm (lhs) tstep_def2(1)} @{text "\<equiv>"}\\
+ @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\
\hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
\hspace{10mm}@{text "in (s', update (l, r) a)"}
\end{tabular}
\end{center}
- No evaluator in HOL, because of totality.
+ \noindent
+ It is impossible in Isabelle/HOL to lift this function in order to realise
+ 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 for which this does not hold. We can however define an evaluation
+ function so that it performs exactly @{text n}:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -387,9 +428,42 @@
\end{tabular}
\end{center}
- \emph{well-formedness} of a Turing program
+ \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.
+
+ 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)"}:
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{term "halt 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}
- programs halts
+ \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
+
+ \begin{center}
+ @{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ the Turing machine starts with a tape containg @{text n} @{term Oc}s
+ and the head pointing to the first one; the Turing machine
+ halts with a tape consisting of some @{term Bk}s, followed by a
+ ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
+ The head in the output is at the first @{term Oc}.
+ The intuitive meaning of this definition is to start Turing machine with a
+ tape corresponding to a value @{term n} and producing
+ a new tape corresponding to the value @{term l} (the number of @{term Oc}s
+ clustered on the tape).
shift and change of a p
@@ -406,7 +480,7 @@
measure for the copying TM, which we however omit.
- standard configuration
+
halting problem
*}