A calculational example

A calculational example

In this note $x$ and $y$ are variables of some type E and P, Q and R are predicates on E , i.e. functions of type E→IB (where B denotes the boolean domain {true, false}).

We introduce square brackets [...] to denote what is known as "the everywhere operator", which is a function of type $\left( {E \rightarrow B}\right) \rightarrow B$ . For any predicate $P$ ,it is defined by

$$ [ P ] \equiv \langle \forall x: P _ {x} \rangle $$

the right-hand side to be read as "for all $x$ (of type E), $P \times \left( { = {\text{true}}\text{)}}\right)$ . The right-hand side has the problem that writing it down forces us to make an irrelevant choice, as we also could have written $\langle \forall y : P \cdot y\rangle$ instead. The left-hand side [P] - read as "everywhere $P$ " is freed from that clutter.

In order to render a universal quantification by the every where operatior as given by (0), it is essential that the term be of the form $P \cdot x$ ,i.e. a func

tion - here $P$ - applied to arbitrarily chosen dummy. As it stands, universal quantifications like $\left\langle {\forall x : 1}\right\rbrack \cdot P.x}$ or $\left\langle {\forall x : P.x \Rightarrow Q.x}\right\rangle$ cannot be rendered by the every where operator because the terms ${P}_{x}$ and $P{x}^{2} \Rightarrow Q{x}^{2}$ respectively do not have the required shape.

There are two ways out of this dilemmas, viz. the introduction of $f_{1}$ new names and of "function expressions". The introductiOn of new names is mathematically very simple: if $R$ is defined by

$$ \langle \forall x: \mathcal {R}. x \equiv \neg \mathcal {P}. x \rangle \quad , \qquad \mathrm {t h e n} $$

$$ [ R ] \equiv \langle \forall x: \neg P _ {x} \rangle $$

Similarly, if $R$ is defined by

$$ \langle \forall x: \mathcal {R}. x \equiv (\mathcal {P}. x \Rightarrow Q. x) \rangle \qquad t h e n $$

$$ [ R ] \equiv \langle \forall x: P _ {x} \Rightarrow Q _ {x} \rangle $$

It is very simple, but does not help much either: there is little we can do with [R] without referring back to R's definition.

The way of introducing "function

convention that application to an argument distributes to the left over the operators on the type of the function value. That is, we introduce for example the new expressions $\neg P$ and $P \Rightarrow Q$ given by

$$ \langle \forall x: (\neg P). x \equiv \neg (P. x) \rangle \quad a n d $$

$$ \langle \forall x: (P \Rightarrow Q). x \equiv (P. x \Rightarrow Q. x) \rangle $$

Notice that this convention implies "overloading" of the operators: at the right-hand side of $\equiv$ , the boolean operators -here 7 and $\Rightarrow$ have arguments and yield values of type B, while at the left-hand side they have arguments and yield values of type E→B.

It is the convention of lifting that allows us to apply the everywhere operator to a whole class of function expressions, e.g.

$$ [ \neg P ] \equiv \langle \forall x: \neg P. x \rangle a n d $$

$$ [ P \Rightarrow Q ] \equiv \langle \forall x: P. x \Rightarrow Q. x \rangle . $$

Finally, notice that $\left\lbrack {P \equiv Q}\right\rbrack$ expresses that $P$ and $Q$ are different names for the same predicate.

In the following, the only logical connectives we shall use are -listed in the order of increasing syntactic binding power - $\equiv , \Rightarrow , \land$ . From predicate calculus we shall use that for all P.O.R we have

(0) $[P \land Q \Rightarrow R] \equiv [Q \Rightarrow (P \Rightarrow R)]$ (1) $\left\lbrack {P \Rightarrow Q}\right\rbrack \equiv \left\lbrack {{P}^{ \land }Q \equiv P}\right\rbrack$

without reference we shall use that

associative: $\left\lbrack {{P}{A}\left( {Q \land P}\right) \equiv \left( {{P}{A} \land Q}\right) \land R}\right\rbrack$ Symmetric: $\left\lbrack {{P}{A} \land Q \equiv Q \land P}\right\rbrack$ idempotent: $\left\lbrack {{P}{A} \land P \equiv P}\right\rbrack$

All the above we are going to use in our study of the "priming operator" given by the assertion that for all $P_{1}$ predicate $P^{\prime}$ is given by

(2) $\left\lbrack {P}^{\prime }\right\rbrack = f \cdot P \Rightarrow P\rbrack$

for some function from predicates to predicates, i.e. of type $\left( {E \rightarrow B}\right) \rightarrow \left( {E \rightarrow B}\right)$ .

Our first lemma puts no further re- requirements on function $f$ .

Lemma 0 : $\left\lbrack {P \Rightarrow {P}^{\prime }}\right\rbrack$

Proof We observe for any $P$

$$ \begin{array}{l} [ P \Rightarrow P ^ {\prime} ] \ \equiv {(\mathbf {2}), \mathrm {t h e d e f i n i t i o n o f p r i m i n g} } \ [ P \Rightarrow (f: P \Rightarrow P) ] \ \equiv {0 } \mathrm {w i t h} P, Q, R := f P, P, R } \ [ f. P \land P \Rightarrow P ] \ \equiv {(\mathbf {1}) \mathrm {w i t h} P, Q := f _ {\cdot} P \wedge P, P } \ [ f. P \land P \land P \equiv f. P \land P ] \ \equiv {\mathrm {p r o p e r h i e s} \varphi^ {\prime} \wedge } \ f r u e \ \end{array} $$

$$ (\mathrm {E n d o f P r o o f .}) $$

Our next investigation explores what we may have to postulate about $f,$ so that we can show that the priming operation is idempotent, i.e. that $P!$ is a fixpoint of the priming operation, that is, in formula, that

(3) $\left\lbrack {{P}^{\prime } \equiv {P}^{\prime \prime }}\right\rbrack$

So we start a proof of the above. We observe for any $p$

$$ \begin{array}{l} \begin{array}{r l} {[ P ^ {\prime} \equiv P ^ {\prime \prime} ]} & \ & {\quad {(2) \mathrm {w i t h} P := P ^ {\prime} }} \ {[ P ^ {\prime} \equiv f: P ^ {\prime} \Rightarrow P ^ {\prime} ]} & \end{array} \ \equiv \begin{array}{l} {\left{ \begin{array}{l} {(2)} \end{array} \right}} \ {[ P ^ {\prime} \equiv f. P ^ {\prime} \Rightarrow (f. P \Rightarrow P) ]} \end{array} \ \equiv {(\mathbf {0}) \mathrm {w i t h} P, Q, R := f. P, f. P ^ {\prime}, P } \ \end{array} $$

$$ \begin{array}{l} [ P ^ {\prime} \equiv f. P \wedge f. P ^ {\prime} \Rightarrow P ] \ \equiv \quad {(4), \mathrm {s e e b e l o w} } \ [ P ^ {\prime} \equiv f. P \Rightarrow P ] \ = {2 } \ t r u e \ \end{array} $$

and this completes the demonstration of (3), conditional on the demonstration of (4).

Remark The above proof appeals 3 times to (2), the definition of the priming operation. This is no accident: (3) contains 3 primes. (End of Remark.)

The lemma (4) we need above is

To demonstrate this we observe $\left\lbrack {\begin{array}{l} f.P \land f.P^{\prime } \equiv f.P \end{array}\rbrack }\right\rbrack$ $\equiv \left{ \begin{array}{l} \left( 1\right) \text{ with }P,Q \mathrel{\text{:=}} f.P,{f}^{\prime }P \ \end{array}\right}$ $\left\lbrack {f,P \Rightarrow f,P}^{\prime }\right\rbrack$ $\Leftrightarrow \left{ \begin{array}{l} f\text{ is monotonict,see (5) below}\ \text{with}\;Q \mathrel{\text{:=}} {P}^{\prime }J \end{array}\right}$ $\left\lbrack {P \Rightarrow {P}^{\prime }}\right\rbrack$ $\equiv \left{ {\text{Lemma }0}\right}$ true where " $f$ is monotonic means" that we have for any $P,Q$ that

(5) $\left\lbrack {P \Rightarrow Q}\right\rbrack \Rightarrow \left\lbrack {f.P \Rightarrow f.Q}\right\rbrack$

and thus we have proved

[\text{Lem}n\overset{1}{\operatorname{or}}\text{for monotonetic}]

Monotonic functions are fairly common. One way of establishing monotonicity is by Lemma 2 A function that distributes over

Proof Given that $f$ . distributes over $\Lambda$ we observe for any $P,Q$

$$ \begin{array}{l} [ f, P \Rightarrow f, Q ] \ \equiv {(\mathbf {1}) \mathrm {w i t h} P, Q := f. P, f. Q } \ [ f. P \wedge f. Q = f. P ] \ \equiv {f _ {i} ^ {\prime} d i s t r i b u t e s o v e r \wedge } \ [ f: \mathrm {d i s t r i b u t e s} ] \ \iff \begin{array}{l} {{\mathrm {L e i b n i z : s u b s t h i t u n g e q u a l s f o r e q u a l s} }} \ {[ P \land Q \equiv P ]} \end{array} \ \equiv \begin{array}{l} \left{ \begin{array}{l} (1) \end{array} \right} \ [ P \Rightarrow Q ] \end{array} \ \end{array} $$

with which (5) has been established.

(End of Proof.)

Because universal quantification dis- tributes over $\land$ in a sense to be shown

below, we now consider an $f$ satis-

$$ (7) \quad (f. R). x \equiv \langle \forall y: y < x: R. y \rangle $$

where the right-hand side should be

read as "for all $y$ such that $y < x$ ,

$R,y$ (holds)". Then $f$ . distributes over $\Lambda$ .

$$ \mathrm {P r o o f} \quad \mathrm {W e s h o w} [ f. (P \land Q) \equiv f. P \land f. Q ] $$

by observing for any $P,Q,x$

$$ (f. (P \land Q)). x $$

$$ \equiv \left{ \begin{array}{l l} (7) & \mathrm {w i t h} R := P \land Q \end{array} \right} $$

$$ \langle \forall y: y < x: (P \land Q). y \rangle $$

$$ = {Y _ {i} f i n g } $$

$$ \langle \forall y: y < x: P. y \land Q. y \rangle $$

$$ \equiv \left{d i s t r i b u t i o n o f \forall o v e r \land \right} $$

$$ \langle \forall y: y < x: P. y \rangle \land \langle \forall y: y < x: Q. y \rangle $$

$$ \equiv {(7) \mathrm {w i t h} R := P \mathrm {a n d} \mathrm {w i t h} R := Q } $$

$$ (f. P). x \wedge (f. Q). x $$

$$ \equiv {\mathrm {l i f t i n g} } $$

$$ (f: P \land f: Q). x $$

and as this holds for any $x$ ,we have

prove $\left\lbrack {{f}{1}\left( {{P}^{1}{Q}^{1}}\right) \equiv {f}{1}^{p}{P}^{1}{f}^{q}{Q}^{1}}\right\rbrack$ .

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

The combination $(E, <)$ is called

a well-founded set if the following

form of proof by mathematical induction

is valid: in order to show $P_{x}$ for any $x$ , it suffices to show that $P_{x}$ is true under the assumption that $P$ holds for all smaller values, i.e.

(8) $\left\langle {\forall y : y < x : {P}{y}y}\right\rangle \Rightarrow {P}{x}$ for all $x$ .

with $f$ as defined in (7),proof obligation (8) takes the form

$$ [ f. P \Rightarrow P ] $$

or, with priming defined as in (2),

$$ [ P ^ {\prime} ] \quad . $$

In other words: "(E, < ) is well-founded" means "for all predicates $P$ on $E$ , $[P'] \Rightarrow [P]$ ". That is, if $(E, < )$ is well-founded, we can prove $[P]$ by proving $[P']$ . Instead, which is in general easier since - see Lemma 0 - $[P \Rightarrow P']$ . But it makes no sense to try to prove $[P']$ in turn by mathematical induction since the priming operation in question guarantees that $[P' \equiv P'']$ .

Concluding remarks

This note is not about the (meta)theorem that the decision to prove something by

mathematical induction does not need to be repeated because it is idempotent (though some would consider this an unusual theo- rem and we have proved it simply) but about calculation. We should try to get an appreciation for which elements have made this calculation so effective.

There is to begin with "the everywhere operator": by doing away with the dummy of the universal quantifier $\forall$ it certainly contributes to the brevity of our formulae. A second issue is the decision to denote this operator by a parenthesis pair surrounding its argument. The observation that this argument is usually an expression of some complexity supports this notational decision. Writing $[\mathcal{P} \equiv \mathcal{Q}]$ instead of $\mathcal{P} = \mathcal{Q}$ deviates, however, from the tradition of denoting a binary relation by an infix operator, and some think this deviation too high a price to pay.

There is no controversy about the benefits of introducing the notational possibility of manipulating unapplied functions, nor about borrowing by "lifting" the operators needed to form function-valued expressions.

unapplied functions $- P,P \Rightarrow Q,f,P,$

I would like to point out that, though the introduction of the name $R$ as on EWD 1278-1 did not buy us much, we used the same technique at great advantage in formula (7) for the definition of $p$ .

Remark For the sake of completeness I mention that (7) can be viewed as two hidden $\lambda$ -abstractions: we could have defined

$$ f = \langle \lambda R: \langle \lambda x: \langle \forall y: y < x: R. y \rangle \rangle \rangle $$

but I don't consider that an improvement over (7). In my limited experience, the $\lambda$ - calculus is better avoided when you don't need it. (End of Remark.)

The calculation further derives its crispness from the degree in which it has been disentangled. Our final goal of the calculation was a (meta) theorem about mathematical induction, but none of the specifics of mathematical induction enter the calculation:

$\left\lbrack {P \Rightarrow {P}^{\prime }}\right\rbrack$ is demonstrated without any assumption about

using the above, $\left\lbrack {{P}^{\prime } \equiv {P}^{\prime \prime }}\right\rbrack$ is demonstratd assuming only $f$ to be monotonic, independent of the above it is shown that $f$ is monotonic if it distributes over independent of the above it is shown that universal quantificaton distributes over $\wedge$ finally the link to mathematical induction is made: implication (8) has a universally quantified antecedent.

In short: "Ain't it a beauty?"

Austin, 10 September 1998

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