Foundations of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders

摘要

Canonical solutions of domain equations are shown to be 'final coalgebras', notonly in a category of nonstandard 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) nonstandard 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. 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.