Domain theory in constructive and predicative univalent foundations

de Jong, Tom ORCID: 0000-0003-1585-3172 (2023). Domain theory in constructive and predicative univalent foundations. University of Birmingham. Ph.D.

Preview

deJong2023PhD.pdf
Text - Accepted Version
Available under License All rights reserved.
Download (1MB) | Preview

Abstract

We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in a variety of fields, such as programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that complex constructions of dcpos, involving countably infinite iterations of exponentials for example, result in a need for ever-increasing universes and are predicatively impossible. We show, through a careful tracking of type universe parameters, that such constructions can be carried out in a predicative setting. We illustrate the development with applications in the semantics of programming languages: the soundness and computational adequacy of the Scott model of PCF, and Scott's D∞ model of the untyped λ-calculus. Both of these applications make use of Escardó's and Knapp's type of partial elements. Taking inspiration from work in category theory by Johnstone and Joyal, we also give a predicative account of continuous and algebraic dcpos, and of the related notions of a small (compact) basis and its rounded ideal completion. This is accompanied by concrete examples, such as the small compact basis of Kuratowski finite subsets of the powerset. The fact that nontrivial dcpos have large carriers is in fact unavoidable and characteristic of our predicative setting, as we explain in a complementary chapter on the constructive and predicative limitations of univalent foundations. We prove no-go theorems for a general class of posets that includes dcpos, bounded complete posets, sup-lattices and frames. In particular, we show that, constructively, locally small nontrivial dcpos necessarily lack decidable equality. Our account of domain theory in univalent foundations has been fully formalised with only a few minor exceptions. The ability of the proof assistant Agda to infer universe levels has been invaluable for our purposes.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):