On the transitive closure of a wellfounded relation

On the transitive closure of a wellfounded relation

$$ E d s g e r \begin{array}{l} \underline {{b y}} \ \overline {{W}}. D i j k s t r a \end{array} $$

$$ \mathrm {D e d i c a t e d} \quad \mathrm {t o} $$

$$ \begin{array}{l} \mathrm {N i k l a u s W i r t h} \end{array} $$

0 Notation, terminology, and imported mathematics

We use the term "predicates" for the elements of a boolean algebra, their standard model being boolean functions defined on some space. Besides the usual boolean operators $(\neg ,\land ,\lor ,\Rightarrow ,\Leftarrow ,\equiv)$ we use for predicates the "everywhere operator" [...] of type predicates $\rightarrow$ {true,false} : [p] is only true if p is, for all other p, [p] = false. In the standard model, [...] corresponds to universal quantification over the underlying space.

In what follows, $f$ is a so-called "predicate transformer", i.e. a function $f$ : predicates $\rightarrow$ predicates. When we then wish to consider the boolean expression $[f.x]$ as an equation to be solved for the unknown $x$ , we denote that equation by $x: [f.x]$ . If

$$ x: ([ f. x ] \wedge \langle \forall y: [ f. y ]: [ x \Rightarrow y ] \rangle) $$

has a solution, it is unique and is called "the strongest solution of $x : {\left\lbrack f.x\right\rbrack }^{\prime \prime }$ ; similarly,if

$$ x: ([ f. x ] \wedge \langle \forall y: [ f. y ]: [ x \Leftarrow y ] \rangle) $$

has a solution, it is unique and is called "the weakest solution of $x : \left\lbrack {p,q}\right\rbrack$ ".

A predicate transformer $f$ being "monotonic" means that for all predicates

$$ [ x \Rightarrow y ] \Rightarrow [ f. x \Rightarrow f. y ] $$

The famous Theorem of Knaster-Tarski tells us that for monotonic $f$ ,the equations $x : \left\lbrack {p.x \Rightarrow x}\right\rbrack$ and $x : \left\lbrack {p.x \equiv x}\right\rbrack$ have the same strongest solution

$$ \langle \forall y: [ f _ {y} \Rightarrow y ]: y \rangle $$

while the equations $x : \left\lbrack {x \Rightarrow {f}{1}x}\right\rbrack$ and $x : \left\lbrack {x \equiv {f}{2}x}\right\rbrack$ have the same weakest solution

$$ \langle \exists y: [ y \Rightarrow p, y ]: y \rangle $$

The "relation calculus" is obtained from the predicate calculus by adding to it two operators ("composition" and "converse") and one constant (the identity element of composition). In this note we only need the composition, which will be denoted by an in. fix ";" with a syntactic binding power be-

tween ? and the logical infix operators. We shall use that composition is associative and that in either argument it distributes over v ; the latter property implies that composition is monotonic in either argu-. ment. In the standard model of the relation calculus, the predicates are boolean functions of two variables of the same type -the underlying space has the structure of a "Cartesian square"-- and the composition of the relations p and q is modelled by

$$ \alpha (p; q) \beta = \langle \exists \gamma : \alpha p \gamma \land \gamma q \beta \rangle $$

(As is usually done, we have treated the rela-

Relation $I$ being (left-)wellfounded means no more and no less than that for any $P$

$$ \langle \forall \alpha : \langle \forall \gamma : \alpha ] \gamma : P _ {\gamma} \rangle \Rightarrow P _ {\alpha} \rangle \Rightarrow \langle \forall \alpha : P _ {\alpha} \rangle , $$

i.e. that proof by mathematical induction is valid: instead of showing $P \propto$ for arbitrary $\alpha$ , it suffices to show that it follows from the assumption that $P$ holds for all "smaller" values $\gamma$ . Taking a contrapositive, denoting $\neg P$ by $x$ (a relation that need not depend on its second argument), and $\exists$ by $r$ , we can express the (left-) well-

foundedness of $r$ by the fact that for all $x$

(0) $\left\lbrack {x \Rightarrow {r}_{;}x}\right\rbrack \Rightarrow \left\lbrack {\neg x}\right\rbrack$

In other words, (left-) wellfoundedness of $r$

means that $\frac{\text{false}}{\text{solution}}$ is the only, and hence the weakest

But then, thanks to Knaster-Tarski, false is also the weakest, and hence the only

solution of $x : \left\lbrack {x \equiv r;x}\right\rbrack$ ,so that we can also characterize the (left-) wellfoundedness of $r$ by the fact that for all $x$

(1) $\left\lbrack {x \equiv r;x} \right\rbrack \Rightarrow \left\lbrack {-r}\right\rbrack$

The two alternative formulations for $r$ being (left-) wellfounded explain our interest in the boolean expressions $\left\lbrack {x \Rightarrow r;x}\right\rbrack$ and $\left\lbrack {x \equiv r;x}\right\rbrack$

Remark Other characterizations of wellfoundedness are in terms of minimal elements of subsets or lengths of decreasing chains. In view of their explicit reference to the elements of the domain, the existence of the point-free characterizations (0) and (1) comes as a surprising simplification. (End of Remark.)

1. The nonreflexive transitive closure

The nonreflexive transitive closure is of

a relation $r$ can be defined as the strongest satisfying

(2) $\left[r \vee r; s \equiv s\right]$

(Because of Knaster-Tarski, there are alter-native definitions, but we chose (2) because, all by itself, it has interesting consequences.)

Lemma 0 For any pair $r,s$ of relations satisfying (2) we have

$$ \langle \forall x: [ x \Rightarrow r; x ] \Rightarrow [ x \Rightarrow s; x ] \rangle $$

Proof We observe for any $r,s$ satisfying

$$ [ x \Rightarrow s; x ] $$

$$ \equiv \quad {(2) } $$

$$ [ x \Rightarrow (r \vee r; s); x ] $$

$\Leftrightarrow$ {pred. calc. and monotonicity of $\therefore }$

$$ [ x \Rightarrow r; x ] $$

(End of Proof.)

Combining Lemma 0 with the characterization (O) of left-wellfoundedness, we conclude

Corollary 0 If the nonreflexive transitive closure of a relation is left-wellfounded,

so is the relation itself.

Lemma 1 For any pair $r,s$ of relations satisfying (2) we have

$$ \langle \forall x: [ x \equiv s; x ] \Rightarrow [ x \equiv r; x ] \rangle $$

Proof We observe for any $r,s$ satisfying (2) and any $x$ satisfying

(3) $\left\lbrack {x \equiv s;x}\right\rbrack$

$$ \begin{array}{l} \equiv \begin{array}{l} x \ {(3) } \ s; x \end{array} \ \equiv \begin{array}{l} {(2) } \ (r \vee r; s); x \end{array} \ \equiv \left{; d i s t r i b u t e s o v e r v a n d i s a s s o c i a t i v e \right} \ \equiv \begin{array}{l} {(3) } \ r; x \vee r; x \end{array} \ \equiv \begin{array}{l} {{\mathrm {p r e d . c a l c .} }} \ {r; x} \end{array} \ \end{array} $$

(End of Proof.)

Combining Lemma 1 with the character-ization (1) of left-wellfoundedness, we conclude

Corollary If a relation is left-wellfounded,

so is its nonreflexive transitive closure.

Remark It is worth noting that neither of our Lemmata requires r to be wellfounded or s to be the strongest s satisfying (2). (End of Remark.)

2 Uniqueness

Finally, we show that for left-wellfounded

(4) $[r \vee r; s \equiv s]$ (5) $\left\lbrack {r \vee r;t = t}\right\rbrack$ (6) $\left\langle {\forall x : \lbrack x \Rightarrow r;x\rbrack \Rightarrow \lbrack 7x\rbrack }\right\rangle$ ,

then $\left\lbrack {s \equiv t}\right\rbrack$ holds.

Proof For reasons of symmetry, it suffices to show $\left\lbrack {t \Rightarrow s}\right\rbrack$ . We observe

$$ \begin{array}{l} [ t \Rightarrow s ] \ \equiv \begin{array}{l} {\text {p r e d . c a l c .} } \ [ 7 (t \wedge 1 s) ] \end{array} \ \Leftrightarrow \quad {(6) \text {w i t h} x := t \wedge 1 5 } \ [ t \wedge \neg s \Rightarrow r; (t \wedge \neg s) ] \ \equiv \begin{array}{l} \left{\text {s h u n t i n g} \right} \ [ t \Rightarrow s \lor r ]; \end{array} \ \equiv \begin{array}{l} {(4) } \ [ t \Rightarrow r \lor r; s \lor r; (t \land 1 s) ] \end{array} \ \end{array} $$

$$ \begin{array}{l} \equiv \begin{array}{l} {\left{\vdots ; \mathrm {d i s t r i b u t e s o v e r} V \mathrm {a n d p r e d . c a l c} \right}} \ {[ t \Rightarrow r \vee r; (t \vee s)} \end{array} \ \Leftarrow {m o n o t o n i c i t y o f ; } \ [ t \Rightarrow r \vee r; t ] \ = {(5) } \ t r u e \ \end{array} $$

(End of Proof.)

I gratefully acknowledge the contribution of Rutger M. Dijkstra (viz. the isolation of Lemma 1) and that of Wim Feijen and Netty van Gasteren (viz. the final proof of unicity).

Austin, 10 January 2000