This is an old revision of the document!

Relational Semantics of Procedures

Let $S$ be the set of states and ${\cal R}$ denote $2^{S\times S}$ , the set of all relations on $S$ .

In Relational Semantics for a language without procedures we had semantic function that maps programs to relations \[

 r_c : C \to {\cal R}

\] so $r_c(c_1)$ was the relation corresponding to the command $c_1$ , and we denote it by $[\![c_1]\!]$ .

How can we define semantics for program with recursive procedures?

One Recursive Procedure

We first illustrate the semantics for one recursive procedure. The definition only relies on the Lattices structure, so it generalizes to recursive definitions with multiple procedures, and recursive definitions in general.

Example: Consider the following procedure that, if $x,y$ are positive, moves the content of x into y.

  var x,y;
  proc move() {
     if (x > 0) {
       x = x - 1;
       move();
       y = y + 1;
     }
  }

or, expressed using non-deterministic choice and assume:

  var x,y;
  proc move() {
     ( assume(x>0);
       x = x - 1;
       move();
       y = y + 1;
     ) 
     [] (assume (!(x>0))
  }

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: \[

 r_{move} = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ r_{move}\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!]

\] Denoting the right-hand side by $F(r_{move})$ , we can write the above as \[

 r_{move} = F(r_{move})

\] Thus, the meaning of the procedure is the fixpoint of function $F : {\cal R} \to {\cal R}$ given by \[

 F(t) = ([\![assume(x>0)]\!]\ \circ\ [\![x=x-1]\!]\ \circ\ t\ \circ\ [\![y=y+1]\!])\ \bigcup\ [\![assume(!(x>0))]\!]

\] 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\ (s \circ r_1) \subseteq (s \circ r_2)$
$r_1 \subseteq r_2\ \rightarrow\ r_1 \cup s \subseteq r_2 \cup s$

Similarly, the function is $\omega$ -continuous (see Tarski's Fixpoint Theorem). Thus, it has the least fixpoint, and this fixpoint is given by \[

  r_{move} = \bigcup_{n \ge 0} F^n(\emptyset)

\] 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}$ .

Multiple Mutually Recursive Procedures

The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions. We have operations $\sqsubseteq$ and $\sqcup$ analogous to $\subseteq$ and $\cup$ (indeed, the domain ${\cal R}^d$ , that is $(2^{S\times S})^d$ , is isomorphic to $2^{S\times S \times \{1,2,\ldots,d\}}$ ).

The meaning of all procedures is therefore 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 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: Tree reversal.