Reading list (this list may be updated during the course):
| Week | Texts |
|---|---|
| 1 | Bengt Nordström, Are all functions computable?. |
| Bengt Nordström, Enumerable sets and Hilbert’s hotel. | |
| C. A. R. Hoare and D. C. S. Allison, Incomputability, ACM Computing Surveys 4(3), 169–178, 1972. | |
| Optional, if you are interested in a careful discussion of the Church-Turing thesis: B. Jack Copeland, The Church-Turing Thesis, The Stanford Encyclopedia of Philosophy (Winter 2017 Edition). | |
| 2 | Bengt Nordström, Some mathematical preliminaries: sets, relations and functions. |
| Bengt Nordström, The primitive recursive functions. | |
| 3 | Bengt Nordström, The language χ. |
| Optional: An Agda formalisation of χ. | |
| 4 | Same as last week. |
| 5 | David Barker-Plummer, Turing Machines, The Stanford Encyclopedia of Philosophy (Winter 2016 Edition). |
| Section 9, up to but not including argument II, of the paper that introduced Turing machines: A. M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society s2-42 (1), 230–265, 1937. | |
| Optional: Mike Davey, A Turing Machine In the Classic Style, 2010. | |
| 6 | Same as last week. |
| Additionally, and optionally: Section 5.2—about the Post correspondence problem—of Michael Sipser’s book Introduction to the Theory of Computation (third international edition, 2013). | |
| 7 | Optional, if you are interested in the history of the subject: Neil Immerman, Computability and Complexity, The Stanford Encyclopedia of Philosophy (Spring 2016 Edition). |
| Optional, if you want to see an example of a (kind of) self-interpreter for a programming language in which all programs terminate: Matt Brown and Jens Palsberg: Breaking through the Normalization Barrier: A Self-Interpreter for F-omega, in POPL’16, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 5–17, 2016. (Note the discussion of terminology in Section 9.) | |
| Optional: In the lectures a universal Turing machine is discussed, but rather imprecisely. Several groups of people have formalised universal Turing machines. One example: Andrea Asperti and Wilmer Ricciotti, A formalization of multi-tape Turing machines, Theoretical Computer Science, 603, 23-42, 2015. | |
| Optional: The programming language LOOP is equivalent in power to PRF. | |
| Optional: Geoffrey K. Pullum, Scooping the Loop Snooper: A proof that the Halting Problem is undecidable, 2012. |
Some of the documents may be behind pay-walls, but it should be possible to access them from Chalmers’ computer network (and hopefully that of GU). If you are not on campus, then you can perhaps use a VPN.
Note that the texts above are not necessarily 100% correct. For instance, Figures 2, 3 and 4 in The primitive recursive functions do not quite agree. The texts are also not guaranteed to use consistent notation or definitions. Read carefully, and do not trust everything that you read.
You can optionally choose to read a standard text book on computability, such as Sipser’s Introduction to the Theory of Computation, or Hopcroft, Motwani and Ullman’s Introduction to Automata Theory, Languages, and Computation. Note, however, that large parts of those two books are not covered in this course, and that the course covers topics that are not included in the books.