Tail recursion through universal invariants (Q685396)

Although initial algebra semantics are a powerful denotational tool, they yield programs based on primitive recursion. Tail-recursion is only derived by further, post hoc optimisation. As an alternative to the usual initial list objects, this paper introduces the convergent list objects. The two semantics are shown to be equivalent, but the latter yields tail-recursive programs directly and systematically. The unfolding of a tail-recursive program yields a loop or endomorphism, whose iteration is captured by its categorical colimit, or universal invariant. If the loop converges (roughly speaking, its universal invariant is its fixed object) then this invariant is the semantics of the original program. A list candidate is a convergent list object if all the necessary loops converge.