Post #2669081
2026-04-08 13:15 UTC
A functor G: ๐I โ ๐I is well founded if for every i โ I there exists a functor $G_{<i}$ s.t.
$โ i โ I. โ X โ ๐I. (G X)i โ
G{<i} (X|{<i})$, where $< i = { j โ I \mid j < i }$
i.e. morally, G is naturally isomorphic to a _family of functors $G_{<i} : (๐{< i} โ ๐)_{i โ I}$ 5/8
Replies (1)
-
@cxandru@types.pl 2026-04-08 13:16
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