Pith. sign in

REVIEW 2 minor 1 cited by

Intrinsically Correct Algorithms and Recursive Coalgebras

T0 review · 0 major / 2 minor · reviewed 2026-05-16 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Every coalgebra for a well-founded functor on indexed families is recursive, so termination follows from the coalgebra type alone.

desk verdict The paper defines well-founded functors on indexed families so that coalgebras for them are automatically recursive, with the whole thing machine-checked in Cubical Agda. read the letter →

arxiv 2512.10748 v3 submitted 2025-12-11 cs.PL cs.LO

Cass Alexandru , Henning Urbat , Thorsten Wi{ss}mann This is my paper · ORCID
classification cs.PLcs.LO
keywords coalgebrasrecursivealgorithmswell-foundedfunctorsterminationindexedfamiliescategorytheoryCubicalAgdaprogramcorrectness
checked against LogicNatabsolute_floor_iff_bare_distinguishability
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper constructs a general setting where recursive algorithms are modeled as coalgebras over categories of families indexed by a well-founded relation. In this setting a functor is called well-founded when it preserves well-foundedness; the central theorem states that every coalgebra for such a functor is automatically recursive. Because recursivity is guaranteed by the type of the coalgebra map, both termination and correctness are obtained without separate proofs. The same abstract condition recovers classical termination arguments such as ranking functions and applies directly to concrete algorithms including Quicksort, the Euclidean algorithm, and CYK parsing. The entire development, including the main theorem and selected examples, has been formalized in Cubical Agda.

What carries the argument

A well-founded functor on the category of families indexed by a well-founded relation; it preserves well-foundedness and thereby forces every coalgebra to satisfy the recursive equation.

What would settle it

An explicit coalgebra whose structure map fails the recursive equation while the underlying functor satisfies the well-foundedness preservation condition.

Watch

Extended reading notes

Core claim

We show as our main result that every coalgebra for a well-founded functor is recursive. A functor on a category of families indexed by a well-founded relation is well-founded when it maps well-founded objects to well-founded objects; the recursivity condition on a coalgebra then follows directly from this preservation property.

Load-bearing premise

The functor must preserve the well-foundedness of families whenever the indexing relation is well-founded.

Editorial extensions

If this is right

  • Termination and partial correctness of a recursive algorithm become intrinsic properties of its coalgebra type.
  • Proofs that rely on ranking functions or other well-founded measures are recovered as instances of the same abstract condition.
  • Algorithms such as Quicksort, the Euclidean algorithm, and CYK parsing receive intrinsic recursive coalgebra structures.
  • Formalization of recursive algorithms in proof assistants is simplified because no separate termination argument needs to be supplied.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The framework may be applied to other coalgebraic models of recursion that currently require manual well-foundedness proofs.
  • Dependent type theories could encode the indexing relation directly, allowing the type checker to discharge termination obligations automatically.
  • Similar well-foundedness preservation conditions might be formulated for other categorical structures such as monads or operads.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 2 minor

Summary. The paper introduces well-founded functors on categories of families indexed by well-founded relations. Its central claim is that every coalgebra for a well-founded functor is recursive; this is proved as the main theorem, shown to subsume ranking-function techniques, and illustrated via case studies (Quicksort, Euclidean algorithm, CYK parsing). Both the theorem and selected case studies are fully formalized in Cubical Agda.

Significance. If the result holds, the framework supplies a uniform, intrinsic categorical criterion that guarantees recursivity directly from the coalgebra type, eliminating ad-hoc termination proofs for a class of recursive algorithms. The complete machine-checked formalization in Cubical Agda and the explicit preservation condition on the functor constitute a strong, reproducible contribution that unifies existing termination methods under a single abstract setup.

minor comments (2)
  1. [§3] §3, definition of well-founded functor: the preservation condition is stated clearly but the surrounding prose could explicitly flag that it is an additional hypothesis on the functor rather than a derived property.
  2. [Case studies] Case-study sections: the Agda code excerpts are helpful, yet a short table summarizing which parts of each algorithm are covered by the formalization would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our paper and for recommending acceptance. The summary accurately captures the main contributions: the introduction of well-founded functors on categories of families, the central theorem that every coalgebra for such a functor is recursive, its subsumption of ranking-function techniques, the case studies, and the Cubical Agda formalization.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity; theorem follows from explicit definitions and is machine-verified

full rationale

The central result states that every coalgebra for a well-founded functor (defined via an explicit well-foundedness preservation condition on functors over families indexed by a well-founded relation) is recursive. This is proved directly as a theorem from the stated definitions rather than by construction or tautology. The paper supplies a complete Cubical Agda formalization covering the core theorem and case studies (Quicksort, Euclidean algorithm, CYK), providing independent machine-checked evidence. No load-bearing step reduces to a fitted input, self-citation chain, or renamed ansatz; the derivation remains self-contained against external benchmarks.

Assumptions & free parameters 0 free parameters · 2 assumptions · 1 invented entities

The framework rests on standard category theory (categories, functors, coalgebras) plus the new definition of well-founded functor. No numerical parameters are fitted. The only invented entity is the well-founded functor itself, which is defined rather than postulated with external evidence.

assumptions (2)
  • domain assumption The base category of families is indexed by a well-founded relation.
    Invoked in the definition of the indexed category on which the well-founded functor acts.
  • standard math Standard properties of coalgebras and recursive coalgebras in a category.
    Background from prior coalgebra literature used to state the main theorem.
invented entities (1)
  • well-founded functor
    purpose: A functor on indexed families that preserves well-foundedness so that its coalgebras are automatically recursive.
    Defined in the paper as the central new construction; no independent falsifiable prediction is given beyond the theorem itself.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Intrinsically Correct Algorithms and Recursive Coalgebras." pith.science (2026). https://pith.science/paper/2512.10748

@misc{pith2026251210748,
  author       = {Pith},
  title        = {Pith review of: Intrinsically Correct Algorithms and Recursive Coalgebras},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2512.10748}},
  note         = {Machine review of arXiv:2512.10748}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives

    math.LO 2025-04 unverdicted novelty 4.0 of 10

    Formalizes Bézout's identity, FTA, and Fermat factorization in Minlog with program extraction to Haskell, comparing binary vs unary encodings for performance.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages · cited by 1 Pith paper

  1. [1]

    Jiří Adámek, Stefan Milius, and Lawrence S. Moss. 2025.Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge University Press. doi:10.1017/9781108884112

    work page doi:10.1017/9781108884112 2025

  2. [2]

    2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation

    The Agda Team. 2025.Function Definitions : Dot Patterns — Agda 2.8.0 documentation. https://agda.readthedocs.io/en/ v2.8.0/language/function-definitions.html#dot-patterns

    work page 2025

  3. [3]

    2024.Intrinsically Correct Sorting in Cubical Agda

    Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2024.Intrinsically Correct Sorting in Cubical Agda. doi:10.5281/zenodo.14279034

    work page doi:10.5281/zenodo.14279034 2024

  4. [4]

    Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide. 2025. Intrinsically Correct Sorting in Cubical Agda. InCertified Programs and Proofs (CPP 2025), Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau (Eds.). ACM, 34–49. doi:10.1145/3703595.3705873

    work page doi:10.1145/3703595.3705873 2025

  5. [5]

    2010.Category Theory(2 ed.)

    Steve Awodey. 2010.Category Theory(2 ed.). Oxford Logic Guides, Vol. 52. Oxford University Press

    work page 2010

  6. [6]

    Bird and Oege de Moor

    Richard S. Bird and Oege de Moor. 1997.Algebra of Programming. Prentice Hall

    work page 1997

  7. [7]

    Ana Bove and Venanzio Capretta. 2005. Modelling General Recursion in Type Theory.Mathematical Structures in Computer Science15, 4 (Aug. 2005), 671–708. doi:10.1017/S0960129505004822

    work page doi:10.1017/s0960129505004822 2005

  8. [8]

    Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. 2006. Recursive coalgebras from comonads.Inf. Comput.204, 4 (2006), 437–468. doi:10.1016/j.ic.2005.08.005

    work page doi:10.1016/j.ic.2005.08.005 2006

Show all 27 references
  1. [9]

    Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination.Commun. ACM54, 5 (May 2011), 88–98. doi:10.1145/1941487.1941509

    2011 doi

  2. [10]

    Peter Dybjer. 1994. Inductive Families.Formal Aspects of Computing6, 4 (July 1994), 440–465. doi:10.1007/BF01211308

    1994 doi

  3. [11]

    Adam Eppendahl. 2000. Fixed Point Objects Corresponding to Freyd Algebras. (May 2000)

    2000

  4. [12]

    Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2015. Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, ...

    2015 doi

  5. [13]

    C. A. R. Hoare. 1962. Quicksort.Comput. J.5, 1 (1962), 10–16. doi:10.1093/comjnl/5.1.10

    1962 doi

  6. [14]

    Hopcroft and Jeffrey D

    John E. Hopcroft and Jeffrey D. Ullman. 1979.Introduction to Automata Theory, Languages, and Computation. Addison- Wesley, Reading, MA

    1979

  7. [15]

    Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. 2017. Well-Founded Coalgebras, Revisited.Mathematical Structures in Computer Science27, 7 (Oct. 2017), 1111–1131. doi:10.1017/S0960129515000481

    2017 doi

  8. [16]

    Laurie Kirby and Jeff Paris. 1982. Accessible independence results for Peano arithmetic.Bulletin of the London Mathematical Society14, 4 (1982), 285–293. doi:10.1112/blms/14.4.285

    1982 doi

  9. [17]

    Donald E. Knuth. 1997.The Art of Computer Programming, Volume 2: Seminumerical Algorithms(3rd ed.). Addison- Wesley, Reading, Massachusetts

    1997

  10. [18]

    Xavier Leroy. 2024. Well-Founded Recursion Done Right. InCoqPL 2024: The Tenth International Workshop on Coq for Programming Languages. ACM, London, United Kingdom. https://inria.hal.science/hal-04356563

    2024

  11. [19]

    1998.Categories for the Working Mathematician(2 ed.)

    Saunders Mac Lane. 1998.Categories for the Working Mathematician(2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer

    1998

  12. [20]

    Fokkinga, and Ross Paterson

    Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. 1991. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. InFunctional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings (Lecture Not...

    1991 doi

  13. [21]

    Gerhard Osius. 1974. Categorical Set Theory: A Characterization of the Category of Sets.Journal of Pure and Applied Algebra4, 1 (Feb. 1974), 79–119. doi:10.1016/0022-4049(74)90032-2

    1974 doi

  14. [22]

    Podelski and A

    A. Podelski and A. Rybalchenko. 2004. Transition invariants. InProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.32–41. doi:10.1109/LICS.2004.1319598

    2004 doi

  15. [23]

    Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißmann Parsers and Formal Grammar Theory in Dependent Lambek Calculus

    Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, and Max S. New. 2025. Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus.Agda Formalization of "Intrinsic Verification of 22 Cass Alexandru, Henning Urbat, and Thorsten Wißm...

    2025

  16. [24]

    Bonsangue, and Jan J

    Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. 2013. Generalizing determinization from automata to coalgebras.Logical Methods in Computer Science9, 1 (2013). doi:10.2168/LMCS-9(1:9)2013

    2013 doi

  17. [25]

    1999.Practical Foundations of Mathematics

    Paul Taylor. 1999.Practical Foundations of Mathematics. Cambridge University Press. doi:10.2307/3621547

    1999 doi

  18. [26]

    Henning Urbat and Thorsten Wißmann. 2025. Well-Founded Coalgebras Meet König’s Lemma. arXiv:2507.18539 [cs.LO] https://arxiv.org/abs/2507.18539 To appear in CSL 2026

    2025

  19. [27]

    Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.Proc. ACM Program. Lang.3, ICFP (July 2019), 87:1–87:29. doi:10.1145/3341691 Intrinsically Correct Algorithms and Recursiv...

    2019 doi

Pith tools

Reviewed May 16, 2026 · model on record in the stance chip above.