• 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)
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 ===