The theory of computing deals with questions such as: what is computation? What problems can be computed? What is the inherent difficulty of a given problem? To answer such questions in a satisfactory manner, we need a formal definition of computation, which does not rely on any specific hardware or programming language. It is perhaps surprising that some real-world problems can be mathematically proven to be undecidable, i.e. regardless of any future advances in hardware, such problems are provably impossible to solve on a computer. In this module we will discuss the main models of computability and provide several examples of undecidable problems. While questions about computability have initially been studied from a theoretical perspective, the resulting theories have had many important practical applications. Among others, the methods discussed in this module are used for implementing compilers (in particular for parsing), for defining functional programming languages, and for formally verifying the correctness of software and hardware.

1. Use standard methods for proving mathematical properties
2. Understand the basic rules of classical logic
3. Apply formal methods to prove the correctness of a java program
4. Use propositional logic to simplify Boolean circuits
5. Understand the application of formal languages and automata theory to problems in computer science
6. Demonstrate an understanding of formal languages and automata

          Explain the notion of undecidability and its importance for computer science

     7.   Explain the basic concepts from complexity theory

     8.   Understand the use of reductions to characterise the complexity of a decision problem

20 lectures, 3 lab classes, 7 tutorials

Formally verifying the correctness of a java program

Implementing a simple parser

Using the functional programming paradigm

Coursework: The coursework will allow the student to demonstrate their knowledge and practical skills and to apply the principles taught in lectures.

Exam: A written exam (2 h) will test the student's knowledge and understanding as elaborated under the learning outcomes.

Formal methods in computer science

• Basic proof techniques: proof by contradiction, proof by induction, case analysis
• Propositional logic
• Application: Boolean circuits
• Application: Hoare calculus

Formal Languages and Automata

• Regular expressions, finite state machines, Kleene's theorem
• Push-down automata, context-free grammars, the pumping lemma
• Application: parsing
• Context-sensitive grammars

Models of computation

• Turing machines
• Lambda calculus
• Application: functional programming
• Undecidability, the halting problem, the domino problem

Computational complexity

• Non-determinism
• The complexity classes P, NP, PSPACE, EXPTIME
• Reductions, the SAT problem
• P vs NP problem

Daniel Velleman. How to prove it: a structured approach, Cambridge  University Press, ISBN 9780521675994, 2006

Michael Sipser. Introduction to the theory of computation (3^rd edition), Cengage Learning, ISBN 113318779X, 2012