Mathematical induction synthesized

Mathematical Induction Synthesized

Let $f$ be a monotonic predicate transformer and let $g$ be the strongest solution of $p: [f.p \Rightarrow p]$ . Then, by definition,

(0) $\left\lbrack {f,q \Rightarrow q}\right\rbrack$ (1) $\left\lbrack {f.p \Rightarrow p}\right\rbrack \Rightarrow \left\lbrack {q \Rightarrow p}\right\rbrack \;$ for all $p$ .

The first theorem of this note is that for mono-tonic $f$ ,(1) can be strengthened to

(2) $\left\lbrack {q \Rightarrow \left( {f.p \Rightarrow p}\right) }\right\rbrack \Rightarrow \left\lbrack {q \Rightarrow p}\right\rbrack \;\operatorname{for all}p.$

Proof We observe for any $p$

$$ \begin{array}{l} [ q \Rightarrow (p, p \Rightarrow p) ] \ = {\text {p r e d . c a l c .} } \ [ q ^ {\prime} \wedge p \Rightarrow p ] \ = {\mathrm {p r e d . c a l c .} } \ \end{array} $$

$$ [ q \wedge f _ {p} \Rightarrow q \wedge p ] $$

$\Rightarrow \;\left{ {\left( 0\right) ,\left( {anti}\right) {monotonicity} \circ P, \Rightarrow }\right}$

$$ [ f, q \land f, p \Rightarrow q \land p ] $$

$\Rightarrow \left{ {f\text{ is monotonic，i.e. }f\left( {q \land p}\right) \Rightarrow f,q \land p}\right}$

$$ [ f. (q \wedge p) \Rightarrow q \wedge p ] $$

$\Rightarrow \;\left{ \begin{array}{l} \left( 1\right) \text{ with }p : = {9p} \ \end{array}\right}$

$$ [ q \Rightarrow q \land p ] $$

$= {$ pred.calc. $}$

$$ [ q \Rightarrow p ] \qquad \mathrm {(E n d o f P r o o f .)} $$

Formula (2) can be rewritten (by predicate calculus) as

$\left\lbrack {f.p \Rightarrow \left( {q \Rightarrow p}\right) }\right\rbrack \Rightarrow \left\lbrack {q \Rightarrow p}\right\rbrack$ from which, by using the monotonicity of $f$ once more, we can derive $\left\lbrack {f.}\left( {q \Rightarrow p}\right) \Rightarrow \left( {q \Rightarrow p}\right) \right\rbrack \Rightarrow \left\lbrack {q \Rightarrow p}\right\rbrack$

We now consider for $p$ the choice $\pi(s; \pi)$ , that is, let $q$ now be the strongest solution of $p: [p \vee s; \pi]$ . Then, by definition,

(5) $\left\lbrack {q \vee s;7q}\right\rbrack$ (6) $\left\lbrack {p \vee s;{np}}\right\rbrack \Rightarrow \left\lbrack {q \Rightarrow p}\right\rbrack$

Our second theorem is that with this choice of $f$ , $g$ is a left-condition, i.e. $[g; \text{true} \Rightarrow g]$ .

Proof We observe

$$ \begin{array}{l} [ q; \mathrm {t r u e} \Rightarrow q ] \ = {\mathrm {l e f t - e x c h a n g e} } \ [ 7 9; \sim t r u e \Rightarrow 7 9 ] \ = {\mathrm {c o n t r a p o s i t i v e}, [ \mathrm {t r u e} \equiv \sim \mathrm {t r u e} ] } \ [ q \Rightarrow \neg (\neg q; t r u e) ] \ \Leftrightarrow \quad {(6) \mathrm {w i t h} p := 7 (7 q; \mathrm {t r u e}) } \ [ 7 (7 q; t r u e) \lor S; 7 q; t r u e ] \ = {\text {p r e d . c a l c .} } \ \end{array} $$

$$ \begin{array}{l} [ \neg q; t r u e \Rightarrow s; \neg q; t r u e ] \ \Leftrightarrow {\mathrm {m o n o t o n i c i t y} o p; } \ [ 7 9 \Rightarrow s; 7 9 ] \ = {5 } \ t r u e \ \end{array} $$

(End of $P$ rrow $?$ )

Let us apply (4) with the last choice

$$ [ q \Rightarrow (7 (s; (q \wedge 7 p)) \Rightarrow p) ] \Rightarrow [ q \Rightarrow p ] $$

Taking for $q$ also a left-condition,we now translate into the standard model with

$$ \begin{array}{l} 9 \quad \mathrm {y i e l d i n g} \quad Q. x \ p \quad y i e l d i n g \quad P. x \ s \quad y i e l d i n g \quad x > y \ [ \dots ] y i e l d m g \quad \langle \forall x, y: \dots . \rangle \ \end{array} $$

Since everything reduces to left-conditions, the universal quantification over $y$ can be dropped. The translation of $s; (q \land 7p)$ is,

$$ \langle \exists z: x > z \land Q. z \land \neg P. z \rangle $$

The whole translation yields

$$ \langle \forall x: Q. x: \langle \forall z: x > z \wedge Q. z: P. z \rangle \Rightarrow P. x \rangle \Rightarrow \langle \forall x: Q. x: P. x \rangle $$

i.e. $q$ emerges as the characterization of the "domain" over which $s$ is well-founded.

Traditionally, well-foundedness is defined for a (domain, relation)-pair. The moral of the story is that we can start with the relation, and any relation then yields the domain over which it is well-founded. Instead of starting with (the natural numbers, $x > y$ ) we can start with the relation $x > y \land y \geq 0$ on the type integer. The corresponding "domain" then follows. It also shows that any relation can be used to do mathematical induction with; if, however, that domain is empty, the induction principle is not very useful.

Once more I shall show that a relation $s$ and its transitive closure $r$ are equally well-founded; this now means that, with

$$ (7) \quad [ r \equiv s v s; r ] $$

the equations

$$ p: [ p \vee s; 7 p ] \quad a n d \quad p: [ p \vee r; 7 p ] $$

have the same strongest solution. To save negation signs, we shall show instead that the equations

$$ p: [ p \Rightarrow s; p ] \quad a n d \quad p: [ p \Rightarrow r; p ] $$

have the same weakest solution. That is, with $q$ determined by

(8) $[q\Rightarrow s;q]$ and (9) $\left\lbrack {p \Rightarrow s;p}\right\rbrack \Rightarrow \left\lbrack {p \Rightarrow q}\right\rbrack$

we have to show

(10) $\left\lbrack {q \Rightarrow r;q}\right\rbrack$ and (11) $\left\lbrack {p \Rightarrow r;p}\right\rbrack \Rightarrow \left\lbrack {p \Rightarrow q}\right\rbrack$

Proof To demonstrate (10) we observe

$$ [ q \Rightarrow r; q ] $$

$\Leftrightarrow \left{ \begin{array}{l} \text{monotonically } \ \text{and } \Rightarrow \ \left\lbrack {q \Rightarrow s;q}\right\rbrack \land \left\lbrack {s \Rightarrow r}\right\rbrack \end{array}\right.$ $= \left{ {\left( 8\right) \text{ and }\left( 7\right) }\right}$

To demonstrate (11) we observe

$$ [ p \Rightarrow r; p ] $$

$= {$ pred. calc. $}$

$$ [ p \vee r; p \Rightarrow r; p ] $$

$\left{ \left( 7\right) \right}$

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

$= \;\left{ {;\text{ over }v}\right}$

$$ [ p \vee r; p \Rightarrow s; p \vee s; r; p ] $$

$= \;\left{ {;\text{ over }v}\right}$

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

$\Rightarrow \;\left{ \begin{array}{l} \left( 9\right) \text{ with }p : p \vee r;p} \ \end{array}\right.$

$$ [ p \vee r; p \Rightarrow , q ] $$

$\Rightarrow$ {pred. calc.}

$\left\lbrack {p \Rightarrow q}\right\rbrack$ (End of Proof.)

The last theorem was independently proved by J.R.Rao, who subsequently assisted me in the phrasing of the above proof. The above proof is independent of the question of whether (7) determines $r$ uniquely; I like it because it uses of the relational calculus only that composition is associative and distributes over disjunction.

I found these results essentially last week on my trip to Poughkeepsie and to Ithaca. When I came home I found among the mail a copy of a manuscript by Rutger M. Dgkstra. It is a manuscript of 74 pages with what looks like a beautiful theory. On the last page but two it casually mentions as a corollary " s' s is left-founded for all s" (Legenda: s" denotes the weakest solution of p: [p ⇒ s; p].) It very much looks as if I can now leave the relational calculus in the more expert hands of the younger generation.

Austin, 17 April 1992

prop. dr. Edsger W. Dyksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78750 - 1188, USA