LFCS Seminar: 4 February 2020 - Fredrik Nordvall Forsberg

Title: Ordinal Notation Systems for Ordinals below ε₀ in modern type theories

Abstract:

Ordinals and well-ordered sets have many applications for reasoning about programs and their termination. For representing ordinals in a computer, one needs a so-called notation system, where each term of the system denotes an ordinal. However, many notation system do not represent ordinals uniquely, which means that e.g. transfinite induction is not provable for the notation system. In contrast, I will present multiple ordinal notation systems uniquely representing ordinals, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. By proving the different systems equivalent, we can transport constructions such as arithmetic operations and properties such as transfinite induction between them using the univalence principle.

This is joint work with Chuangjie Xu and Nicolai Kraus.

Affiliation:

Mathematically Structured Programming Group at the Department of Computer & Information Sciences, University of Strathclyde.