The operation “trickle”

The operation "frickle"

Consider a directed acyclic graph. Each "arrow" (= di- directed edge) leads from its "source" (= source node) to its "target" (= target node). The targets of the arrows of which $x$ is the source are elliptically called "the targets of $x$ ". Similarly, "the sources of $x$ " are the sources of the arrows of which $x$ is the target. The following three predicates are equivalent for any pair of nodes $x$ and $y$

(i) there exist a non-empty $p$ -th $f\left( {x + y}\right)$ (ii) $x$ is an ascendant of (iii) $y$ is a descendant of

i.e. "being an ascendent of" is the nonreflexive transitive closure of "being a source of", and "being a descendant of" is that of "being a target of".

[The relation "being a descendant of" is a partial order between the nodes. Note that the same partial order can in general be induced by many graphs: graphs may contain arrows that are redundant in the sense that their removal would leave their sources ascendants of their targets. In other words, the directed acyclic graph contains in general more information than the induced partial order.]

Each node $x$ "owns" an integer value v.x. Be-tween sets X and Y the relation "dominates" is defined by

$X$ dominates $Y \equiv \left( {\underline{A}x,y : x \in X \land y \in Y : v.x \geq v.y}\right)$

Identifying a singleton set with its only element, we shall also feel free to state things like "x dominates Y"

"X dominates y" for single nodes $x$ and $y$ . Note

$$ X = \varnothing \vee Y = \varnothing \Rightarrow X d o m i n a t e s Y $$

So far, we only dealt with terminology (and we may not need all of it). We may permute the values owned by the nodes, and, in the usual fashion, we shall confine ourselves to successive moves, a move consisting of two nodes exchanging their values. Our goal is R, given by

R: (A $x : x$ a node: $x$ dominates its targets)

or, equivalently

R: (A $x\colon x$ a node: $x$ dominates its descendants)

I am now not in the mood of proving the equivalence of the above two formulations; it should be a theorem.

Let an "inversion" be defined by

$$ \begin{array}{l} ((x, y) i s a n d i n v e r s i o n) \equiv \ (y \mathrm {i s a d e s c e n d a n t o f} x) \land \neg (x \mathrm {d o m i n a t e s} y) \ \end{array} $$

Does the following program

[\text{d}0 \mid \left\lbrack {p,q : \left( {p,q}\right) \text{ is an inversion } \rightarrow v.p,v.q = v.q,v.p}\right\rbrack \text{ od}]

establish R ? (Here I have used the initializing guard: if the equation has no solution, the guard is false , if the equation can be solved, the guard is true and the unknowns, which are local variables of the block, are initialized so as to solve the equation.

In this generalization, the traditional guard emerges as an equation in zero variables.) Yes, it does, because the repeatable statement decreases the number of inversions.

Proof We only need to consider possible inversions of the form $(x,p), (x,q), (p,y)$ or $(q,y)$ .

If $x$ is an ascendant of $p$ , it is also an ascendant of $q$ and the value exchange between $p$ and $q$ leaves the number of inversions among $(x,p)$ and $(x,q)$ unchanged.

If $x$ is an ascendant of $q$ , but not of $p$ , we observe that, as the exchange decreases v.q, no inversion $(x,q)$ is introduced. For $x = p$ , we even know that an inversion disappears.

For inversions of the form (p,y) or (q,y) the mirror argument holds. (End of Proof.)

Since

$$ \begin{array}{l} (E p, q: (p, q) i s a n i n v e r s i o n) \equiv \ (E p, q: ((p, q) \mathrm {i s a n i n v e r s i o n}) \land (q \mathrm {i s a t a r g e t o f} p)), \ \end{array} $$

our program can confine itself each time to a 9 which is a target of $p$ .

Let us now weaken $\mathcal{R}$ in its second formulation and admit one exceptional node, i.e. let us consider

P: (A $x:: x = p \lor (x$ dominates its descendants))

Since

$$ (p d o m i n a t e s i t s d e c e n d a n t s) \equiv $$

$$ (p d o m i n a t e s i t s t a r g e t s) \land $$

$$ (\underline {{A}} q: q \mathrm {t a r g e t o f} p: q \mathrm {d o m i n a t e s i t s d e s c e n d a n t s}) $$

• also this is a theorem I don't feel like proving now

$$ P \land (p d o m i n a t e s i t s t a r g e t s) \equiv R, $$

i.e. even introducing a weakening $P$ by starting with its second formulation draws our attention to a p that does not dominate (all) its targets.

Having found a p that does not dominate (all) its targets, we can select one its targets q it does not dominate and have p and q exchange the values they own. After the exchange, q may fail to dominate its descendants, as q.v has been decreased. If so, we would like q to be the only node not dominating its descendants. Node p certainly continues to fail to dominate its descendants if we choose for q a target of p that does not dominate p's other target.

Hence we are hoping that $p$ is an invariant for the following repetition - $p$ ,occurring in the invariant is now global to the block, and no longer viewed as unknown of the equation

do $\left\lbrack q : \left( q\right) \text{is a target of}p\right) \land \right.$

(g dominates the targets of $p$ )

1 (p dominates q)

$$ \rightarrow v. p, v. q := v. q, v. p; p := q $$

1

ad

and now we have to convince ourselves that the value exchange establishes $P_{q}^{p}$ , i.e.

(Ax: x = 9 v (x dominates its dependants))

and this under the initial validity of $P$ and the guard.

Proof Our outer case analysis distinguishes three cases.

(0) $x \neq p \land x \neq q$ .

From $P \land x \neq p$ we conclude that initially (x dominates its descendants); hence it suffices to show that the value exchange between $p$ and $q$ does not falsify (x dominates its descendants. We distinguish:

(0.0) ( $p$ is a descendant of $x$ ) $\equiv \left( q\right)$ is a descendant ${P}_{x}$ ).

In this case, the value exchange between $p$ and $q$ does not modify the bag of values owned by the descendants of $x$ , and hence does not change the value of $(x$ dominates its descendants).

(0.1) $\left( {p\text{ is a descendant of }x}\right) \neq \left( {q\text{ is a descendant of }x}\right)$ .

From ( $q$ is target of $p$ ),we have in this case

From $n$ ( $p$ dominates $q$ ),we conclude that only $p$ ’s owned value increases in the value exchange between $p$ and $q$ .

Combining these two, we conclude that the value exchange does not falsify ( $x$ dominates its descendants).

$\left( 1\right) \;x = p\;y = 0$

We observe

(y is a descendant of $p$ ) $\equiv$

(y is a target of $p$ )

(y is a descendant of a target of $p$ ).

We therefore distinguish the two - not necessarily

exclusive - cases (1.0) and (1.1)

(1.0) (y is a target of $p$ )

We distinguish

(1.0.0) $y = q$ ; since initially $r\left( {p\text{dominates}q}\right)$ , hence(q dominates p), eventually (p domi- nates q), i.e. (p dominates y).

(1.0.1) $y \neq q\;j$ since initially ( $q$ dominates the targets of $p$ ),hence ( $q$ dominates $y$ ), eventually(p dominates y)

(1.1) (y is a descendant of a target $r$ of $p$ ).

Since (r is a target of p) implies (r#p), we conclude - from P' r#p- initially (r dominates its descendants), i.e. (r dominates y).

From (q dominates the targets of p) we conclude initially (q dominates r) Combining the two, we conclude initially (q dominates y). hence eventually (p domi y) -independent of $r = q$ or $y = q!$

Combining (1.0) -i.e. (1.0.0) and (1.0.1) - and (1.1), (p dominates its descendants), i.e. (x dominates its descendants).

(2) $x = 9.$

In this case, $x = 9$

Combining (0) - i.e. (0.0) and (0.1) - (1) and (2) we conclude

$\left( {\underline{A}x\because x = q \vee \left( {x\text{ dominates its descendants}}\right) }\right)$

(End of Proof.)

This was of course not the kind of proof I like.

Depending on the shape of the graph, relation $R$ can be viewed as a stepping stone to complete ordering: the maximum value owned can be found among the nodes without source, the minimum among the nodes without target.

Our program is of interest because the number of iterations is never greater than the longest path.

Austin, 1 November 1984

pruf. dr. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin, Austin,TX,78712-1188 USA