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-- |
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
44e9d0c24fbc
added
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
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
9
diff
changeset
|
38 |
of computability theory, |
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
9
diff
changeset
|
40 |
formalisation is a clever infrastructure for reducing |
44e9d0c24fbc
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
9
diff
changeset
|
41 |
$\lambda$-terms. He also established the computational equivalence |
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
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
44e9d0c24fbc
added
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 |
44e9d0c24fbc
added
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
44e9d0c24fbc
added
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
44e9d0c24fbc
added
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
965df91a24bc
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
8
diff
changeset
|
134 |
|
965df91a24bc
more
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
44e9d0c24fbc
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
9
diff
changeset
|
159 |
|
9
965df91a24bc
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
8
diff
changeset
|
160 |
*} |
965df91a24bc
more
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
f7896d90aa19
more
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
f7896d90aa19
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
6
diff
changeset
|
167 |
|
f7896d90aa19
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
6
diff
changeset
|
168 |
text {* |
f7896d90aa19
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
6
diff
changeset
|
169 |
Used in texture mapings - graphics |
f7896d90aa19
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
6
diff
changeset
|
170 |
*} |
f7896d90aa19
more
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
6
diff
changeset
|
171 |
|
f7896d90aa19
more
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 |
(*>*) |