Post #2669082
2026-04-08 13:16 UTC
What does this buy us? Well, we can make dual use of an indexed setting already present for intrinsic verification of partial correctness
to also prove total correctness, by combining the index with a suitable relation such that it corresponds to a ranking argument. And all this is done at the level of the functor, allowing the separation of recursion behaviour from nonrecursive business logic, in the spirit of structured recursion. 6/8
Replies (1)
-
@cxandru@types.pl 2026-04-08 13:16
The Agda implementation of the main theorem of our paper, as well as a library we wrote for writing recursive algorithms based on coalgebras for well founded functors, can be found at https://git8.cs.fau.de/software/intrinsically-recursive/ . In our paper we show how one can also use our technique for proving recursivity of coalgebras in a non-indexed setting, as well as providing case studies of QuickSort, CYK parsing, and the Euclidean algorithm. 7/8