A characterization of the least-fixed-point operator by dinaturality (Q685386)

The 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.