Intrinsically Correct Algorithms and Recursive Coalgebras

TL;DR

This paper introduces a new framework using well-founded functors to ensure recursive coalgebras are intrinsically correct, simplifying proofs of recursivity and termination in categorical algorithms.

Contribution

It presents a novel approach to guarantee recursivity of coalgebras from their type, unifying existing techniques and formalizing results in Cubical Agda.

Findings

Every coalgebra for a well-founded functor is recursive.

The framework subsumes traditional ranking function techniques.

Main results and case studies are formalized in Cubical Agda.

Abstract

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.