Fixed-point operations on ccc's. Part I

AbstractMost studies of fixed points involve their existence or construction. Our interest is in their equational properties. We study certain equational properties of the fixed-point operation in computationally interesting cartesian closed categories. We prove that in most of the poset categories that have been used in semantics, the least fixed-point operation satisfies four identities we call the Conway identities. We show that if %plane1D;49E;0 is a sub-ccc of any ccc %plane1D;49E; with a fixed-point operation satisfying these identities, then there is a simple normal form for the morphisms in the least sub-ccc of %plane1D;49E; containing %plane1D;49E;0 closed under the fixed-point operation. In addition, the standard functional completeness theorem is extended to Conway ccc's