Coinduction for recursive data types: Partial orders, metric spaces and Ω-categories - Worrell, J (2000)
In this paper we prove coinduction theorems for final coalgebras of endofunctors on categories of partial orders and (generalized) metric spaces. These results characterize the order, respectively the metric, on a final coalgebra as maximum amongst all simulations. As suggested in [15], and motivated by the idea that partial orders and metric spaces are types of enriched category, the notion of simulation is based on the enriched categorical counterpart of relations, called bimodules. In fact, the results above arise as instances of a coinduction theorem, parametric in a quan-tale Ω, applying to final coalgebras of endofunctors on the category of all (small) Ω-categories and Ω-functors. Also, we give a condition under which the operational notion of simulation coincides with the denotational notion of final semantics. © 2000 Published by Elsevier Science B.V.