Categorical fixed point semantics (Q1813970): Difference between revisions

The paper is devoted to the presentation of several fixed point results in a cartesian closed category and in some special cartesian closed categories relevant to computer science. The author begins with Lawvere's fixed point theorem and presents some variants of this theorem. Examples in categories of Scott domains, effective domains, and modest sets, as well as in the effective topos are discussed. The author constructs the least fixed point operator in the category of Scott domains DOM using the ordered natural number object defined as a suitable weakening of the notion of a natural number object. It is also noted that the fixed point operator in DOM can be described as a dinatural transformation. These results are extended to the case of an enriched category over \(\omega\)- cpo's, and the case of effective domains is discussed.