Differences

This shows you the differences between two versions of the page.

--- sav08:review_of_fixpoints_in_semantics [2008/04/30 10:18]
vkuncak
+++ sav08:review_of_fixpoints_in_semantics [2008/04/30 11:05]
vkuncak
@@ Line 1: / Line 1: @@
 ====== 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 =====
@@ Line 25: / Line 11: @@
 **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 =====
+===== Meaning of Recursive and Iterative Constructs as Fixpoints of Relations =====
 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
@@ Line 43: / Line 29: @@
   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 meaning 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
 \[
     f(r) = (\Delta_c \circ r_s \circ r) \cup \Delta_{\lnot c}
@@ Line 59: / Line 50: @@
   * relation does not always represent terminating computation
-===== Collecting Semantics =====
+===== 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 constraints:
+\[
+  I \subseteq C(p_0)
+\]
+\[
+  \bigwedge_{(p_1,p_2) \in E} sp(C(p),r(c(p_1,p_2)))) \subseteq C(p_2)
+\]
+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.
-Particular way of representing and computing sets of reachable, splitting states by program counter.