nLab fixed point operator

Contents

Contents

Idea

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.

Definition

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 MM is a family of functions fix:M(Γ,X;X)M(Γ;X)fix \colon M(\Gamma,X;X) \to M(\Gamma;X) satisfying:

  1. (Naturality in Γ\Gamma) For any substitution γ:M(Δ,Γ)\gamma : M(\Delta,\Gamma), fix(f)γ=fix(fγ)fix(f) \circ \gamma = fix(f \circ \gamma)
  2. (Dinaturality in XX) For any f:M(Γ,X;Y)f : M(\Gamma, X;Y) and g:M(Γ,Y;X)g : M(\Gamma,Y;X), fix(fg)=ffix(gf)fix(f \circ g) = f \circ fix(g \circ f)
  3. (Diagonal property) For any f:M(Γ,X,X;X)f : M(\Gamma, X, X; X), fix(fix(f))=fix(f(γ,x,x))fix(fix(f)) = fix(f \circ (\gamma, x,x)) where here the substitution (γ,x,x):M(Γ,X;Γ,X,X)(\gamma, x,x) : M(\Gamma,X;\Gamma,X,X) duplicates the input.

Note that picking gg to be the identity in (2) implies the fixed point property: for any fM(Γ,X;X)f \in M(\Gamma,X;X), ffix(f)=fix(f)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.

References

Last revised on November 26, 2022 at 04:45:06. See the history of this page for a list of all contributions to it.