1 (*<*)

     1 (*<*)

     2 theory Paper

     2 theory Paper

     3 imports "../thys/UTM" "../thys/Abacus_Defs"

     3 imports "../thys/UTM" "../thys/Abacus_Defs"

     4 begin

     4 begin

     5 

     5 

     7 hide_const (open) s 

     9 hide_const (open) s 

     8 

    10 

     9 

    11 

    10 

    12 

    11 hide_const (open) Divides.adjust

    13 hide_const (open) Divides.adjust

    67   steps0 ("steps") and

    69   steps0 ("steps") and

    68   adjust0 ("adjust") and

    70   adjust0 ("adjust") and

    69   exponent ("_\<^bsup>_\<^esup>") and

    71   exponent ("_\<^bsup>_\<^esup>") and

    70   tcopy ("copy") and 

    72   tcopy ("copy") and 

    71   tape_of ("\<langle>_\<rangle>") and 

    73   tape_of ("\<langle>_\<rangle>") and 

    73   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    75   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    74   inv_begin0 ("I\<^isub>0") and

    76   inv_begin0 ("I\<^isub>0") and

    75   inv_begin1 ("I\<^isub>1") and

    77   inv_begin1 ("I\<^isub>1") and

    76   inv_begin2 ("I\<^isub>2") and

    78   inv_begin2 ("I\<^isub>2") and

    77   inv_begin3 ("I\<^isub>3") and

    79   inv_begin3 ("I\<^isub>3") and

   528   implements the move of the head one step to the left: we need

   530   implements the move of the head one step to the left: we need

   529   to test if the left-list @{term l} is empty; if yes, then we just prepend a 

   531   to test if the left-list @{term l} is empty; if yes, then we just prepend a 

   530   blank cell to the right list; otherwise we have to remove the

   532   blank cell to the right list; otherwise we have to remove the

   531   head from the left-list and prepend it to the right list. Similarly

   533   head from the left-list and prepend it to the right list. Similarly

   532   in the fourth clause for a right move action. The @{term Nop} operation

   534   in the fourth clause for a right move action. The @{term Nop} operation

   534 

   536 

   535   %Note that our treatment of the tape is rather ``unsymmetric''---we

   537   %Note that our treatment of the tape is rather ``unsymmetric''---we

   536   %have the convention that the head of the right list is where the

   538   %have the convention that the head of the right list is where the

   537   %head is currently positioned. Asperti and Ricciotti

   539   %head is currently positioned. Asperti and Ricciotti

   538   %\cite{AspertiRicciotti12} also considered such a representation, but

   540   %\cite{AspertiRicciotti12} also considered such a representation, but

   597   case of reading @{term Oc}. We have the convention that the first

   599   case of reading @{term Oc}. We have the convention that the first

   598   state is always the \emph{starting state} of the Turing machine.

   600   state is always the \emph{starting state} of the Turing machine.

   599   The @{text 0}-state is special in that it will be used as the

   601   The @{text 0}-state is special in that it will be used as the

   600   ``halting state''.  There are no instructions for the @{text

   602   ``halting state''.  There are no instructions for the @{text

   601   0}-state, but it will always perform a @{term Nop}-operation and

   603   0}-state, but it will always perform a @{term Nop}-operation and

   604   representation for Turing machine programs, because when constructing a universal

   606   representation for Turing machine programs, because when constructing a universal

   605   Turing machine, we need to define a coding function for programs.

   607   Turing machine, we need to define a coding function for programs.

   608 

   610 

   609   Given a program @{term p}, a state

   611   Given a program @{term p}, a state

   610   and the cell being scanned by the head, we need to fetch

   612   and the cell being scanned by the head, we need to fetch

   611   the corresponding instruction from the program. For this we define 

   613   the corresponding instruction from the program. For this we define 

   612   the function @{term fetch}

   614   the function @{term fetch}

   637   The first states that @{text p} must have at least an instruction for the starting 

   639   The first states that @{text p} must have at least an instruction for the starting 

   638   state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 

   640   state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 

   639   state, and the third that every next-state is one of the states mentioned in

   641   state, and the third that every next-state is one of the states mentioned in

   640   the program or being the @{text 0}-state.

   642   the program or being the @{text 0}-state.

   641 

   643 

   674   A \emph{configuration} @{term c} of a Turing machine is a state

   645   A \emph{configuration} @{term c} of a Turing machine is a state

   675   together with a tape. This is written as @{text "(s, (l, r))"}.  We

   646   together with a tape. This is written as @{text "(s, (l, r))"}.  We

   676   say a configuration \emph{is final} if @{term "s = (0::nat)"} and we

   647   say a configuration \emph{is final} if @{term "s = (0::nat)"} and we

   677   say a predicate @{text P} \emph{holds for} a configuration if @{text

   648   say a predicate @{text P} \emph{holds for} a configuration if @{text

   678   "P"} holds for the tape @{text "(l, r)"}.  If we have a configuration and a program, we can

   649   "P"} holds for the tape @{text "(l, r)"}.  If we have a configuration and a program, we can

   712   definition, say \cite{Boolos87}, less than @{text n} steps before it

   683   definition, say \cite{Boolos87}, less than @{text n} steps before it

   713   halts, then in our setting the @{term steps}-evaluation does not

   684   halts, then in our setting the @{term steps}-evaluation does not

   714   actually halt, but rather transitions to the @{text 0}-state (the

   685   actually halt, but rather transitions to the @{text 0}-state (the

   715   final state) and remains there performing @{text Nop}-actions until

   686   final state) and remains there performing @{text Nop}-actions until

   716   @{text n} is reached. 

   687   @{text n} is reached. 

   717   

   747   

   718   \begin{figure}[t]

   748   \begin{figure}[t]

   719   \begin{center}

   749   \begin{center}

   720   \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}

   750   \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}

   721   \begin{tabular}[t]{@ {}l@ {}}

   751   \begin{tabular}[t]{@ {}l@ {}}

   828   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}

   858   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}

   829   \label{copy}

   859   \label{copy}

   830   \end{figure}

   860   \end{figure}

   831 

   861 

   832 

   862 

   857 

   864 

   858   Before we can prove the undecidability of the halting problem for

   865   Before we can prove the undecidability of the halting problem for

   859   our Turing machines working on standard tapes, we have to analyse

   866   our Turing machines working on standard tapes, we have to analyse

   860   two concrete Turing machine programs and establish that they are

   867   two concrete Turing machine programs and establish that they are

   861   correct---that means they are ``doing what they are supposed to be

   868   correct---that means they are ``doing what they are supposed to be

  1059   \hline

  1066   \hline

  1060   \end{tabular}

  1067   \end{tabular}

  1061   \end{center}

  1068   \end{center}

  1062   \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of 

  1069   \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of 

  1063   @{term tcopy_begin}. Below, the invariants only for the starting and halting states of

  1070   @{term tcopy_begin}. Below, the invariants only for the starting and halting states of

  1065   @{term n} stands for the number

  1072   @{term n} stands for the number

  1066   of @{term Oc}s with which the Turing machine is started.}\label{invbegin}

  1073   of @{term Oc}s with which the Turing machine is started.}\label{invbegin}

  1067   \end{figure}

  1074   \end{figure}

  1068 

  1075 

  1069   \begin{center}

  1076   \begin{center}

  1390 

  1397 

  1391 text {*

  1398 text {*

  1392   The main point of recursive functions is that we can relatively 

  1399   The main point of recursive functions is that we can relatively 

  1393   easily construct a universal Turing machine via a universal 

  1400   easily construct a universal Turing machine via a universal 

  1394   function. This is different from Norrish \cite{Norrish11} who gives a universal 

  1401   function. This is different from Norrish \cite{Norrish11} who gives a universal 

  1396   \cite{AspertiRicciotti12} who construct a universal Turing machine

  1403   \cite{AspertiRicciotti12} who construct a universal Turing machine

  1397   directly, but for simulating Turing machines with a more restricted alphabet.

  1404   directly, but for simulating Turing machines with a more restricted alphabet.

  1398   Unlike Norrish \cite{Norrish11}, we need to represent recursive functions

  1405   Unlike Norrish \cite{Norrish11}, we need to represent recursive functions

  1399   ``deeply'' because we want to translate them to abacus programs.

  1406   ``deeply'' because we want to translate them to abacus programs.

  1400   Thus \emph{recursive functions} are defined as the datatype

  1407   Thus \emph{recursive functions} are defined as the datatype

  1512   unexpected since \cite{Boolos87} is a classic textbook which has

  1519   unexpected since \cite{Boolos87} is a classic textbook which has

  1513   undergone several editions (we used the fifth edition; the material 

  1520   undergone several editions (we used the fifth edition; the material 

  1514   containing the inconsistency was introduced in the fourth edition

  1521   containing the inconsistency was introduced in the fourth edition

  1515   \cite{BoolosFourth}). The central

  1522   \cite{BoolosFourth}). The central

  1516   idea about Turing machines is that when started with standard tapes

  1523   idea about Turing machines is that when started with standard tapes

  1518   when they define the case when this function should \emph{not} return a

  1525   when they define the case when this function should \emph{not} return a

  1519   result. Boolos at al write in Chapter 3, Page 32:

  1526   result. Boolos at al write in Chapter 3, Page 32:

  1520 

  1527 

  1521   \begin{quote}\it

  1528   \begin{quote}\it

  1522   ``If the function that is to be computed assigns no value to the arguments that 

  1529   ``If the function that is to be computed assigns no value to the arguments that 

  1536   \noindent

  1543   \noindent

  1537   where @{text "stat(conf(m, x, t))"} computes the current state of the

  1544   where @{text "stat(conf(m, x, t))"} computes the current state of the

  1538   simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}

  1545   simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}

  1539   if the tape content is non-standard. If either one evaluates to

  1546   if the tape content is non-standard. If either one evaluates to

  1540   something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of 

  1547   something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of 

  1542   in terms of @{text stdh} for computing the steps the Turing machine needs to

  1549   in terms of @{text stdh} for computing the steps the Turing machine needs to

  1543   execute before it halts (in case it halts at all). According to this definition, the simulated

  1550   execute before it halts (in case it halts at all). According to this definition, the simulated

  1544   Turing machine will continue to run after entering the @{text 0}-state

  1551   Turing machine will continue to run after entering the @{text 0}-state

  1545   with a non-standard tape. The consequence of this inconsistency is

  1552   with a non-standard tape. The consequence of this inconsistency is

  1546   that there exist Turing machines that given some arguments do not compute a value

  1553   that there exist Turing machines that given some arguments do not compute a value

  1560   @{term "counter_example \<equiv> [(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}

  1567   @{term "counter_example \<equiv> [(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}

  1561   \end{center}

  1568   \end{center}

  1562 

  1569 

  1563   \noindent

  1570   \noindent

  1564   If started with standard tape @{term "([], [Oc])"}, it halts with the

  1571   If started with standard tape @{term "([], [Oc])"}, it halts with the

  1566   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 

  1573   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 

  1568   We solve this inconsistency in our formalisation by

  1575   We solve this inconsistency in our formalisation by

  1569   setting up our definitions so that the @{text counter_example} Turing machine does not 

  1576   setting up our definitions so that the @{text counter_example} Turing machine does not 

  1570   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 

  1577   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 

  1571   This solution implements essentially the definition in Chapter 3; it  

  1578   This solution implements essentially the definition in Chapter 3; it  

  1572   differs from the definition in Chapter 8, where perplexingly the instruction 

  1579   differs from the definition in Chapter 8, where perplexingly the instruction 

  1639   computability because in Isabelle/HOL we cannot represent the

  1646   computability because in Isabelle/HOL we cannot represent the

  1640   decidability of a predicate @{text P}, say, as the formula @{term "P

  1647   decidability of a predicate @{text P}, say, as the formula @{term "P

  1641   \<or> \<not>P"}. For reasoning about computability we need to formalise a

  1648   \<or> \<not>P"}. For reasoning about computability we need to formalise a

  1642   concrete model of computations. We could have followed Norrish

  1649   concrete model of computations. We could have followed Norrish

  1643   \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,

  1650   \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,

  1647   (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).

  1656   (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).

  1648 

  1657 

  1649   We therefore have formalised Turing machines in the first place and the main

  1658   We therefore have formalised Turing machines in the first place and the main

  1650   computability results from Chapters 3 to 8 in the textbook by Boolos

  1659   computability results from Chapters 3 to 8 in the textbook by Boolos

  1651   et al \cite{Boolos87}.  For this we did not need to implement

  1660   et al \cite{Boolos87}.  For this we did not need to implement

  1722   programs where Hoare-style reasoning is sometimes possible, but

  1731   programs where Hoare-style reasoning is sometimes possible, but

  1723   sometimes it is not. In order to ease their reasoning, they

  1732   sometimes it is not. In order to ease their reasoning, they

  1724   introduced a more primitive specification logic, on which

  1733   introduced a more primitive specification logic, on which

  1725   Hoare-rules can be provided for special cases.  It remains to be

  1734   Hoare-rules can be provided for special cases.  It remains to be

  1726   seen whether their specification logic for assembly code can make it

  1735   seen whether their specification logic for assembly code can make it

  1728   attractive result, because Turing machine programs are very much

  1737   attractive result, because Turing machine programs are very much

  1729   like assembly programs and it would connect some very classic work on

  1738   like assembly programs and it would connect some very classic work on

  1730   Turing machines to very cutting-edge work on machine code

  1739   Turing machines to very cutting-edge work on machine code

  1731   verification. In order to try out such ideas, our formalisation provides the

  1740   verification. In order to try out such ideas, our formalisation provides the

  1732   ``playground''. The code of our formalisation is available from the

  1741   ``playground''. The code of our formalisation is available from the