Existenz von Fixpunkten

Fixpunkt von f : : C→C ist x : : C mit fx = x.

Existenz? Eindeutigkeit? Konstruktion?

Satz: Wenn C pointed CPO und f stetig,
dann besitzt f genau einen kleinsten Fixpunkt.

• CPO = complete partial order = vollständige Halbordnung
• complete = jede monotone Folge besitzt Supremum (= kleinste obere Schranke)
• pointed: C hat kleinstes Element $\bot$
• stetig: x≤y⇒f (x)≤f (y) und für monotone Folgen [x₀, x₁,…] gilt: f (sup[x₀, x₁,…]) = sup[f (x₀), f (x₁),…]

Dann fix(f )= sup[$\bot$, f ($\bot$), f²($\bot$),…]