1st Semester 2021/22: Kleene Algebra

Instructors

Tobias Kappé

ECTS

6

Description

You probably have experience with manipulating mathematical expressions. For instance, you can make the following derivation for all x, y, z ∈ ℕ:

x · (y + z)

  = x · y + x · z (distributivity of multiplication over addition)

  = y · x + z · x (commutativity of multiplication)

  = z · x + y · x (commutativity of addition)

Kleene Algebra (KA) is the study of such equalities, except that the objects under consideration are computer programs. You may have encountered KA expressions inside the modal operators of Propositional Dynamic Logic, or through the expression matching libraries offered by many programming languages.

A good understanding of KA is useful when you are reorganizing program code — e.g., to improve readability, or to optimize performance — and you want to be sure that your new program is equivalent to your old program. Interestingly, KA can even help you create programming languages that allow the user to automatically verify certain correctness properties. This course covers KA in detail, from the basic reasoning steps to its advanced logical properties.

Organisation

The first half of this course consists of a set of lectures that explain KA from first principles, with one week to introduce the system, and another to consider advanced topics such as decidability and logical completeness. This part of the course will also involve self-contained homework sets, to help you further familiarise yourself with the material.

 

The lectures are organised as follows:

• Lecture #1: Getting acquainted. We introduce KA as a “programming language”, review its axioms, and demonstrate reasoning about equivalence.
• Lecture #2: Adding flow control. We extend KA to Kleene Algebra with Tests (KAT), and show how the extended system can reason about flow control.
• Lecture #3: Models and refutation. We give two possible (sound) semantics to KA, show how they relate, and use them to refute some equalities.
• Lecture #4: Automation. We show how to use automata to automatically check semantic equivalences, paving the way to automatic refutation.
• Lecture #5: Kleene’s theorem. KA expressions correspond to automata, and vice versa. We review this celebrated result by Kleene, and its proof.
• Lecture #6: Logical completeness. We show that KA is logically complete: one can prove all equivalences that are semantically true.

In the second half of the course you will choose a particular subject related to KA, which you will study in detail based on some relevant papers suggested by the instructor. In the final week, you will summarise the relevant results within this topic in detail for your peers.

 

The following are suggested topics for further study. You are allowed and in fact encouraged to propose KA-related subjects that you would like to pursue, in consultation with the instructor. Regardless of the topic chosen, you are expected to deliver a lecture explaining the material to your peers.

• Kleene Algebra with Tests.
• Concurrent Kleene Algebra.
• Guarded programs.
• NetKAT and its applications.
• Optimized equivalence checking.
• Complexity of equivalence checking.
• Connections to Propositional Dynamic Logic.

Prerequisites

Technical content includes elementary discrete mathematics,
including inductive and equational proofs. Earlier exposure to automata theory and linear algebra is useful (but not necessary!) for the second half of the course.

Assessment

The course will be assessed as fail/pass based on homework exercises, final presentations (roughly 30 minutes), and lecture attendance.