### Lectures

**Because of the
coronavirus situation, all teaching on the course has moved to the Zoom
remote meeting platform. For further information, see Forums -> Announcements.**

What is theoretical computer science? Sets. Relations and functions. Equivalence relations. Proof by induction. Automata, alphabets, strings, languages.

State diagrams and transition tables. Programming with finite automata. Formal definition of finite automata. Excursion: Extensions of finite automata.

Minimisation of finite automata. Nondeterministic finite automata. Equivalence of deterministic and nondeterministic finite automata.

Syntax and semantics of regular expressions. Regular expressions and finite automata. Excursion: Regular expressions in programming languages.

The pumping lemma. Generating strings with grammars. Context-free grammars. Some useful constructions. Right- and left-linear grammars.

The parsing problem and parse trees. Recursive-descent parsing. LL(1) grammars. Excursion: Attribute grammars. Excursion: Parsing tools in the Scala language. Supplement: General definition of LL(1) grammars.

Parsing context-free grammars. The Chomsky normal form for CFGs. The CYK parsing algorithm. Pushdown automata. Pushdown automata and context-free languages. A pumping lemma for context-free languages.

Turing machines. Extensions of Turing machines: multitrack machines, multitape machines, nondeterministic machines. Some computability theory: Turing-recognisable and Turing-decidable languages. Excursion: The halting problem, first encounter.

Decidable and semi-decidable languages and problems. Background: countable and uncountable sets. Universal Turing machines and undecidable problems.

Undecidability of some Turing machine properties: the halting and non-emptiness problems. Other undecidability results: logic and algebra, Post's correspondence problem, the Chomsky hierarchy. Computable functions and reductions. Excursion: Post's correspondence problem.

Rice's theorem. Unrestricted grammars and their relation to Turing machines. Context-sensitive grammars. A glimpse beyond: Computational complexity.

Programs as state transformers. Specification and correctness of programs: weak and strong correctness, proving weak correctness viar loop invariants. Establishing strong correctness.