On the foundations of final semantics: Non-standard sets, metric spaces, partial orders

Abstract

Canonical solutions of domain equations are shown to be final coalgebras, not only in a category of non-standard sets (as already known), but also in categories of metric spaces and partial orders. Coalgebras are simple categorical structures generalizing the notion of post-fixed point. They are also used here for giving a new comprehensive presentation of the (still) non-standard theory of non-well-founded sets (as non-standard sets are usually called). This paper is meant to provide a basis to a more general project aiming at a full exploitation of the finality of the domains in the semantics of programming languages — concurrent ones among them. Such a final semantics enjoys uniformity and generality. For instance, semantic observational equivalences like bisimulation can be derived as instances of a single ‘coalgebraic’ definition (introduced elsewhere), which is parametric of the functor appearing in the domain equation. Some properties of this general form of equivalence are also studied in this paper.