Guarded induction on final coalgebras
Duško Pavlović · Electronic Notes in Theoretical Computer Science · 1998
We make an initial step towards a categorical semantics of guarded induction. While ordinary induction is usually modelled in terms of the least fixpoints and the initial algebras, guarded induction is based on the unique fixpoints of certain operations, called guarded, on the final coalgebras. So far, such operations were treated syntactically [3,8,9,23]. We analyse them categorically. Guarded induction appears as couched in coinductively constructed domains, but turns out to be reducible to coinduction only in special cases. The applications of the presented analysis span across the gamut of the applications of guarded induction — from modelling computation to solving differential equations. A subsequent paper [26] will provide an account of some domain theoretical aspects, which are presently left implicit.