Models of Computation
The course intends to make sure that all students establish a stronger foundation in the more theoretical side of Computer Science, thus better preparing them for the courses that will follow in the fourth year.
The course will focus on teaching students the fundamental skills involved in dealing with abstract systems and constructing proofs, through both teaching and exercises.
At the end of the course, the students will:
- Understand the notion of computable functions and various formalisms which capture this notion, including Register Machines and the Lambda Calculus
- Be able to read and write small- and big-step operational semantics for simple programming languages, and also to prove properties about such semantics and languages using structural induction.
- Be able to read and construct register machines and Turing machines, and reason about the execution of such machines.
- Be able to construct rigorous arguments about properties of the Lambda Calculus, construct reduction sequences according to particular reduction orders, and understand the relationship bewteen the Lambda Calculus and other notions of computability.
The course will address the following fundamental questions:
1. What does a computer program mean?
2. How can we be sure that what runs is what we intended?
3. What programs can we write, and what not?
4. Is there a fundamental difference between programming paradigms?
5. How effective is a program, how much does running a program cost?
It will address these by, in the first part, starting with the rudimentary imperative programming language While, a programming language with conditionals, variables, and loops, for which two formal semantics are defined. The course will look at URM, a formal, abstract assembler language machine, and it will be shown that compiled programs have the same behaviour as their original. In the second part, the students will be introduced to Turing Machines, and the concept of the Universal Turing Machine. The halting problemand undecidabilitywill be discussed in the context of TuringMachines. Then the focus turns to the Lambda Calculus, and is main properties. Attention the turns to definability of functions, and the mapping of lambda term to Turing Machines. In the third part, the focus turns to complexity. The students will be introduced to non-determinism, and polynomial time. The class NP will be introduced and discussed, as well as the issue P vs NP.
The course will last the full 11 weeks of Autumn term, so will take up 22 + 11 hours.
Part 1: Semantics
1. Syntax and Semantics: Why formal semantics? States Difference between Operational Semantics,
Denotational Semantics, and Axiomatic Semantics Abstract and Concrete Syntax
2. Natural Semantics: Natural Semantics of Arithmetic Expressions Denotational Semantics for Arithmetic
Expressions Show that these are equivalent and deterministic. Semantics of Boolean Expressions
3. The languageWhile: Natural Semantics of While
4. Semantic Equivalence for Natural Semantics Determinism for Natural Semantics
5. Structural Operational Semantics Sequences
6. Determinism and Equivalence
7. Provably correct implementation: The abstract machine language: URM
8. Translation of programs Correctness of translation
Part 2: Lambda Calculus
1. Introduction to the Lambda-Calculus - basic syntax - informal reductions - examples
2. Reduction and substitution - alpha-conversion - substitution - beta-reduction
3. Normal Forms and the Church-Rosser Theorem - normal forms - church rosser - standard reductions
4. Lambda-Computable Functions - encoding of numbers, truth values, conditionals - examples
5. The fixpoint Theorem- equational theory of the lambda-calculus - fixpoint combinators and recursive
6. From Lambda-Calculus to the URM - simulation of reduction on a URM (or while-program) - simulation
of URMs via lambda-terms (in parts)
7. Self-Reference and universal machines - indices of computable functions - functions of multiple
variables - construction of the universal machine
8. The halting problem and other undecidable problems - basic decision problems - the halting problem
- the totality problem
Part 3: Complexity
1. The turing machine as a more primitive model - definition and examples - mapping of URMs to
2. How to measure complexity of computation and polynomial time: The robustness of the polynomial.
Introduce the class of polynomial time. Give examples and establish polynomial time as efficient.
3. Nondeterminism as a model for parallel computation: Establish that nondeterministic machines can
be simulated by deterministic machines.
4. Introduce the class NP: Examples of problems solvable in NP.
5. P=NP: Discuss the techniques to show that P=NP. Introduce reductions between problems and
measure the complexity of reductions. Introduce the notion of NP-complete problems.
6. SAT as an NP-complete problem: Prove that SAT is NP-complete.
The material will be presented in the form of lecture notes. These will be made available to the students in batches over the term. Students are expected to print out these notes in advance. This material is supplemented with problem sheets, where students get to practice what they have seen in lectures.
Module leadersDr Herbert Wiklicky
Professor Philippa Gardner