This is an old revision of the document!

Review of Fixpoints in Semantics

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
- $f(x)=x^2$ the set of fixedpoints is
- $f(x)=3x-6$ has exactly one fixpoint
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

Transitive Closure as Least Fixedpoint

Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation \[

  r^* = \bigcup_{n \ge 0} r^n

\] where $r^0 = \Delta_D$ .

Lemma: Reflexive transitive closure is the least fixpoint of function $f(r) = \Delta \cup r$ , mapping $f : D^2 \to D^2$

Relations and Reachable States Fixpoints

Consider program with single loop:

while (c) {
  s;
}

Using tail recursion, we could rewrite it as procedure p such that

p = if (c) then (s;p) else skip

This can be written as \[

 p = F(p)

\] where

F(p) = if (c) then (s;p) else skip

  f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c}

Any program can be reduced to a loop:

introduce program counter and iterate until it reaches exit point
more generally, can write an interpreter that interprets the program

Recall Relational semantics of procedures.

Collecting Semantics

Particular way of representing and computing sets of reachable, splitting states by program counter.