Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$

Tom de Jong

TL;DR

This work develops domain theory within constructive, predicative univalent foundations, building dcpos and Scott-continuous maps while carefully tracking universe parameters to preserve predicativity. It introduces lifting, products, exponentials, and bilimits, and culminates in a predicative reconstruction of Scott's $D_\infty$ model, establishing an isomorphism with its self-exponential. The development is formalised in Agda, demonstrating that large carriers are compatible with predicative reasoning and universe management. The results extend domain-theoretic methods to a topos-friendly, intuitionistic setting and lay groundwork for a predicative theory of continuous and algebraic domains in a subsequent Part II, with significant implications for semantics and higher-type computability in univalent foundations.

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 iterative constructions of dcpos may 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. In particular, we give a predicative reconstruction of Scott's $D_\infty$ model of the untyped $λ$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$

TL;DR

This work develops domain theory within constructive, predicative univalent foundations, building dcpos and Scott-continuous maps while carefully tracking universe parameters to preserve predicativity. It introduces lifting, products, exponentials, and bilimits, and culminates in a predicative reconstruction of Scott's model, establishing an isomorphism with its self-exponential. The development is formalised in Agda, demonstrating that large carriers are compatible with predicative reasoning and universe management. The results extend domain-theoretic methods to a topos-friendly, intuitionistic setting and lay groundwork for a predicative theory of continuous and algebraic domains in a subsequent Part II, with significant implications for semantics and higher-type computability in univalent foundations.

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 iterative constructions of dcpos may 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. In particular, we give a predicative reconstruction of Scott's model of the untyped -calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
Paper Structure (21 sections, 48 theorems, 49 equations)

This paper contains 21 sections, 48 theorems, 49 equations.

Table of Contents

  1. Introduction
  2. Constructivity
  3. Predicativity
  4. Related work
  5. Relation to our other work
  6. Formalisation
  7. Organisation
  8. Foundations
  9. Universes
  10. The univalent point of view
  11. Extensionality axioms
  12. The propositional truncation
  13. Size and impredicativity
  14. Directed complete posets
  15. Scott continuous maps
  16. ...and 6 more sections

Key Result

Lemma 3.3

If $(P,\mathrel\sqsubseteq)$ is a poset, then $P$ is a set.

Theorems & Definitions (150)

  • Definition 2.1: Smallness
  • Definition 2.2: Type of propositions $\Omega_{\mathcal{U}}$
  • Definition 2.3: $\mathcal{V}$-powerset $\mathop{\mathrm{\mathcal{P}}}\nolimits_{\mathcal{V} }(X)$, $\mathcal{V}$-subsets
  • Definition 2.4: $\in,\subseteq$
  • Definition 3.1: Preorder, reflexivity, transitivity
  • Definition 3.2: Poset, antisymmetry
  • Lemma 3.3
  • proof
  • Definition 3.4: (Semi)directed family
  • Remark 3.5
  • ...and 140 more