# Review of Fixpoints in Semantics

## Transitive Closure as Least Fixedpoint

Recall the definition of transitive closure for a binary relation

where .

**Lemma:** Reflexive transitive closure is the least fixpoint of function , mapping

## 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

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
- look for solution of , which contains twice, so it expresses recursion
- we can abstract the question of existence of values of recursive functions using fixpoints

If is meaning of and is meaning of *assume( c )*, the meaning is the fixpoint of function

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 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 , edges and for each edge a command , with initial and final node

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**.

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

For each program point , we have the set of reachable states .

The set of all reachable states of the program is .

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

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

where is command associated with edge , and is the relation giving semantics for this command.