LARA

Differences

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

Link to this comparison view

sav08:review_of_fixpoints_in_semantics [2008/04/30 11:05]
vkuncak 		sav08:review_of_fixpoints_in_semantics [2015/04/21 17:30]
Line 1: Line 1:
-====== 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 
-\[ 
-    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 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.