Intrinsically Correct Algorithms and Recursive Coalgebras

Reference. Intrinsically Correct Algorithms and Recursive Coalgebras

Cass Alexandru, Henning Urbat, Thorsten Wißmann · arXiv · 2026 · coalgebra · PDF · Web · arXiv · pldb

Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda.

Cite

Cite as @alexandruIntrinsicallyCorrectAlgorithms2025-preprint (helia, typst) · \cite{alexandruIntrinsicallyCorrectAlgorithms2025-preprint} (LaTeX)

BibTeX

bibtex · 10 lines

@article{alexandruIntrinsicallyCorrectAlgorithms2025-preprint,
 title = {Intrinsically Correct Algorithms and Recursive Coalgebras},
 author = {Cass Alexandru and Henning Urbat and Thorsten Wißmann},
 year = {2026},
 eprint = {2512.10748},
 archiveprefix = {arXiv},
 primaryclass = {cs.PL},
 note = {v2},
 url = {https://arxiv.org/abs/2512.10748}
}

hayagriva YAML (typst)

yaml · 14 lines

alexandruIntrinsicallyCorrectAlgorithms2025-preprint:
  type: article
  title: Intrinsically Correct Algorithms and Recursive Coalgebras
  author:
  - Alexandru, Cass
  - Urbat, Henning
  - Wißmann, Thorsten
  date: 2026
  url: https://arxiv.org/abs/2512.10748
  serial-number:
    arxiv: '2512.10748'
  note: v2
  parent:
    type: periodical

Download: alexandruIntrinsicallyCorrectAlgorithms2025-preprint.bib · alexandruIntrinsicallyCorrectAlgorithms2025-preprint.yml

Cited by (1)

Definition. Recursive coalgebra recursive-coalgebra

Fix an endofunctor $𝐹 : 𝒞︀ \to 𝒞︀$ . A coalgebra $𝛾 : 𝑋 \to 𝐹 𝑋$ is recursive when for every algebra $𝛼 : 𝐹 𝐵 \to 𝐵$ there is exactly one hylomorphism $ℎ : 𝑋 \to 𝐵$ from $𝛾$ to $𝛼$ , that is, exactly one solution of

ℎ = 𝛾 ⋆ 𝐹 ℎ ⋆ 𝛼 .

Equivalently, the functor $𝖧𝗒𝗅𝗈 (𝛾, -)$ of the hylomorphism profunctor is constantly a singleton.

Recursiveness is a coalgebraic form of well-foundedness: $𝛾$ decomposes each input into subproblems, and recursiveness says that every divide-and-conquer program built on this decomposition has a unique meaning, without mentioning an order on inputs. [1] use recursive coalgebras on categories of indexed families to obtain algorithms that are correct by the type of the map they compute.

Example. If $(𝜇 𝐹, 𝗂𝗇)$ is an initial algebra, then $𝗂𝗇$ is invertible (Lambek’s lemma) and ${𝗂𝗇}^{- 1} : 𝜇 𝐹 \to 𝐹 (𝜇 𝐹)$ is a recursive coalgebra. Precomposing with the isomorphism $𝗂𝗇$ , the equation $ℎ = {𝗂𝗇}^{- 1} ⋆ 𝐹 ℎ ⋆ 𝛼$ is equivalent to $𝗂𝗇 ⋆ ℎ = 𝐹 ℎ ⋆ 𝛼$ , which says $ℎ$ is an algebra map out of the initial algebra; there is exactly one, $𝖿𝗈𝗅𝖽 𝛼$ .

The dual notion is a corecursive algebra.

Cites 32 works (4 here)

With notes (4)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

Intrinsically Correct Sorting in Cubical Agda alexandruIntrinsicallyCorrectSorting2025CPP · 2025

The paper “Sorting with Bialgebras and Distributive Laws” by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.

PDF · DOI · arXiv · pldb

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types VezzosiMortbergAbel2019ICFP · 2019

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

PDF · DOI · pldb

Generalizing determinization from automata to coalgebras silva-2013-generalizingLMCS · 2013

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics.

DOI · arXiv

External (28)

Well-Founded Coalgebras Meet König's Lemma (2026)
Initial Algebras and Terminal Coalgebras (2025)
Program Optimisations via Hylomorphisms for Extraction of Executable Code (2025)
Formalization accompanying the paper “Intrinsically Correct Sorting in Cubical Agda” version v0 (2024)
Well-Founded Recursion Done Right (2024)
Well-founded coalgebras, revisited (2017)
Conjugate Hylomorphisms – Or (2015)
Proving program termination (2011)
Category Theory (2nd ed.) (2010)
Recursive coalgebras from comonads (2006)
Containers: Constructing strictly positive types (2005)
Modelling general recursion in type theory (2005)
Transition invariants (2004)
Abstract and Concrete Categories: The Joy of Cats (2004)
Fixed Point Objects Corresponding to Freyd Algebras (Eppendahl, manuscript) (2000)
Practical Foundations of Mathematics (1999)
Categories for the Working Mathematician (2nd ed.) (1998)
Algebra of Programming (1997)
The Art of Computer Programming, Volume 2: Seminumerical Algorithms (3rd ed.) (1997)
Inductive families (1994)
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire (1991)
Automata and Algebras in Categories (1990)
Accessible Independence Results for Peano Arithmetic (1982)
Introduction to Automata Theory, Languages, and Computation (1979)
Categorical set theory: A characterization of the category of sets (1974)
Quicksort (1962)
Function Definitions : Dot Patterns — Agda 2.8.0 documentation
Rocq-Prover/Rocq: Rocq