Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:review_of_fixpoints_in_semantics [2008/04/29 23:05] vkuncak |
sav08:review_of_fixpoints_in_semantics [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Review of Fixpoints in Semantics ====== | ====== 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 ===== | ===== Transitive Closure as Least Fixedpoint ===== | ||
Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation | Recall the definition of transitive closure for $r \subseteq D \times D$ a binary relation | ||
- | \[ | + | \begin{equation*} |
r^* = \bigcup_{n \ge 0} r^n | r^* = \bigcup_{n \ge 0} r^n | ||
- | \] | + | \end{equation*} |
where $r^0 = \Delta_D$. | 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$ | **Lemma:** Reflexive transitive closure is the least fixpoint of function $f(r) = \Delta \cup r$, mapping $f : D^2 \to D^2$ | ||
- | ===== Reachable States are a Fixpoint ===== | + | ===== Meaning of Recursive and Iterative Constructs as Fixpoints of Relations ===== |
Consider program with single loop: | Consider program with single loop: | ||
Line 32: | Line 18: | ||
} | } | ||
- | Using tail recursion, we could rewrite it as procedure p such that | + | Using tail recursion, we could rewrite it as a procedure p such that |
p = if (c) then (s;p) else skip | p = if (c) then (s;p) else skip | ||
This can be written as | This can be written as | ||
- | \[ | + | \begin{equation*} |
p = F(p) | p = F(p) | ||
- | \] | + | \end{equation*} |
where | where | ||
F(p) = if (c) then (s;p) else skip | F(p) = if (c) then (s;p) else skip | ||
- | If $r_s$ is meaning of $s$ and $\Delta_c$ is meaning of //assume(c)//, the set of reachable states is the fixpoint of function | + | 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} | f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c} | ||
- | \] | + | \end{equation*} |
Any program can be reduced to a loop: | Any program can be reduced to a loop: | ||
Line 52: | Line 43: | ||
* more generally, can write an interpreter that interprets the program | * more generally, can write an interpreter that interprets the program | ||
- | Recall [[Relational semantics of procedures]] | + | 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. | ||