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 10:18]
vkuncak 		sav08:review_of_fixpoints_in_semantics [2015/04/21 17:30]
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 ===== 
- 
-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$ 
- 
-===== Relations and Reachable States Fixpoints ===== 
- 
-Consider program with single loop: 
-  while (c) { 
-    s; 
-  } 
- 
-Using tail recursion, we could rewrite it as 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 
- 
-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 
- 
-===== Collecting Semantics ===== 
- 
-Particular way of representing and computing sets of reachable, splitting states by program counter.