LARA

Review of Fixpoints in Semantics

Transitive Closure as Least Fixedpoint

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

\begin{equation*}
    r^* = \bigcup_{n \ge 0} r^n
\end{equation*}

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

\begin{equation*}
   p = F(p)
\end{equation*}

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

\begin{equation*}
    f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c}
\end{equation*}

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 states, 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 constraints:

\begin{equation*}
  I \subseteq C(p_0)
\end{equation*}

\begin{equation*}
  \bigwedge_{(p_1,p_2) \in E} sp(C(p),r(c(p_1,p_2)))) \subseteq C(p_2)
\end{equation*}

where $c(p_1,p_2)$ is command associated with edge $(p_1,p_2)$, and $r(c(p_1,p_2))$ is the relation giving semantics for this command.