Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:relational_semantics_of_procedures [2009/05/26 23:02] vkuncak |
sav08:relational_semantics_of_procedures [2015/04/21 17:30] (current) |
||
---|---|---|---|
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: | ||
</code> | </code> | ||
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 === |