On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces

Abstract

This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle , which pervades modern mathematics, and a dual, non-standard ‘ coinduction principle ’, which underlies many of the recursive phenomena occurring in computer science. The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.