• English only

# Differences

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

 sav08:relational_semantics_of_procedures [2009/05/26 23:02]vkuncak sav08:relational_semantics_of_procedures [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/05/26 23:06 vkuncak 2009/05/26 23:02 vkuncak 2009/05/26 23:01 vkuncak 2009/05/26 22:52 vkuncak 2009/05/26 20:35 vkuncak 2009/05/26 17:59 vkuncak 2009/05/26 17:58 vkuncak 2009/05/26 17:48 vkuncak 2009/05/26 17:45 vkuncak 2009/05/26 17:44 vkuncak 2009/05/26 17:44 vkuncak 2009/05/26 15:50 vkuncak 2009/05/26 15:19 vkuncak 2009/05/26 14:35 vkuncak 2009/05/26 13:59 vkuncak 2009/05/26 13:58 vkuncak 2009/05/26 13:56 vkuncak 2009/05/26 13:37 vkuncak 2009/05/26 13:32 vkuncak 2009/05/26 13:31 vkuncak 2009/05/26 13:20 vkuncak 2009/05/26 13:19 vkuncak 2009/05/26 13:12 vkuncak 2009/05/26 13:09 vkuncak 2009/05/26 13:07 vkuncak 2009/05/26 12:59 vkuncak 2009/05/26 12:50 vkuncak Next revision Previous revision 2009/05/26 23:06 vkuncak 2009/05/26 23:02 vkuncak 2009/05/26 23:01 vkuncak 2009/05/26 22:52 vkuncak 2009/05/26 20:35 vkuncak 2009/05/26 17:59 vkuncak 2009/05/26 17:58 vkuncak 2009/05/26 17:48 vkuncak 2009/05/26 17:45 vkuncak 2009/05/26 17:44 vkuncak 2009/05/26 17:44 vkuncak 2009/05/26 15:50 vkuncak 2009/05/26 15:19 vkuncak 2009/05/26 14:35 vkuncak 2009/05/26 13:59 vkuncak 2009/05/26 13:58 vkuncak 2009/05/26 13:56 vkuncak 2009/05/26 13:37 vkuncak 2009/05/26 13:32 vkuncak 2009/05/26 13:31 vkuncak 2009/05/26 13:20 vkuncak 2009/05/26 13:19 vkuncak 2009/05/26 13:12 vkuncak 2009/05/26 13:09 vkuncak 2009/05/26 13:07 vkuncak 2009/05/26 12:59 vkuncak 2009/05/26 12:50 vkuncak 2008/04/10 13:37 vkuncak 2008/04/10 13:36 vkuncak 2008/04/10 13:35 vkuncak 2008/04/10 12:12 vkuncak 2008/04/09 21:02 vkuncak 2008/04/09 15:31 vkuncak 2008/04/09 15:27 vkuncak 2008/04/09 15:26 vkuncak 2008/04/09 15:22 vkuncak 2008/04/09 11:08 vkuncak 2008/04/09 10:57 vkuncak 2008/04/09 10:57 vkuncak created Line 4: Line 4: In [[Relational Semantics]] for a language without procedures we had semantic function that maps programs to relations In [[Relational Semantics]] for a language without procedures we had semantic function that maps programs to relations - $+ \begin{equation*} r_c : C \to {\cal R} r_c : C \to {\cal R} -$ + \end{equation*} so $r_c(c_1)$ was the relation corresponding to the command $c_1$, and we denote it by $[\![c_1]\!]$. so $r_c(c_1)$ was the relation corresponding to the command $c_1$, and we denote it by $[\![c_1]\!]$. Line 41: Line 41: ​ Suppose we have relation $r_{move}$ describing the meaning of the procedure. By [[Relational Semantics]],​ this procedure should behave similarly as the meanings of commands, so we should have the following equation: Suppose we have relation $r_{move}$ describing the meaning of the procedure. By [[Relational Semantics]],​ this procedure should behave similarly as the meanings of commands, so we should have the following equation: - $+ \begin{equation*} ​r_{move} = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] ​r_{move} = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] -$ + \end{equation*} Denoting the right-hand side by $F(r_{move})$,​ we can write the above as Denoting the right-hand side by $F(r_{move})$,​ we can write the above as - $+ \begin{equation*} ​r_{move} = F(r_{move}) ​r_{move} = F(r_{move}) -$ + \end{equation*} Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by - $+ \begin{equation*} F(t) = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] F(t) = ([\![assume(x>​0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>​0))]\!] -$ + \end{equation*} Note that $F$ is monotonic in its argument, because the operators $\circ$, $\cup$ are monotonic: Note that $F$ is monotonic in its argument, because the operators $\circ$, $\cup$ are monotonic: * $r_1 \subseteq r_2\ \rightarrow\ (r_1 \circ s) \subseteq (r_2 \circ s)$ * $r_1 \subseteq r_2\ \rightarrow\ (r_1 \circ s) \subseteq (r_2 \circ s)$ Line 57: Line 57: * $r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$ * $r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$ Similarly, the function is $\omega$-continuous (see [[sav08:​Tarski'​s Fixpoint Theorem]]). Thus, it has the least fixpoint, and this fixpoint is given by Similarly, the function is $\omega$-continuous (see [[sav08:​Tarski'​s Fixpoint Theorem]]). Thus, it has the least fixpoint, and this fixpoint is given by - $+ \begin{equation*} r_{move} = \bigcup_{n \ge 0} F^n(\emptyset) r_{move} = \bigcup_{n \ge 0} F^n(\emptyset) -$ + \end{equation*} In fact, $F^n(\emptyset)$ represents the result of inlining the recursive procedure $n$ times. Therefore, if $s_0$ is the initial state such In fact, $F^n(\emptyset)$ represents the result of inlining the recursive procedure $n$ times. Therefore, if $s_0$ is the initial state such that the computation in the procedure terminates within $n$ steps, then $(s_0,s) \in F^n(\emptyset)$ iff $(s_0,s) \in r_{move}$. that the computation in the procedure terminates within $n$ steps, then $(s_0,s) \in F^n(\emptyset)$ iff $(s_0,s) \in r_{move}$. In this example, we have In this example, we have - $+ \begin{equation*} ​r_{move} = \{((x,​y),​(x',​y'​).\ (x > 0 \land x'=0 \land y'​=x+y) \lor (x \le 0 \land x'=x \land y'=y) \} ​r_{move} = \{((x,​y),​(x',​y'​).\ (x > 0 \land x'=0 \land y'​=x+y) \lor (x \le 0 \land x'=x \land y'=y) \} -$ + \end{equation*} ===== Multiple Mutually Recursive Procedures ===== ===== Multiple Mutually Recursive Procedures ===== Line 106: Line 106: Now, we turn mutually recursive definition into a simple recursive definition by taking the pair of the meaning of odd and even. We need to find Now, we turn mutually recursive definition into a simple recursive definition by taking the pair of the meaning of odd and even. We need to find relations $r_{even}$, $r_{odd}$ such that relations $r_{even}$, $r_{odd}$ such that - $+ \begin{equation*} ​(r_{even},​r_{odd}) = G(r_{even},​r_{odd}) ​(r_{even},​r_{odd}) = G(r_{even},​r_{odd}) -$ + \end{equation*} where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by: where the function $G : {\cal R}^2 \to {\cal R}^2$ is given by: - $+ \begin{equation*} G(E,O) = G(E,O) = \begin{array}[t]{@{}l@{}} \begin{array}[t]{@{}l@{}} Line 118: Line 118: ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg) ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ E) \bigg) \end{array} \end{array} -$ + \end{equation*} We define lattice structure on ${\cal R}^2$ by We define lattice structure on ${\cal R}^2$ by - $+ \begin{equation*} ​(r_1,​r_2) \sqsubseteq (r'​_1,​r'​_2) \ \mbox{ iff } \ (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2) ​(r_1,​r_2) \sqsubseteq (r'​_1,​r'​_2) \ \mbox{ iff } \ (r_1 \subseteq r'_1) \land (r_2 \subseteq r'_2) -$ + \end{equation*} - $+ \begin{equation*} ​(r_1,​r_2) \sqcup (r'​_1,​r'​_2) = (r_1 \cup r'_1, r_2 \cup r'_2) ​(r_1,​r_2) \sqcup (r'​_1,​r'​_2) = (r_1 \cup r'_1, r_2 \cup r'_2) -$ + \end{equation*} Note that: Note that: - $+ \begin{equation*} ​G(\emptyset,​\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!],​ [\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) ​G(\emptyset,​\emptyset) = ([\![assume(x==0)]\!] \circ [\![wasEven=true]\!],​ [\![assume(x==0)]\!] \circ [\![wasEven=false]\!]) -$ + \end{equation*} - $+ \begin{equation*} ​G(G(\emptyset,​\emptyset)) = ​G(G(\emptyset,​\emptyset)) = \begin{array}[t]{@{}l@{}} \begin{array}[t]{@{}l@{}} Line 139: Line 139: ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,​\emptyset).\_1) \bigg) ([\![assume(x!=0)]\!] \circ [\![x=x-1]\!] \circ G(\emptyset,​\emptyset).\_1) \bigg) \end{array} \end{array} -$ + \end{equation*} where $p.\_1$ and $p.\_2$ denote first, respectively,​ second, element of the pair $p$. where $p.\_1$ and $p.\_2$ denote first, respectively,​ second, element of the pair $p$. Line 151: Line 151: In the example above, we can prove that In the example above, we can prove that - $+ \begin{equation*} ​r_{even} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land ​r_{even} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land - ​(wasEven'​ \leftrightarrow (x \pmod 2 = 0)) + ​(wasEven'​ \leftrightarrow ​((x \mod 2) = 0)) -$ + \end{equation*} - $+ \begin{equation*} ​r_{odd} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land ​r_{odd} = \{((x,​wasEven),​(x',​wasEven'​).\ x \ge 0 \land x' = 0 \land - ​(wasEven'​ \leftrightarrow (x \pmod 2 \ne 0)) + ​(wasEven'​ \leftrightarrow ​((x \mod 2) \ne 0)) -$ + \end{equation*} === Remark === === Remark ===