Paper.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 09 Jan 2013 13:35:09 +0000
changeset 17 66cebc19ef18
parent 16 a959398693b5
child 18 a961c2e4dcea
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
(*<*)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
theory Paper
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
imports UTM
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
begin
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
declare [[show_question_marks = false]]
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
(*>*)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
section {* Introduction *}
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
text {*
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
8
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    13
\noindent
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    14
We formalised in earlier work the correctness proofs for two
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    15
algorithms in Isabelle/HOL---one about type-checking in
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    16
LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    17
in access control~\cite{WuZhangUrban12}.  The formalisations
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    18
uncovered a gap in the informal correctness proof of the former and
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    19
made us realise that important details were left out in the informal
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    20
model for the latter. However, in both cases we were unable to
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    21
formalise in Isabelle/HOL computability arguments about the
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    22
algorithms. The reason is that both algorithms are formulated in terms
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    23
of inductive predicates. Suppose @{text "P"} stands for one such
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    24
predicate.  Decidability of @{text P} usually amounts to showing
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    25
whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    26
in Isabelle/HOL, since it is a theorem prover based on classical logic
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    27
where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    28
is always provable no matter whether @{text P} is constructed by
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    29
computable means. The same problem would arise if we had formulated
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    30
the algorithms as recursive functions, because internally in
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    31
Isabelle/HOL, like in all HOL-based theorem provers, functions are
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    32
represented as inductively defined predicates too.
8
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    33
12
dd400b5797e1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 10
diff changeset
    34
The only satisfying way out of this problem in a theorem prover based on classical
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    35
logic is to formalise a theory of computability. Norrish provided such
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    36
a formalisation for the HOL4 theorem prover. He choose the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    37
$\lambda$-calculus as the starting point for his formalisation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    38
of computability theory,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    39
because of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    40
formalisation is a clever infrastructure for reducing
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    41
$\lambda$-terms. He also established the computational equivalence
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    42
between the $\lambda$-calculus and recursive functions.  Nevertheless he
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    43
concluded that it would be ``appealing'' to have formalisations for more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    44
operational models of computations, such as Turing machines or register
12
dd400b5797e1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 10
diff changeset
    45
machines.  One reason is that many proofs in the literature use 
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    46
them.  He noted however that in the context of theorem provers
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
    47
\cite[Page 310]{Norrish11}:
8
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    48
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    49
\begin{quote}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    50
\it``If register machines are unappealing because of their 
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    51
general fiddliness, Turing machines are an even more 
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    52
daunting prospect.''
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    53
\end{quote}
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    54
c216ae455c90 more on the paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 7
diff changeset
    55
\noindent
13
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    56
In this paper we took on this daunting prospect and provide a
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    57
formalisation of Turing machines, as well as abacus machines (a kind
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    58
of register machines) and recursive functions. To see the difficulties
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    59
involved with this work, one has to understand that interactive
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    60
theorem provers, like Isabelle/HOL, are at their best when the
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    61
data-structures at hand are ``structurally'' defined, like lists,
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    62
natural numbers, regular expressions, etc. Such data-structures come
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    63
with convenient reasoning infrastructures (for example induction
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    64
principles, recursion combinators and so on).  But this is \emph{not}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    65
the case with Turing machines (and also not with register machines):
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    66
underlying their definition is a set of states together with a
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    67
transition function, both of which are not structurally defined.  This
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    68
means we have to implement our own reasoning infrastructure in order
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    69
to prove properties about them. This leads to annoyingly fiddly
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    70
formalisations.  We noticed first the difference between both,
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    71
structural and non-structural, ``worlds'' when formalising the
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    72
Myhill-Nerode theorem, where regular expressions fared much better
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    73
than automata \cite{WuZhangUrban11}.  However, with Turing machines
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    74
there seems to be no alternative if one wants to formalise the great
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    75
many proofs from the literature that use them.  We will analyse one
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    76
example---undecidability of Wang tilings---in Section~\ref{Wang}. The
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    77
standard proof of this property uses the notion of \emph{universal
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    78
Turing machines}.
12
dd400b5797e1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 10
diff changeset
    79
13
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    80
We are not the first who formalised Turing machines in a theorem
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
    81
prover: we are aware of the preliminary work by Asperti and Ricciotti
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    82
\cite{AspertiRicciotti12}. They describe a complete formalisation of
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    83
Turing machines in the Matita theorem prover, including a universal
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    84
Turing machine. They report that the informal proofs from which they
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    85
started are not ``sufficiently accurate to be directly used as a
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    86
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    87
our formalisation we followed the proofs from the textbook
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    88
\cite{Boolos87} and found that the description there is quite
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    89
detailed. Some details are left out however: for example, it is only
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    90
shown how the universal Turing machine is constructed for Turing
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    91
machines computing unary functions. We had to figure out a way to
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    92
generalize this result to $n$-ary functions. Similarly, when compiling
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    93
recursive functions to abacus machines, the textbook again only shows
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    94
how it can be done for 2- and 3-ary functions, but in the
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    95
formalisation we need arbitrary functions. But the general ideas for
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    96
how to do this are clear enough in \cite{Boolos87}. However, one
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    97
aspect that is completely left out from the informal description in
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    98
\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
    99
machines are correct. We will introduce Hoare-style proof rules
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   100
which help us with such correctness arguments of Turing machines.
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
   101
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   102
The main difference between our formalisation and the one by Asperti
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   103
and Ricciotti is that their universal Turing machine uses a different
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   104
alphabet than the machines it simulates. They write \cite[Page
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   105
23]{AspertiRicciotti12}:
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
   106
15
90bc8cccc218 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 13
diff changeset
   107
\begin{quote}\it
13
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
   108
``In particular, the fact that the universal machine operates with a
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
   109
different alphabet with respect to the machines it simulates is
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
   110
annoying.'' 
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
   111
\end{quote}
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
15
90bc8cccc218 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 13
diff changeset
   113
\noindent
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   114
In this paper we follow the approach by Boolos et al \cite{Boolos87},
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   115
which goes back to Post \cite{Post36}, where all Turing machines
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   116
operate on tapes that contain only blank or filled cells (represented 
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   117
by @{term Bk} and @{term Oc}, respectively, in our
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   118
formalisation). Traditionally the content of a cell can be any
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   119
character from a finite alphabet. Although computationally
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   120
equivalennt, the more restrictive notion of Turing machines make
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   121
the reasoning more uniform. Unfortunately, it also makes it
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   122
harder to design programs for Turing machines. Therefore
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   123
in order to construct a \emph{universal Turing machine} we follow
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   124
the proof in \cite{Boolos87} by relating abacus machines to
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   125
turing machines and in turn recursive functions to abacus machines. 
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   127
\medskip
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
\noindent
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
{\bf Contributions:} 
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
*}
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   133
section {* Turing Machines *}
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 8
diff changeset
   134
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 8
diff changeset
   135
text {*
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   136
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   137
  Tapes
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   138
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   139
  %\begin{center}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   140
  %\begin{tikzpicture}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   141
  %%
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   142
  %\end{tikzpicture}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   143
  %\end{center}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   144
  
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   145
  An action is defined as 
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   146
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   147
  \begin{center}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   148
  \begin{tabular}{rcll}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   149
  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   150
  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   151
  & $\mid$ & @{term L} & move left\\
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   152
  & $\mid$ & @{term R} & move right\\
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   153
  & $\mid$ & @{term Nop} & do nothing\\
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   154
  \end{tabular}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   155
  \end{center}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   156
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   157
  For showing the undecidability of the halting problem, we need to consider
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   158
  two specific Turing machines.
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 9
diff changeset
   159
  
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 8
diff changeset
   160
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 8
diff changeset
   161
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   162
section {* Abacus Machines *}
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   163
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   164
section {* Recursive Functions *}
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   165
13
a7ec585d7f20 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 12
diff changeset
   166
section {* Wang Tiles\label{Wang} *}
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   167
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   168
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   169
  Used in texture mapings - graphics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   170
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   171
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 6
diff changeset
   172
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
section {* Related Work *}
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
text {*
17
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   176
  The most closely related work is by Norrish \cite{Norrish11}, and Asperti and 
66cebc19ef18 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 16
diff changeset
   177
  Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on 
6
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
  lambda-terms. For this he introduced a clever rewriting technology
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
  based on combinators and de-Bruijn indices for
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
  rewriting modulo $\beta$-equivalence (to keep it manageable)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
*}
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
(*
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
Questions:
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   187
Can this be done: Ackerman function is not primitive 
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   188
recursive (Nora Szasz)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   189
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
Tape is represented as two lists (finite - usually infinite tape)?
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
*)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
(*<*)
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
end
50880fcda34d added paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
(*>*)