6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory Paper
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
imports UTM
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
hide_const (open) s
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
"update p a == new_tape a p"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
lemma fetch_def2:
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
shows "fetch p 0 b == (Nop, 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
and "fetch p (Suc s) Bk ==
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
(case nth_of p (2 * s) of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
Some i \<Rightarrow> i
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
| None \<Rightarrow> (Nop, 0))"
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
and "fetch p (Suc s) Oc ==
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
(case nth_of p ((2 * s) + 1) of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
Some i \<Rightarrow> i
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
| None \<Rightarrow> (Nop, 0))"
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
apply -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
apply(rule_tac [!] eq_reflection)
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
by (auto split: block.splits simp add: fetch.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
lemma new_tape_def2:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
shows "new_tape W0 (l, r) == (l, Bk#(tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
and "new_tape W1 (l, r) == (l, Oc#(tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
and "new_tape L (l, r) ==
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
(if l = [] then ([], Bk#r) else (tl l, (hd l) # r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
and "new_tape R (l, r) ==
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
(if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
and "new_tape Nop (l, r) == (l, r)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
apply -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
apply(rule_tac [!] eq_reflection)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
apply(auto split: taction.splits simp add: new_tape.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
lemma tstep_def2:
|
23
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
shows "tstep (s, l, []) p == (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
and "tstep (s, l, x#xs) p == (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
apply -
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
apply(rule_tac [!] eq_reflection)
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
by (auto split: prod.split list.split simp add: tstep.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
consts DUMMY::'a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
notation (latex output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
Cons ("_::_" [78,77] 73) and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
DUMMY ("\<^raw:\mbox{$\_$}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
declare [[show_question_marks = false]]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
section {* Introduction *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
We formalised in earlier work the correctness proofs for two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
algorithms in Isabelle/HOL---one about type-checking in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
in access control~\cite{WuZhangUrban12}. The formalisations
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
uncovered a gap in the informal correctness proof of the former and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
made us realise that important details were left out in the informal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
model for the latter. However, in both cases we were unable to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
formalise in Isabelle/HOL computability arguments about the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
algorithms. The reason is that both algorithms are formulated in terms
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
of inductive predicates. Suppose @{text "P"} stands for one such
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
predicate. Decidability of @{text P} usually amounts to showing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
in Isabelle/HOL, since it is a theorem prover based on classical logic
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
is always provable no matter whether @{text P} is constructed by
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
computable means. The same problem would arise if we had formulated
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
the algorithms as recursive functions, because internally in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
Isabelle/HOL, like in all HOL-based theorem provers, functions are
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
represented as inductively defined predicates too.
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
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>
diff
changeset
|
83 |
logic is to formalise a theory of computability. Norrish provided such
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
a formalisation for the HOL4 theorem prover. He choose the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
$\lambda$-calculus as the starting point for his formalisation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
of computability theory,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
formalisation is a clever infrastructure for reducing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
$\lambda$-terms. He also established the computational equivalence
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
between the $\lambda$-calculus and recursive functions. Nevertheless he
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
concluded that it would be ``appealing'' to have formalisations for more
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
operational models of computations, such as Turing machines or register
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
machines. One reason is that many proofs in the literature use
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
them. He noted however that in the context of theorem provers
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
\cite[Page 310]{Norrish11}:
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
\begin{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
\it``If register machines are unappealing because of their
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
general fiddliness, Turing machines are an even more
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
daunting prospect.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
\end{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
\noindent
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
In this paper we took on this daunting prospect and provide a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
formalisation of Turing machines, as well as abacus machines (a kind
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
of register machines) and recursive functions. To see the difficulties
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
involved with this work, one has to understand that interactive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
theorem provers, like Isabelle/HOL, are at their best when the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
data-structures at hand are ``structurally'' defined, like lists,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
natural numbers, regular expressions, etc. Such data-structures come
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
with convenient reasoning infrastructures (for example induction
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
principles, recursion combinators and so on). But this is \emph{not}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
the case with Turing machines (and also not with register machines):
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
underlying their definition is a set of states together with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
transition function, both of which are not structurally defined. This
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
means we have to implement our own reasoning infrastructure in order
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
to prove properties about them. This leads to annoyingly fiddly
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
formalisations. We noticed first the difference between both,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
structural and non-structural, ``worlds'' when formalising the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
Myhill-Nerode theorem, where regular expressions fared much better
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
than automata \cite{WuZhangUrban11}. However, with Turing machines
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
there seems to be no alternative if one wants to formalise the great
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
many proofs from the literature that use them. We will analyse one
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
125 |
standard proof of this property uses the notion of \emph{universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
Turing machines}.
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
We are not the first who formalised Turing machines in a theorem
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
prover: we are aware of the preliminary work by Asperti and Ricciotti
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
\cite{AspertiRicciotti12}. They describe a complete formalisation of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
Turing machines in the Matita theorem prover, including a universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
Turing machine. They report that the informal proofs from which they
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
started are not ``sufficiently accurate to be directly useable as a
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
our formalisation we followed mainly the proofs from the textbook
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
\cite{Boolos87} and found that the description there is quite
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
detailed. Some details are left out however: for example, it is only
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
shown how the universal Turing machine is constructed for Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
machines computing unary functions. We had to figure out a way to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
generalize this result to $n$-ary functions. Similarly, when compiling
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
recursive functions to abacus machines, the textbook again only shows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
how it can be done for 2- and 3-ary functions, but in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
formalisation we need arbitrary functions. But the general ideas for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
how to do this are clear enough in \cite{Boolos87}. However, one
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
aspect that is completely left out from the informal description in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
machines are correct. We will introduce Hoare-style proof rules
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
which help us with such correctness arguments of Turing machines.
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
The main difference between our formalisation and the one by Asperti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
and Ricciotti is that their universal Turing machine uses a different
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
alphabet than the machines it simulates. They write \cite[Page
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
23]{AspertiRicciotti12}:
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
\begin{quote}\it
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
``In particular, the fact that the universal machine operates with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
different alphabet with respect to the machines it simulates is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
annoying.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
\end{quote}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
\noindent
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
In this paper we follow the approach by Boolos et al \cite{Boolos87},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
which goes back to Post \cite{Post36}, where all Turing machines
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
operate on tapes that contain only \emph{blank} or \emph{occupied} cells
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
(represented by @{term Bk} and @{term Oc}, respectively, in our
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
formalisation). Traditionally the content of a cell can be any
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
character from a finite alphabet. Although computationally equivalent,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
the more restrictive notion of Turing machines in \cite{Boolos87} makes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
the reasoning more uniform. In addition some proofs \emph{about} Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
machines will be simpler. The reason is that one often needs to encode
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
Turing machines---consequently if the Turing machines are simpler, then the coding
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
functions are simpler too. Unfortunately, the restrictiveness also makes
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
it harder to design programs for these Turing machines. Therefore in order
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
to construct a \emph{universal Turing machine} we follow the proof in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
\cite{Boolos87} by relating abacus machines to Turing machines and in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
turn recursive functions to abacus machines. The universal Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
177 |
machine can then be constructed as a recursive function.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
\smallskip
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
{\bf Contributions:}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
section {* Turing Machines *}
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
text {* \noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
Turing machines can be thought of as having a read-write-unit
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
189 |
``gliding'' over a potentially infinite tape. Boolos et
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
190 |
al~\cite{Boolos87} only consider tapes with cells being either blank
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
or occupied, which we represent by a datatype having two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
constructors, namely @{text Bk} and @{text Oc}. One way to
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
represent such tapes is to use a pair of lists, written @{term "(l,
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
r)"}, where @{term l} stands for the tape on the left-hand side of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
read-write-unit and @{term r} for the tape on the right-hand side. We have the
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
convention that the head, written @{term hd}, of the right-list is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
the cell on which the read-write-unit currently operates. This can
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
be pictured as follows:
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
\draw[very thick] (-3.0,0) -- ( 3.0,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
\draw (-0.25,0.8) -- (-0.25,-0.8);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
\node [anchor=base] at (-0.8,-0.5) {\small left list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
\node [anchor=base] at (0.35,-0.5) {\small right list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
\node [anchor=base] at (0.1,0.7) {\small head};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
\node [anchor=base] at (-2.2,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
\node [anchor=base] at ( 2.3,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
\end{center}
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
Note that by using lists each side of the tape is only finite. The
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
potential infinity is achieved by adding an appropriate blank cell
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
whenever the read-write unit goes over the ``edge'' of the tape. To
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
make this formal we define five possible \emph{actions}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
the Turing machine can perform:
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
\begin{tabular}{rcll}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
@{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
& $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
& $\mid$ & @{term L} & move left\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
& $\mid$ & @{term R} & move right\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
& $\mid$ & @{term Nop} & do-nothing operation\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
242 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
243 |
\noindent
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
244 |
We slightly deviate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
245 |
from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
246 |
will become important when we formalise universal Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
machines later. Given a tape and an action, we can define the
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
following updating function:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
249 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
250 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
@{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
253 |
@{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
254 |
@{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
255 |
\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
@{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
@{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
The first two clauses replace the head of the right-list
|
21
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
with new a @{term Bk} or @{term Oc}, repsectively. To see that
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
these tow clauses make sense in case where @{text r} is the empty
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
list, one has to know that the tail function, @{term tl}, is defined
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
such that @{term "tl [] == []"} holds. The third clause
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
implements the move of the read-write unit one step to the left: we need
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
to test if the left-list @{term l} is empty; if yes, then we just prepend a
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
blank cell to the right-list; otherwise we have to remove the
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
head from the left-list and prepend it to the right-list. Similarly
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
in the clause for a right move action. The @{term Nop} operation
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
leaves the the tape unchanged.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
Note that our treatment of the tape is rather ``unsymmetric''---we
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
276 |
have the convention that the head of the right-list is where the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
read-write unit is currently positioned. Asperti and Ricciotti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
\cite{AspertiRicciotti12} also consider such a representation, but
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
279 |
dismiss it as it complicates their definition for \emph{tape
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
280 |
equality}. The reason is that moving the read-write unit one step to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
281 |
the left and then back to the right might change the tape (in case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
282 |
of going over the ``edge''). Therefore they distinguish four types
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
of tapes: one where the tape is empty; another where the read-write
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
unit is on the left edge, respectively right edge, and in the middle
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
of the tape. The reading, writing and moving of the tape is then
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
defined in terms of these four cases. In this way they can keep the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
tape in a ``normalised'' form, and thus making a left-move followed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
by a right-move being the identity on tapes. Since we are not using
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
the notion of tape equality, we can get away with the unsymmetric
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
definition above and by using the @{term update} function
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
291 |
cover uniformely all cases including the corner cases.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
Next we need to define the \emph{states} of a Turing machine. Given
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
how little is usually said about how to represent them in informal
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
presentaions, it might be surprising that in a theorem prover we have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
to select carfully a representation. If we use the naive representation
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
where a Turing machine consists of a finite set of states, then we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
298 |
will have difficulties composing two Turing machines. In this case we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
299 |
would need to combine two finite sets of states, possibly requiring
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
renaming states apart whenever both machines share states. This
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
renaming can be quite cumbersome to reason about. Therefore we made
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
the choice of representing a state by a natural number and the states
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
303 |
of a Turing machine will always consist of the initial segment
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
304 |
of natural numbers starting from @{text 0} up to number of states
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
305 |
of the machine minus @{text 1}. In doing so we can compose
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
two Turing machine by ``shifting'' the states of one by an appropriate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
307 |
amount to a higher segment.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
308 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
An \emph{instruction} of a Turing machine is a pair consisting of a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
310 |
natural number (the next state) and an action. A \emph{program} of a Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
machine is then a list of such pairs. Given a program @{term p}, a state
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
312 |
and the cell being read by the read-write unit, we need to fetch
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
the corresponding instruction from the program. For this we define
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
314 |
the function @{term fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
317 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
\multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
@{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
\multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
322 |
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
@{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
324 |
\multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
start state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
331 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
What is tinres? What is it used for?
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
@{thm dither_def}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
337 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
339 |
A \emph{configuration} @{term c} of a Turing machine is a state together with
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
a tape. If we have a configuration and a program, we can calculate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
what the next configuration is by fetching the appropriate next state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
342 |
and action from the program. Such a single step of execution can be defined as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
@{thm tstep_def2(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
346 |
@{thm tstep_def2(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
\end{center}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
For showing the undecidability of the halting problem, we need to consider
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
two specific Turing machines.
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
|
19
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
No evaluator in HOL, because of totality.
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
section {* Abacus Machines *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
section {* Recursive Functions *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
section {* Wang Tiles\label{Wang} *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
Used in texture mapings - graphics
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
367 |
section {* Related Work *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
368 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
369 |
text {*
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
The most closely related work is by Norrish \cite{Norrish11}, and Asperti and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
372 |
lambda-terms. For this he introduced a clever rewriting technology
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
373 |
based on combinators and de-Bruijn indices for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
374 |
rewriting modulo $\beta$-equivalence (to keep it manageable)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
375 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
376 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
377 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
378 |
(*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
379 |
Questions:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
380 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
381 |
Can this be done: Ackerman function is not primitive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
382 |
recursive (Nora Szasz)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
383 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
384 |
Tape is represented as two lists (finite - usually infinite tape)?
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
385 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
386 |
*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
387 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
388 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
389 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
390 |
end
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
391 |
(*>*) |