Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Intrinsically Correct Algorithms and Recursive Coalgebras

Cass Alexandru, Henning Urbat, Thorsten Wißmann

TL;DR

The paper addresses how to guarantee termination and intrinsic correctness for recursive algorithms by modeling them as recursive coalgebras in categories of indexed families. It introduces well-founded functors on these indexed categories, proving that coalgebras for such functors are inherently recursive and well-founded, thereby unifying recursivity and termination proofs. The authors illustrate the framework with case studies (Quicksort, Euclidean algorithm, CYK parsing, Hydra game) and provide formalized Cubical Agda implementations. The work offers a principled, modular foundation for formalizing and verifying intrinsically correct recursive algorithms in proof assistants and beyond.

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.

Intrinsically Correct Algorithms and Recursive Coalgebras

TL;DR

The paper addresses how to guarantee termination and intrinsic correctness for recursive algorithms by modeling them as recursive coalgebras in categories of indexed families. It introduces well-founded functors on these indexed categories, proving that coalgebras for such functors are inherently recursive and well-founded, thereby unifying recursivity and termination proofs. The authors illustrate the framework with case studies (Quicksort, Euclidean algorithm, CYK parsing, Hydra game) and provide formalized Cubical Agda implementations. The work offers a principled, modular foundation for formalizing and verifying intrinsically correct recursive algorithms in proof assistants and beyond.

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.

Paper Structure

This paper contains 22 sections, 20 theorems, 65 equations.

Table of Contents

  1. Introduction
  2. Recursive Algorithms as Recursive Coalgebras
  3. Categorical Preliminaries
  4. Running Example: Quicksort
  5. Recursive Coalgebras
  6. Well-Founded Coalgebras
  7. Intrinsic Correctness of Quicksort
  8. The Fundamental Challenge
  9. Well-Founded Functors
  10. Well-Founded Coreflection
  11. Agda Library Interface
  12. Well-Founded Functors
  13. Quicksort
  14. Ranked Coalgebras and Termination Proofs
  15. Case Studies
  16. ...and 7 more sections

Key Result

proposition 1

The coalgebra $c\colon Z^*\to 1+Z^*\times Z \times Z^*$ defined by eq:sort-coalgebra is recursive.

Theorems & Definitions (34)

  • definition 1: Recursive Coalgebra, \onlineHtmlURL Cubical.Categories.Functor.RecursiveCoalgebra.html#isRecursive
  • proposition 1
  • definition 2: Well-Founded Coalgebra
  • Remark 2
  • proposition 2: taylor99
  • theorem 3: Recursion Theorem for Indexed Sets
  • proposition 3
  • theorem 5: Correctness of Quicksort, \onlineHtmlURL QuickSort.QuickSort.html#quickSort
  • Remark 7
  • definition 3: Well-Founded Functor
  • ...and 24 more