A characterisation of the least-fixed-point operator by dinaturality

AbstractThe paper addresses the question of when the least-fixed-point operator, in a cartesian-closed category of domains, is characterised as the unique dinatural transformation from the exponentiation bifunctor to the identity functor. We give a sufficient condition on a cartesian-closed full subcategory of the category of algebraic cpos for the characterisation to hold. The condition is quite mild, and the least-fixed-point operator is so characterised in many of the most commonly used categories of domains. By using retractions, the characterisation extends to the associated cartesian-closed categories of continuous cpos. However, dinaturality does not always characterise the least-fixed-point operator. We show that in cartesian-closed full subcategories of the category of continuous lattices the characterisation fails