Constructive fixed-point theorems where finite iteration yields the fixed point

120 Views Asked by At

I would like to show that $p$, a fixed point of some effective map $f : S\rightarrow S$, can be constructed effectively. Ideally, I would like there to exist a finite $n$ such that $p = f^n(p_0)$, where $p_0$ is a point in the domain of $f$.

What fixed-point theorem yields such a statement? What are the conditions that $f$ and ${\rm dom}\ f$ must satisfy for the theorem to hold?

I would find order-theoretic fixed-point theorems useful, but other kinds of fixed-point theorem are welcome.

1

There are 1 best solutions below

2
On

Tarski's fixed point theorem will give you just what you're looking for if the function is order-preserving and its domain is a complete lattice.