Models of computation

The classical formalizations of the notion of computable function. The course defines Turing machines, unlimited register machines, LOOP and WHILE programs, primitive and partial recursive functions and the λ-calculus, develops each model far enough to program non-trivial functions in it, and proves that all of them compute the same partial functions. It closes with Kleene's normal form theorem and a discussion of the Church–Turing thesis. Primitive recursive coding of finite sequences, introduced along the way, is used throughout the rest of the curriculum.

Contents

1. 1

   Algorithms and partial functions

   Historical motivation for a formal notion of computability, partial functions and their notation, and the coding of finite objects by integers.

   1. 1.1 The Entscheidungsproblem
   2. 1.2 Features of an algorithm
   3. 1.3 Partial functions
   4. 1.4 Coding finite objects by integers
   5. 1.5 Exercises
   6. 1.6 Notes and references
   30 min
2. 2

   Turing machines

   Formal definition of Turing machines, configurations and computations, input and output conventions, and two machines verified in detail.

   1. 2.1 Definition
   2. 2.2 Computing functions
   3. 2.3 First example: the successor function
   4. 2.4 Second example: addition
   5. 2.5 Exercises
   6. 2.6 Notes and references
   35 min
3. 3

   Programming Turing machines

   Auxiliary symbols, sequential composition of machines, translation invariance, multi-tape machines and their simulation by single-tape machines.

   1. 3.1 Auxiliary symbols: a doubling machine
   2. 3.2 Translation invariance
   3. 3.3 Sequential composition
   4. 3.4 Multi-tape machines
   5. 3.5 Other variants
   6. 3.6 Exercises
   7. 3.7 Notes and references
   40 min
4. 4

   Register machines

   Unlimited register machines (URM), their operational semantics, examples, concatenation of programs, and closure of URM-computable functions under composition.

   1. 4.1 Definition
   2. 4.2 Examples
   3. 4.3 Combining programs
   4. 4.4 Closure under composition
   5. 4.5 Goto programs and assembly languages
   6. 4.6 Exercises
   7. 4.7 Notes and references
   35 min
5. 5

   Primitive recursive functions

   Definition of the primitive recursive functions and predicates, and their closure under definition by cases, bounded sums and products, bounded quantification and bounded minimization.

   1. 5.1 Definition
   2. 5.2 First closure properties
   3. 5.3 Predicates
   4. 5.4 Bounded sums, products and quantifiers
   5. 5.5 Bounded minimization
   6. 5.6 Arithmetic functions and primes
   7. 5.7 Exercises
   8. 5.8 Notes and references
   45 min
6. 6

   Coding finite sequences

   Primitive recursive coding of finite sequences of integers, operations on codes, course-of-values recursion, and Gödel's β-function.

   1. 6.1 Prime power coding
   2. 6.2 Course-of-values recursion
   3. 6.3 Gödel's β-function
   4. 6.4 Exercises
   5. 6.5 Notes and references
   35 min
7. 7

   The Ackermann function

   A total computable function which is not primitive recursive. Monotonicity properties, the majorization theorem, and a diagonal argument.

   1. 7.1 Definition and computability
   2. 7.2 Monotonicity
   3. 7.3 Majorization
   4. 7.4 A diagonal argument
   5. 7.5 Exercises
   6. 7.6 Notes and references
   40 min
8. 8

   Minimization and partial recursive functions

   The minimization operator, the partial recursive functions, recursive functions and predicates, and the statement of Kleene's normal form theorem.

   1. 8.1 The minimization operator
   2. 8.2 Partial recursive functions
   3. 8.3 Examples
   4. 8.4 Regular minimization
   5. 8.5 Kleene's normal form
   6. 8.6 Exercises
   7. 8.7 Notes and references
   35 min
9. 9

   LOOP and WHILE programs

   Structured programs with bounded and unbounded loops. The LOOP-computable functions are the primitive recursive functions, and the WHILE-computable functions are the partial recursive functions.

   1. 9.1 Syntax and semantics
   2. 9.2 Programming in LOOP
   3. 9.3 LOOP programs compute the primitive recursive functions
   4. 9.4 WHILE programs compute the partial recursive functions
   5. 9.5 WHILE programs and register machines
   6. 9.6 Exercises
   7. 9.7 Notes and references
   45 min
10. 10

    The λ-calculus

    λ-terms, free variables and substitution, α-equivalence, β-reduction, normal forms, the Church–Rosser theorem, and reduction strategies.

    1. 10.1 Terms
    2. 10.2 Free variables and substitution
    3. 10.3 β-reduction
    4. 10.4 Confluence
    5. 10.5 Reduction strategies
    6. 10.6 Exercises
    7. 10.7 Notes and references
    40 min
11. 11

    Computing with λ-terms

    Church numerals, arithmetic, booleans and pairs in the pure λ-calculus, Kleene's predecessor, fixed-point combinators, and the λ-definability of the partial recursive functions.

    1. 11.1 Church numerals and arithmetic
    2. 11.2 Booleans, conditionals and pairs
    3. 11.3 The predecessor
    4. 11.4 Fixed-point combinators
    5. 11.5 λ-definability of the partial recursive functions
    6. 11.6 Exercises
    7. 11.7 Notes and references
    45 min
12. 12

    Equivalence of the models

    Arithmetization of Turing machines, proof of Kleene's normal form theorem, simulation of register machines by Turing machines, and the universal partial recursive function.

    1. 12.1 Arithmetization of Turing machines
    2. 12.2 Kleene's normal form theorem
    3. 12.3 From register machines to Turing machines
    4. 12.4 Proof of the equivalence
    5. 12.5 The universal function
    6. 12.6 Exercises
    7. 12.7 Notes and references
    45 min
13. 13

    The Church–Turing thesis

    Formulation and status of the Church–Turing thesis, Turing's analysis of human computation, Gandy's principles, physical and complexity-theoretic variants, and the use of the thesis in proofs.

    1. 13.1 Status of the thesis
    2. 13.2 Turing's analysis
    3. 13.3 Evidence
    4. 13.4 Variants
    5. 13.5 Using the thesis in proofs
    6. 13.6 Notes and references
    25 min