Uniform Elgot Iteration in Foundations

TL;DR

This paper introduces a categorical notion of partiality using uniform iteration, resulting in a new monad structure that connects to classical choice principles and Elgot monads.

Contribution

It provides a generic categorical framework for partiality via uniform iteration, leading to the construction of an equational lifting monad with desirable properties.

Findings

The free structures called uniform-iteration algebras are established.

The resulting monad is shown to be an Elgot monad under certain classical assumptions.

The approach unifies partiality concepts in category theory and computer science.

Abstract

Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which makes them easily transferable across application domains. The notion of partiality is however notoriously difficult to characterize in this way, although the importance of it is certain, especially for computer science where entire research areas, such as synthetic and axiomatic domain theory revolve around notions of partiality. More recently, this issue resurfaced in the context of (constructive) intensional type theory. Here, we provide a generic categorical iteration-based notion of partiality, which is arguably the most basic one. We show that the emerging free structures, which we dub uniform-iteration algebras enjoy various desirable properties, in particular, yield an equational lifting monad. We then study the impact of classicality assumptions and choice principles on this monad, in particular, we establish a suitable categorial formulation of the axiom of countable choice entailing that the monad is an Elgot monad.