Reference. Initial Algebras of Domains via Quotient Inductive-Inductive Types

Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language concepts, to understand how programs behave and to reason about programs. At the same time it serves as a great theory to model various algebraic effects such as non-determinism, partial functions, side effects and numerous other forms of computation. In the present paper, we present a general framework to construct algebraic effects in domain theory, where our domains are DCPOs: directed complete partial orders. We first describe so called DCPO algebras for a signature, where the signature specifies the operations on the DCPO and the inequational theory they obey. This provides a method to represent various algebraic effects, like partiality. We then show that initial DCPO algebras exist by defining them as so called Quotient Inductive-Inductive Types (QIITs), known from homotopy type theory. A quotient inductive-inductive type allows one to simultaneously define an inductive type and an inductive relation on that type, together with equations on the type. We illustrate our approach by showing that several well-known constructions of DCPOs fit our framework: coalesced sums, smash products and free DCPOs (partiality and power domains). Our work makes use of various features of homotopy type theory and is formalized in Cubical Agda.

Cite

Cite as @vancollem-2025-initial (helia, typst) · \cite{vancollem-2025-initial} (LaTeX)
BibTeX
bibtex · 1 line
@article{vancollem-2025-initial, title={Initial Algebras of Domains via Quotient Inductive-Inductive Types}, volume={Volume 5 - Proceedings of...}, ISSN={2969-2431}, url={http://dx.doi.org/10.46298/entics.16512}, DOI={10.46298/entics.16512}, journal={Electronic Notes in Theoretical Informatics and Computer Science}, publisher={Centre pour la Communication Scientifique Directe (CCSD)}, author={van Collem, Simcha and van der Weide, Niels and Geuvers, Herman}, year={2025}, month=Dec }
hayagriva YAML (typst)
yaml · 21 lines
vancollem-2025-initial:
  type: article
  title: Initial Algebras of Domains via Quotient Inductive-Inductive Types
  author:
  - name: Collem
    given-name: Simcha
    prefix: van
  - name: Weide
    given-name: Niels
    prefix: van der
  - Geuvers, Herman
  date: 2025-12
  url: http://dx.doi.org/10.46298/entics.16512
  serial-number:
    doi: 10.46298/entics.16512
    issn: 2969-2431
  parent:
    type: periodical
    title: Electronic Notes in Theoretical Informatics and Computer Science
    publisher: Centre pour la Communication Scientifique Directe (CCSD)
    volume: Volume 5 - Proceedings of...
Cites 25 works (3 here)
With notes (3)

The Interval Domain in Homotopy Type Theory vanderweide-2024-the

DOI

Quotient Inductive-Inductive Types altenkirch_etal_2018

Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules.
DOI

Homotopy Type Theory: Univalent Foundations of Mathematics hottbook

Web · arXiv
vancollem-2025-initial reference entries/refs/vancollem-2025-initial/vancollem-2025-initial.hel