A fixed point operator in a cartesian monoidal category, or more generally a cartesian multicategory is a structure on a category that models that every object of the category has the fixed point property?, i.e., every endomorphism in the category has a fixed point.
In denotational semantics of programming languages, these can be used to model recursive definitions.
There are several equivalent formulations in the literature, here we present the definition that is most useful (parameterized) and general (multicategorical): that of parameterized fixed point operators in cartesian multicategories.
A parameterized fixed point operator on a cartesian multicategory $M$ is a family of functions $fix \colon M(\Gamma,X;X) \to M(\Gamma;X)$ satisfying:
Note that picking $g$ to be the identity in (2) implies the fixed point property: for any $f \in M(\Gamma,X;X)$, $f \circ fix(f) = fix(f)$.
A parameterized fixed-point operator is equivalent to a trace structure on a cartesian monoidal category.
For a Lawvere theory, a fixed-point operator is the same thing as the structure of an Conway theory.
Masahito Hasegawa, Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi, TLCA 1997 doi
Alex Simpson and Gordon Plotkin, Complete Axioms for Categorical Fixed-Point Operators, LICS ‘00, doi
Last revised on November 26, 2022 at 04:45:06. See the history of this page for a list of all contributions to it.