LARA

Fixpoints

Definition: Given a set $A$ and a function $f : A \to A$ we say that $x \in A$ is a fixed point (fixpoint) of $f$ if $f(x)=x$.

Definition: Let $(A,\le)$ be a partial order, let $f : A \to A$ be a monotonic function on $(A,\le)$, and let the set of its fixpoints be $S = \{ x \mid f(x)=x \}$. If the least element of $S$ exists, it is called the least fixpoint, if the greatest element of $S$ exists, it is called the greatest fixpoint.

Note:

  • a function can have various number of fixpoints. Take $f : {\cal Z} \to {\cal Z}$,
    • $f(x)=x$ the set of fixedpoints is $\mathbb Z$
    • $f(x)=x^2$ the set of fixedpoints is $\{0, 1\}$
    • $f(x)=3x-6$ has exactly one fixpoint: $3$
  • a function can have at most one least and at most one greatest fixpoint

We can use fixpoints to give meaning to recursive and iterative definitions

  • key to describing arbitrary long executions in programs