equal
deleted
inserted
replaced
56 %predicate is either true or false because of the law of excluded |
56 %predicate is either true or false because of the law of excluded |
57 %middle. The only way to reason about computability in a classical |
57 %middle. The only way to reason about computability in a classical |
58 %theorem prover is to formalise a concrete model of computation. |
58 %theorem prover is to formalise a concrete model of computation. |
59 Following the textbook by Boolos et al, we formalise Turing machines |
59 Following the textbook by Boolos et al, we formalise Turing machines |
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 knot'' 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 concrete Turing machine and abacus programs. |
65 to reason about concrete Turing machine and abacus programs. |
66 %Our theory can be |
66 %Our theory can be |