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$

Meaning of Recursive and Iterative Constructs as Fixpoints of Relations

Consider program with single loop:

while (c) {
  s;
}

Using tail recursion, we could rewrite it as a 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

How to give semantics to recursive definitions?

eliminate recursive by denoting left-hand side as the result of non-recursive function $F$
look for solution of $p=F(p)$ , which contains $p$ twice, so it expresses recursion
we can abstract the question of existence of values of recursive functions using fixpoints

If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of assume( c ), the meaning is the fixpoint of function \[

  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.

What is the fixpoint of the recursive function $f(x)=1+f(x)$ mapping integers to integers?

we need ordering to ensure existence of fixpoints
relations have a natural subset ordering
relation does not always represent terminating computation

Reachable States and Collecting Semantics

Main question: What values can variables of the program take at different program points?

We can represent programs by control-flow graphs (CFG).

Definition: Control flow-graph is a graph with nodes $V$ , edges $E \subseteq V\times V$ and for each edge $e \in E$ a command $c(e)$ , with initial $init$ and final node $final$

Program points are CFG nodes. Statements are labels on CFG edges.

We look at a particular way of representing and computing sets of reachable, splitting states by program counter (control-flow graph node): collecting semantics.

$PS$ - the set of values of program variables (not including program counter).

For each program point $p$ , we have the set of reachable states $C(p) \subseteq PS$ .

The set of all reachable states of the program is $\{(p,s) \mid s \in C(p) \}$ .

Let $p_0$ be initial program counter and $I$ the set of values of program variables in $p_0$ .

The set of reachable states is defined as the least solution of: