equal
deleted
inserted
replaced
60 and relate them to abacus machines and recursive functions. We ``tie |
60 and relate them to abacus machines and recursive functions. We ``tie |
61 the know'' between these three computational models by formalising a |
61 the know'' between these three computational models by formalising a |
62 universal function and obtaining from it a universal Turing machine by |
62 universal function and obtaining from it a universal Turing machine by |
63 our verified translation from recursive functions to abacus programs |
63 our verified translation from recursive functions to abacus programs |
64 and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us |
64 and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us |
65 to reason about Turing machine and abacus programs. Our theory can be |
65 to reason about concrete Turing machine and abacus programs. |
66 used to formalise other computability results. |
66 %Our theory can be |
|
67 %used to formalise other computability results. |
67 %We give one example about the computational equivalence of |
68 %We give one example about the computational equivalence of |
68 %single-sided Turing machines. |
69 %single-sided Turing machines. |
69 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
70 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses |
70 %the notion of a universal Turing machine.} |
71 %the notion of a universal Turing machine.} |
71 \end{abstract} |
72 \end{abstract} |