# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1357894022 0
# Node ID 2557d2946354452c03411fb5a9484d7b6d3002ed
# Parent  4ef4b25e29974666e5accb5d28673136d2a44b6d
update

diff -r 4ef4b25e2997 -r 2557d2946354 Paper.thy
--- 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
 *}
diff -r 4ef4b25e2997 -r 2557d2946354 paper.pdf
Binary file paper.pdf has changed