Content
The course will introduce and relate different models of computation:
- recursive function theory
- combinatory logic
- LOOP/WHILE programs
- lambda calculus
Schedule
| week |
date |
topics |
slides |
exercises |
solutions |
|---|
| 1 |
02.10 |
primitive recursion |
pdf (1x1, 4x1) |
pdf |
pdf |
| 2 |
09.10 |
Gödel numbering, Ackermann function, recursive functions |
pdf (1x1, 4x1) |
pdf |
pdf |
| 3 |
16.10 |
LOOP programs, elementary functions, Grzegorczyk hierarchy |
pdf (1x1, 4x1) |
pdf |
pdf |
| 4 |
23.10 |
WHILE programs, (partial) recursive functions, Kleene's normal form
theorem |
pdf (1x1, 4x1) |
pdf |
pdf |
| 5 |
30.10 |
normal form theorem, undecidability, s-m-n theorem, fixed point
theorem |
pdf (1x1, 4x1) |
pdf |
pdf |
| 6 |
06.11 |
recursive (enumerable) sets, diophantine sets |
pdf (1x1, 4x1) |
pdf |
pdf |
| 7 |
13.11 |
combinatory logic, Church numerals, combinatorial completeness |
pdf (1x1, 4x1) |
pdf |
pdf |
| 8 |
20.11 |
Church – Rosser theorem, Z property, CL representability |
pdf (1x1, 4x1) |
pdf |
pdf |
| 9 |
27.11 |
normalization theorem, CL representability |
pdf (1x1, 4x1) |
pdf |
pdf |
| 10 |
04.12 |
arithmetization, fixed point theorem, undecidability, types |
pdf (1x1, 4x1) |
pdf |
pdf |
| 11 |
11.12 |
typing, strong normalization, intuitionistic propositional logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 12 |
08.01 |
Hilbert systems, Curry – Howard isomorphism, intuitionistic
propositional logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 13 |
15.01 |
lambda-calculus |
pdf (1x1, 4x1) |
pdf |
pdf |
| 14 |
22.01 |
test practice |
pdf (1x1, 4x1) |
|
|
| 15 |
29.01 |
test
(solution) |
|
|
|
Literature
Slides as well as solutions to selected exercises will be made available
online. Accompanying literature will be linked from the course website.