Semantics of recursive procedures (with C.S.Scholten)

Semantics of recursive procedures

We recall that the semantics of the repetition

DO: do $B \rightarrow S$ od

is most compactly expressed in terms of the predicate transformer $f$ given by

f o r a l l X [ f X \equiv (B \wedge w p (S, X)) \vee (¬ B \wedge R) ]

The traditional expression for $wp(DO, R)$ , viz.

(\exists i: i ≥ 0: f ^ {i} \mathrm {f a l s e}) , \tag {0}

is valid in the absence of unbounded nondeterminacy: it is satisfied by those initial states in which DO establishes R in a bounded number of repetitions. In the presence of unbounded nondeterminacy, (0) has that same meaning; the initial states in which DO establishes R in a (possibly unbounded) number of repetitions then satisfy the strongest solution of

X: [ f X \equiv X ] . (1)

(In the absence of unbounded nondeterminacy, $p$ is or-continuous,as a result of which (0) equals the strongest solution of (1).)

We mentioned the above since the definition of $p$ has been inspired by the intended semantic equivalence of $D$ and its first unfolding:

i f B \rightarrow S; D O ∥ ¬ B \rightarrow s k i p F i

Viewed as a recursive definition of $\mathbf{J}\mathbf{O}$ ,the above unfolding is a so-called "tail recursion". We can always deal with tail recursion, using an equation of form (1), i.e. an equation in predicates.

We now turn our attention to the more general case of recursion, as exemplified by

\begin{array}{r l}{\mathrm {R E C}}&{= \mathrm {i f} B \rightarrow S _ {0}; \mathrm {R E C}; S _ {1}; \mathrm {R E C}; S _ {2}}\&{∥ \mathrm {T B} \rightarrow S _ {3}}\&{∥ .}\end{array}

In this case, $w p\left( {R E C,\pi }\right)$ has to be a solution of the equation

\begin{array}{l} h: (\underline {{A}} \mathbb {R}:: [ h \mathbb {R} \equiv \ (B \wedge w p (S _ {0}, h w p (S _ {1}, h w p (S _ {2}, R)))) \vee \ ([ B ∧ w p (S _ {3}, R) ]) \ \end{array}

i.e. an equation with a predicate transformer as un- known, and hence of a shape very different from that of (1).

Our purpose is to show how $wp(REC, R)$ can be defined by an equation very similar to (1). To this end we only have to generalize the notion of a single predicate to structures of predicates, such as pairs, triples, sequences, trees of constant multiplicity, etc. Before we can relate recursive definitions to equations in such predicate structures, we have to do some groundwork.

In the following all predicates of a structure are defined on the same space. For equally shaped predicate structures $X$ and $Y$ , $¬ X, X \vee Y, X \wedge Y, X \equiv Y, X ⇒ Y$ stand for predicate structures of the same shape, the logical operations being performed elementwise over the structure. Universal quantification as denoted by square brackets - as in $[X ⇒ Y]$ - is understood to be extended over all elements of the structure.

Note that the above is consistent with an alternative view of a structure of predicates on some space S, viz. as a single predicate on the cartesian product of S and the space of the anonymous coordinate that distinguishes between the elements of the struc-ture. Though this alternative view will not be the pre-dominant one, it will be used whenever convenient, for instance to justify an appeal to the Theorem of Knaster-Tarski in order to prove the existence of strongest solutions of equations in predicate struc-tures.

For convenience, we extend the domain of any function $f$ defined on predicates to any structure of such predicates: for $X$ such a predicate structure, $P X$ stands for the identically shaped structure of the corresponding function values.

Notational Remark. We would like to draw attention to the anonymity of the coordinate that distinguishes between the elements of a structure. In the case of a

sequence, we do not refer to two successive elements as " $x_{i}$ and $x_{i + 1}$ ", but to the heads of a sequence and of its tail respectively. Instead of the single "+" we now need the two Functions "head" and "tail"; for the general tree-shaped structure we shall use the analogyos "root" and "sontrees" -for a precise definition, see later-. We believe, however, the cost of introducing these functions well-spent: they seem to contribute sig-nificantly to brevity. (End of Notational Remark.)

We assume the reader familiar with "pairs," "triples", and "m-tuples" in general. In the sequel these will always be considered ordered.

An infinite sequence of elements is a pair (head, tail) in which

(1) head is an element , and (ii) fail is an infinite sequence of elements.

Similarly, an infinite m-tree of elements is a pair (root, sontrees) in which

(i) root is an element (ii) Sontrees is an m-tuple of infinite m-trees of elements.

Since all our sequences and m-trees in the sequel will be infinite, the adjective "infinite" will be omitted.

Note. By identifying single elements with 1-tuples, we identify sequences with 1-trees. (End of Note.)

The above introduced some special predicate structures that we shall encounter later. Our first lemmata pertain to predicate structures of any shape.

Lemma 0. Let $X$ and $Y$ range over predicate structures of given shapes; let $b$ be a boolean function such that $bXY$ is defined for all $X, Y$ and such that the equation

(X, Y): b \times Y \tag {2}

has a strongest solution; let $\left( {{X}{s},{Y}{s}}\right)$ be the strongest solution of (2). Then, ${X}_{S}$ is the strongest solution of

Proof. true. $\equiv \left{ {\left( {{X}{s},{Y}{s}}\right) \text{ is a solution of }\left( 2\right) }\right}$ b Xs Ys $⇒ \left{ \begin{array}{l} \text{predicate calculus}\ \left( {EY}\right) : b{X}{S}Y) \end{array}\right.$ , hence, ${X}{S}$ is a solution of (3).

for any $X$ we observe

$⇒ \left{ {\left( {{X}{s},{Y}{s}}\right) \text{ is the strongest solution of }\left( 2\right) }\right}$ $⇒$ {predicate calculus} $\left\lbrack {{X}_{S} ⇒ X}\right\rbrack$ ,

hence $Xs$ is at least as strong as any solution of (3). (End of Proof.)

Remark. With $X$ and $Y$ structures of predicates, $(X,Y)$ is again a structure of predicates, of which the pair $(X,Y)$ represents a dichotomy. But such a dichotomy is far from unique. For instance, if $X$ and $Y$ are both m-trees (with the same value for $m$ ), $(X,Y)$ is a pair of m-trees of predicates. That total structure -which by the way is also an m-tree of predicate pairs - could be partitioned very differently, e.g. the root of one of the trees versus the rest.

A consequence of the above is that Lemma 0 can be applied in all sorts of ways when (Xs,Ys,Zs) is the strongest solution of an equation of the form (X,Y,Z): bXYZ

Zs is the strongest solution of $Z : \left( {{\underline{E}}X,{Y}_{1} : {bX}YZ}\right)$ but also

$\left( {{X}{s},{Z}{s}}\right)$ is the strongest solution of $\left( {X,Z}\right) : \left( {{EY} : b{X}^{\prime }YZ}\right) .$ (End of Remark.)

Lemma 1. Let $X$ and $Y$ range over predicate structures of given shapes; let $f_{X}$ and $f_{Y}$ be doubly monotonic functions such that $f_{X}X_{Y}$ is of the shape of $X$ and $f_{Y}XY$ is of the shape of $Y$ .

Let $g \in$ be the strongest solution of

let $X$ s be the strongest solution of

X: [ f _ {X} X (g X) \equiv X ] ; (5)

then $\left( {{X}{s},g{X}{s}}\right)$ is the strongest solution of

(X, Y): ([ f _ {X} \times Y = X ] \wedge [ f _ {Y} \times Y = Y ]) . (6)

Proof. Since -see EWD85g-2 - structures of predicates can be viewed as predicates, and $\rho_{\mathcal{Y}}$ is monotonic in its second argument, Knaster-Tarshi is applicable and $gX$ exists. Furthermore -by Lemma 2 of EWD84ga-, $g$ is monotonic. Hence $f_{X}X(gX)$ , $f_{X}$ being doubly monotonic, is a monotonic function of $X$ and -Knaster-Tarshi again-Xs exists.

Substituting $\left( {{X}{s},g{X}{s}}\right)$ in (6) we observe

[ f _ {x} X _ {s} (g X _ {s}) \equiv X _ {s} ] \wedge [ f _ {y} X _ {s} (g X _ {s}) \equiv g X _ {s} ]

equiv $\left{ {{\text{defin}}{1}\text{ions of}{X}{s}and{p}^{2}g\text{respectively}}\right}$

true A true

hence $\left( {{X}{s},g{X}{s}}\right)$ is a solution of (6). In order to show that it is the strongest solution of (6) we observe for any $X$ and $Y$

[ f _ {X} X Y \equiv X ] \wedge [ f _ {Y} X Y \equiv Y ]

$⇒$ {definition of } g as strongest solution $}$

[ f _ {X} \times Y = X ] \wedge [ g X ⇒ Y ]

$⇒ { {f}_{x}$ is monotonic in its second argument $}$

[ p _ {X} X (g X) ⇒ X ] \wedge [ g X ⇒ Y ]

$⇒$ {definition of} $X$ s as strongest solution,and Knaaster-Tarski;

[ X _ {s} ⇒ X ] ^ {\wedge} [ g X ⇒ Y ]

$⇒ { a}$ is monolonic $}$

[ X _ {s} ⇒ X ] ∧ [ g X _ {s} ⇒ Y ]. \qquad (E n d o f P r o o p.)

Note. Equation (6) is of the form $z : \left\lbrack {{fz} \equiv z}\right\rbrack$ , with the predicate structure $Z$ partitioned as(X,Y). (End of Note.)

We use the above two lemmata to prove the more specific Lemma 2. Let $f_{X}, f_{Y},$ and $f_{Z}$ be multiply monotonic; let $g_{XY}$ be the strongest solution of

Z: [ f _ {2} \times Y Z \equiv Z ] \tag {7}

Then, the strongest solutions of the equations

\begin{array}{l} X: (E Y, Z:: [ f _ {X} X Y Z \equiv X ] \wedge [ f _ {Y} X Y Z \equiv Y ] \wedge [ f _ {Z} X Y Z \equiv Z ]) (8) \ X: (\underline {{E}} Y:: [ f _ {x} \times Y (g \times Y) \equiv X ] \wedge [ f _ {y} \times Y (g \times Y) \equiv Y ]) (g) \ \end{array}

are equal.

Proof. Let $X$ be the $X$ -component of the strongest solution of

(X, Y, Z): ([ f _ {X} X Y Z \equiv X ] \wedge [ f _ {Y} X Y Z \equiv Y ] \wedge [ f _ {Z} X Y Z \equiv Z ])

According to Lemma 0, Xs is the strongest solution of equation (8). According to Lemma 1 and (7), Xs is the X-component of the strongest solution of

(X, Y): ([ p _ {X} \times Y (g \times Y) \equiv X ] \wedge [ p _ {Y} \times Y (g \times Y) \equiv Y ])

hence, according to Lemma 0, Xs is the strongest solution of equation (g) (End of Proof.)

Our next lemma plays a central role: it deals with equations in $m$ -trees of predicates. In order to formu

late it succinctly, we introduce the following standard functions on m-trees. For m-tree X (m≥1)

\begin{array}{l} r X = (\mathrm {t h e r o o t o f} X) \ s X = (\mathrm {t h e s o n t r e e s} \circ f X) \ r s X = r (s X) \ \end{array}

With X an m-tree of "things" - predicates, predicate pairs, structures - the value of rX is a "thing"; the value of sX can be parsed in two ways: either as an m-tuple of m-trees of "things", or as an m-tree of m-tuples of "things"; in either interpretation the value of rsX is an m-tuple of "things" -usually referred to as "the sons of the root of X".

Warning. Above, the function root, primarily defined for a tree has been considered defined for an m-tuple of trees, viz. the m-tuple of the corresponding roots; the extension is in the vein of the extension of the domain of a predicate transformer as mentioned near the bottom of EWD85g-2. In the case of a function primarily defined on a structure of some type - such as "root"- a word of caution is in order since we may have structures of structures. Let $f$ be defined on "A-structures" but not on "B-structures"; then $fX$ is defined for an $X$ that can be equally well regarded as an A-structure of B-structures or a B-structure of A-structures; the value of $fX$ is independent of the view taken. With an $p$ applicable to both structures - e.g. because they are the

same - two values would be possible; if the case arises, we shall make the value of $f\left( x\right)$ dependent on the parsing of $X$ such that the root of a 4-tree of 5-trees is a 5-tree.

It could -and very probably should- be argued that in a context in which this case arises, even if only once, the silent identification of an $A$ -structure of $B$ -structures with a $B$ -structure of $A$ -structures is a methodological mistake. We shall see to it that in this note the case does not arise. (End of Warning.)

Next we define on $m$ -trees the relation sub by defining $Y$ sub $X$ - read: " $Y$ is a subtree of ${X}^{\prime \prime }$ - as follows:

(i) $X$ sub $X$ (ii) $Y$ sub $X $ for each $Y$ that is an element of $s$ (iii) relation sub is transitive (sub is the strongest relation satisfying the above.

For the above functions we mention a few consequences of the convention to extend the domain of a predicate transformer to structures of predicates. For a predicate transformer and $X$ and $Y$ m-trees of predicates we have

[ r (f X) \equiv f (r X) ] \tag {10}

[ s (f X) \equiv f (s X) ] \tag {n}

(Y \underline {{\operatorname {s u b}}} X) ⇒ (f Y \underline {{\operatorname {s u b}}} f X) \tag {12}

In the sequel we shall be interested in the strongest solution of equations in predicate transformers; we define "predicate transformer $g$ is at least as strong as predicate transformer $h$ " to mean "[gR] for all $R$ ".

After the above, we are ready to formulate and prove

Theorem 0. Let $(p,q)$ be a doubly monotonic function on (predicates $x$ m-tuples of predicates) to that same space; let $X,Y,U,$ and $V$ range over $m$ -trees of predicates; let predicate transformer $g$ be defined by

$\left\lbrack {gR \equiv \left( {\text{the root of the }\mathrm{X}\text{-component of the strongest}}\right) }\right.$ solution of (13))], for all $R$ ,with (13)

given by

\begin{array}{l} (X, Y): ([ r Y \equiv R ] \wedge \tag {13} \ (A (U, V): (U, V) \underline {{s u b}} (X, Y): \ [ r U \equiv p (r V) (\overline {{r s}} U) ] \wedge [ r s V \equiv q (r V) (\overline {{r s}} U) ]) \ \end{array}

Then $g$ is the strongest solution of

h: (\underline {{A R}}: (\underline {{E Z}}: [ h \mathcal {R} \equiv p \mathcal {R} (h Z) ] \wedge [ Z \equiv q \mathcal {R} (h Z) ]) \rangle , (k)

where $Z$ ranges over $m$ -tuples of predicates. (Note that in the boolean expression $\left( {U,V}\right)$ sub $\left( {X,Y}\right)$ both sides have to be considered $m$ -trees of predicate pairs.)

Proof. For brevity's sake we introduce "cUV" as

[ r U \equiv p (r V) (r s U) ] \wedge [ r s V \equiv q (r V) (r s U) ]

This abbreviation reduces (13) to the form

(X, Y): ([ r Y \equiv R ] \wedge (\underline {{A}} U, V: (U, V) \underline {{\operatorname {s u b}}} (X, Y): c U V)) . (1 3 ^ {\prime})

To begin with, we have to show that this equation has a strongest solution. To this end we note that (13) is of the form $(X,Y):[f(X,Y)\equiv (X,Y)]$ with monotonic $f$ (and $R$ as parameter):

thanks to the first term of c UV, each root of a subtree of X - i.e. each predicate occurring in X - is given as a monotonic function of X and Y; hence X is a monotonic function of (X,Y);

thanks to the second term of cUV, all predicates in Y, except rY, which is the constant R, are given as monotonic functions of X and Y; hence Y is a monotonic function of (X,Y);

hence $\left( {X,Y}\right)$ is a monotonic function of(X,Y). As a result,(13) has a strongest solution.

We shall first show that $g$ is a solution of (14). To this end we observe for any $R$

true

\begin{array}{l} = {d e f i n i t i o n o f g } \ [ g \dot {R} \equiv r (X - c o m p o n e n t o f s t r a n g e s t s o l u t i o n o f (1 3)) ] \ = {\mathrm {L e m m a} o } \ \left[ g R \equiv r (\mathrm {t h e s t r o n g e s t s o l u t i o n o f} \right. \ X: (\underline {{E}} Y:: [ r Y \equiv R ] \wedge (\underline {{A}} (U, V): (U, V) _ {\mathrm {s u b}} (X, Y); c U V))) ] \ = {\mathrm {L e m m a} 0, \mathrm {w i t h} X \mathrm {d e c o m p o s e d a s} (P, X ^ {\prime}) \mathrm {a n d} Y \mathrm {d e c o m p o s e d a s} (X ^ {\prime}, P) }. \ p o s e d a s (R, Y ^ {\prime}) w i t h X ^ {\prime} a n d Y ^ {\prime} m - h u p l e s o f m - t r e e s \ \end{array}

-i.e. $s \in$ and $s$ Y respectively- $}$

[{g}_{R} \equiv ]

P: (E X ^ {\prime}, Y ^ {\prime}: (\underline {{A}} (U, V): (U, V) \underline {{s u b}} ((P, X ^ {\prime}), (R, Y ^ {\prime})): c U V)) ]

$= { 1\left( {U,V}\right)$ sub $\left( {{X}^{\prime },{Y}^{\prime }}\right)$ meaning that(U,V),viewed as tree of predicate pairs, is a subtree of one of the trees of predicate pairs occurring in the m-tuple of trees $\left( {{X}^{\prime },{Y}^{\prime }}\right)$ , and the definition of $c}$

[{gR} \equiv {the}]

P: (E X ^ {\prime}, Y ^ {\prime}: \tilde {[} P \equiv p R (r X ^ {\prime}) ] \wedge [ r Y ^ {\prime} \equiv q R (r X ^ {\prime}) ] \wedge

(A U, V: (U, V) \underline {{\operatorname {s u b}}} (X ^ {\prime}, Y ^ {\prime}): c U \dot {V})) ]

$= {$ predicate calculus; 2 ranges over $m$ -tuples of predicates $}$ ${gR} \equiv$ the strongest solution of

P: (E X ^ {\prime}, Y ^ {\prime}, Z:: [ P \equiv p R (r X ^ {\prime}) ] \wedge [ Z \equiv g R (r X ^ {\prime}) ] \wedge

[ r Y ^ {\prime} \equiv Z ] \wedge (\underline {{A}} U, V: (U, V) \underline {{\operatorname {s u b}}} (X ^ {\prime}, Y ^ {\prime}): c (U V)) ]

$= \left{ \begin{array}{l} \text{ the roles of }X,Y,andZ \in \text{ Lemma 2 are played by } \ P,Z,{\left( {X}^{\prime },{Y}^{\prime }\right) }_{\text{ from the above , in that order; the }} \end{array}\right.$ bottom line of the above is, apart from the replace-

ment of predicates by m-luples of predicates, of the

[ g Z \equiv r (\mathrm {t h e} X \mathrm {- c o m p o n e n t o f t h e s t r a n g e s t s o l u t i o n}

o f (1 3 ^ {\prime}) w i t h R, X, Y r e p l a c e d b y Z, X ^ {\prime}, Y ^ {\prime}) ] }

[{I}_{g}R \equiv {the}]

P: (E Z:: [ P \equiv p R (g Z) ] ∧ [ Z \equiv q R (g Z) ]) ]

$⇒ {$ predicate calculus

(\exists Z: [ g R \equiv p R (g Z) ] ∧ [ Z \equiv q R (g Z) ])

in other words, $g$ is a solution of (14)

Note: The equation

(X ^ {\prime}, Y ^ {\prime}): ([ r Y ^ {\prime} \equiv Z ] ∧ (\underline {{A}} U, V: (U, V) _ {s u b} (X ^ {\prime}, Y ^ {\prime}): c U V))

is a conjunction of $m$ equations like (13'). (End of Note.)

Finally we show that $g$ is at least as strong as any solution of (14). For any $h$ satisfying (14) we observe

t r u e

= {(1 4) }

(\underline {{A}} R: (\underline {{E}} Z: [ h R \equiv p R (h Z) ] \wedge [ Z \equiv q R (h Z) ]))

$= \left{ {\text{the existence of an }\mathrm{m} - \text{tuple}\mathrm{Z}\text{for each}\mathrm{R}\text{satisf.}}\right.$ Flying b R Z equivales the existence of an $m$ -tree $Y$ with arbitrary root with $b$ holding all along the free $}$

(\underset {\sim} {A} \mathcal {R}: (\underset {\sim} {E} \mathcal {Y}: [ r Y \equiv \mathcal {R} ] \wedge

(A V: V _ {s u b} Y:

[ h (r V) \equiv p (r V) (h (r s V)) ] \wedge

[ r s V \equiv q (r V) (h (r s V)) ] ])

= {(1 0) a n d (1 1) }

(A R: C E Y: [ r Y \equiv R ] ∧

(A V: V _ {\mathrm {s u b}} Y:

[ r (h V) \equiv p (r V) (r s (h V)) ] \wedge

[ r s. V \equiv q (r V) (r s (h V)) ]))))

$= \left{ \begin{array}{l} \text{since the range}"y\text{sub} Y ∧ \left\lbrack {U \equiv hV}\right\rbrack \text{" is for }\left( {U,V}\right) \ \text{the same one as the range "}\left( {U,V}\right) \underline{\text{sub}}\left( {hY,Y}\right) \end{array}\right}$

(\underline {{A}} \cdot \underline {{R}}: (\underline {{E}} \cdot \underline {{Y}}: [ r \cdot Y \equiv \overline {{B}} ] \wedge

(\underline {{A}} U, V: (U, V) \underline {{\operatorname {s u b}}} (h Y, Y):

[ r U \equiv p (r V) (r s U) ] ∧

[ r s V \equiv q (r V) (r s U) ]))))

⇒ {\mathrm {d e f i n i t i o n} g R }

(\underline {{A}} \overline {{R}}: (\underline {{E}} Y: [ \overline {{r}} Y \equiv \overline {{R}} ] \wedge [ g \overline {{R}} ⇒ r (h Y) ])

= {(1 0) a n d p r e d i c a t e c a l c u l u s }

(\underline {{A}} R: [ g R ^ {\prime} ⇒ h R ])

(E n d o f P r o o f.)

In Theorem 0, the sole purpose of (13) - and the whole apparatus of m-trees of predicates, etc. - was to prove that (14) is solvable and has a strongest solution. We are interested in (14) because it reflects what is to be expected of a recursively defined predicate transformer. To illustrate this we return to the example of REC as given on EWD85g-1.

To this purpose we rephrase:

\begin{array}{l} [ h R \equiv (B \wedge w p (S _ {0}, h w p (S _ {1}, h w p (S _ {2}, R))) ] \vee \ (¬ B ∧ w p (S _ {3}, R)) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , i n t r o d u c i n g t h e d u m m y p r e d i c a t e s} Z 0 \mathrm {a n d} Z 1 } \ (E Z o, Z 1:: \ [ h R \equiv (B \wedge w p (S _ {0}, h Z _ {0})) \vee (7 B \wedge w p (S _ {3}, R)) ] \wedge \ [ z _ {0} \equiv w p (S _ {1}, h; Z _ {1}) ] \wedge [ z _ {1} \equiv w p (S _ {2}, R) ]) \ \end{array}

with $z = \left( {{Z}{0},{Z}{1}}\right)$ -and,as usual, $h z = \left( {h {Z}{0},h {Z}{1}}\right)$ - the two lines are of the forms

[ h R \equiv p R (h Z) ] a n d

[ Z \equiv q R (h Z) ] r e s p e c i v e l y, w i t h

obviously monotonic $p$ and 9 . With $m$ internal calls of REC the above procedure leads to an m-tuple $Z$ and the corresponding equation (13) is an equation in $m$ -trees.

The above procedure works for a body without calls of REC inside a repetition. Since each repetition can be written as a tail-recursion, the occurrence of REC inside a repetition can be viewed as

a special case of mutual recursion. In the case of n mutually recursive procedures we define a predicate transformer h such that h R stands for an n-tuple of predicates, viz. with one component for each procedure. Note that the corresponding value of m equals the sum of the numbers of internal calls occurring in the n bodies.

11 November 1983

drs. C.S. Schohen

Scientific Adviser

Philips Research Laboratories

5600 JA EINDHOVEN

The Netherlands

prof.dr.Edsger W.Dyksra

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

The Netherlands