Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:relational_semantics_of_procedures [2009/05/26 17:59] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 22:52] vkuncak |
||
---|---|---|---|
Line 10: | Line 10: | ||
How can we define semantics for program with recursive procedures? | How can we define semantics for program with recursive procedures? | ||
+ | |||
+ | We consider first the case of procedures without parameters; adding parameters is straightforward. | ||
===== One Recursive Procedure ===== | ===== One Recursive Procedure ===== | ||
Line 60: | Line 62: | ||
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 | ||
+ | \[ | ||
+ | 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) \} | ||
+ | \] | ||
===== Multiple Mutually Recursive Procedures ===== | ===== Multiple Mutually Recursive Procedures ===== | ||
Line 141: | Line 148: | ||
The meaning of all procedures is then the tuple $p_* \in {\cal R}^n$ given by $\bigsqcup\limits_{n \ge 0} G^n(\emptyset,\ldots,\emptyset)$. | The meaning of all procedures is then the tuple $p_* \in {\cal R}^n$ given by $\bigsqcup\limits_{n \ge 0} G^n(\emptyset,\ldots,\emptyset)$. | ||
- | **Remark:** $p_*$ is the least fixpoint of $G$, so by [[sav08:Tarski's Fixpoint Theorem]], it is also the least $p$ such that $G(p) \sqsubseteq p$. Thus, $G(p) \sqsubseteq p$ implies $p_* \sqsubseteq p$. | + | === Example === |
+ | |||
+ | In the example above, we have | ||
+ | |||
+ | === Remark === | ||
+ | |||
+ | $p_*$ is the least fixpoint of $G$, so by [[sav08:Tarski's Fixpoint Theorem]], it is also the least $p$ such that $G(p) \sqsubseteq p$. Thus, $G(p) \sqsubseteq p$ implies $p_* \sqsubseteq p$. | ||