Part I: Computation
This page contains all the information specific to Part I.
Schedule
This part will follow a route from logic to computability and back again:
- We start by introducing two logical theories of arithmetic, True Arithmetic and Presburger Arithmetic.
- We will show that Presburger Arithmetic is decidable (can be solved by an algorithm), using an algorithm that represents the truth of formulas as finite automata.
- In order to show that True Arithmetic is undecidable, we propose a formal definition of algorithm: the Turing Machine.
- We will argue that Turing Machines can express any conceivable algorithm.
- We will argue that many natural and interesting problems simply cannot be solved by any Turing Machine, and therefore cannot be solved by any algorithm.
- We will argue that True Arithmetic cannot be solved by any Turing Machine and hence is undecidable.
| Week | Lecture 1 | Lecture 2 | Problem Sheet | Lecture 3 |
|---|---|---|---|---|
| Week 1 | Introduction 1 Informal introduction to the themes of the unit. 2 Informal introduction to the logical theories we will be studying 3 Prerequesites and fixing notation for strings and sets |
First-Order Theories of Arithmetic 1 The syntax of first-order arithmetic. 2 Satisfying assignments and arithmetical definability |
FO Arithmetic Problems Solutions |
Automata (1) 1 Introduction to finite automata by example 2 How to think about the design of a finite autoamta 3 A finite automaton that can express the addition of two natural numbers |
| Week 2 | Automata (2) 1 The formal definition of (nondeterministic) finite state automata 2 The product construction for finite automata 3 Determinisation of finite automata using the powerset construction |
Decidability of Presburger Arithmetic 1 Deciding Presburger Arithmetic: an overview 2 Transforming the formula into a convenient shape 3 Building an automaton to characterise the quantifier free body 4 Extending the automaton to the quantifier prefix |
Finite Automata Problems Solutions |
Turing Machines (1) 1 Towards undecidability and a definition of algorithm 2 Turing machines by example |
| Week 3 | Turing Machines (2) 1 The formal definition of Turing machine 2 Definition of Turing-recognisibility and Turing-decidability |
Other Machine Models 1 Understanding the power of Turing machines by showing that extensions or variations are equivalent 2 Multitape Turing machines and Turing machines are equally powerful 3 Enumeration machines and Turing machines are equally powerful |
Turing Machines Problems Solutions |
The Church-Turing Thesis 1 Imperative programming and Turing machines are equally powerful 2 The Church-Turing thesis |
| Week 6 | Undecidability 1 The Turing machine acceptance problem is Turing-recognisible. 2 The Turing machine acceptance problem is undecidable. 3 Introducing corecognisibility. How recognisibility, corecognisibility and decidability relate to each other. |
Undecidability via Reduction 1 Undecidability of the halting problem by reduction to the Turing machine acceptance problem. 2 Definition of mapping reducibility and illustration of its use showing undecidability of the halting problem. 3 Precise relationship between mapping reducibility and (co)recognisibility. Illustration by showing that the equivalence problem for Turing machines is neither recognisible nor corecognisible. |
Undecidability Problems |
No lecture |
| Week 7 (NOT ASSESSED) |
Undecidability of True Arithmetic 1 Introducing the undecidability of True Arithmetic via reduction from the complement of the acceptance problem. 2 Defining a scheme for encoding runs of a Turing machine in arithmetic. 3 Defining useful formulas for working with the encoding. 4 Defining a formula to characterise computational steps, and wrapping up. |
Logic and Computation 1 Necessary incompleteness of axiomatisations of arithmetic via Goedel’s Theorem: there are true formulas that are not provable. |
No sheet | No lecture |
You will know enough to attempt the problem sheet for a given Week after listening to the first two lectures of the same week, but the corresponding lab will not actually occur until the following week.
Problem Sheets
The problem sheets are linked here (but may not be available until the appropriate week). Solutions will be released after the Friday lab of each week. They can also be found under the Files tab of the General channel in the COMS20007 Team.
Mini Project
An additional, optional activity is to complete the mini project. The aim of the project is to implement in Haskell the algorithm described in Lecture 5 for deciding Presburger Arithmetic.
You may find the resources provided for the Part II Haskell programming useful, see here.
Materials
This site contains all the definitions and theorems that you need to be able to do the problem sheets and exam for the “Computation” part of Programming Languages and Computation.
The Onenote notebook I write on in the lectures is available here.
The textbook Introduction to the Theory of Computation by Michael Sipser is the ultimate reference for the computability theory in this part of the unit, but I have collected the formal material into this site because:
- Not everyone has a paper copy of the book and the electronic version (which everyone has access to via the library catalogue) is not easy to navigate.
- I want to talk about (and therefore display) the definitions and theorems during lectures.
- The Sipser book does not cover the logic part especially well.
You will need to refer to the textbook or take notes during lectures for discussion of examples, motivation etc.
In the following table “Sipser” refers to Introduction to the Theory of Computation, 3rd edition and “Schoening” refers to Logic for Computer Scientists. Lecture number refers to an entire lecture (of which there are three per week) and not only a part of a lecture.
| Lecture | Additional recommended reading |
|---|---|
| 1 | None |
| 2 | Schoening (pp 67-68) |
| 3 | Sipser (pp 31-34, 47-52) |
| 4 | Sipser (pp 45-46, 55-56) |
| 5 | None |
| 6 | Sipser (pp 165-175) |
| 7 | Sipser (pp 165-175) |
| 8 | Sipser (pp 176-178, 180-182) |
| 9 | Sipser (pp 182-187) |
| 10 | Sipser (pp 202, 207-210) |
| 11 | Sipser (pp 216-217, 234-238) |