Solving reflexive domain equations in a category of complete metric spaces

Abstract

This paper presents a technique by which solutions to reflexive domain equations can be found in a certain category of complete metric spaces. The objects in this category are the (non-empty) metric spaces and the arrows consist of two maps: an isometric embedding and a non-distance-increasing left inverse to it. The solution of the equation is constructed as a fixed point of a functor over this category associated with the equation. The fixed point obtained is the direct limit (colimit) of a convergent tower. This construction works if the functor is contracting, which roughly amounts to the condition that it maps every embedding to an even denser one. We also present two additional conditions, each of which is sufficient to ensure that the functor has a unique fixed point (up to isomorphism). Finally, for a large class of functors, including function space constructions, we show that these conditions are satisfied, so that they are guaranteed to have a unique fixed point. The techniques we use are so reminiscent of Banach's fixed-point theorem that we feel justified to speak of a category-theoretic version of it.