Heuristics for a calculational proof

Theuristics for a calculational proof

Edsger W. Dijkstra

Abstract Using a small, yet sufficiently sophisticated example, we show the heuristics that lead to a compact and clear solution. An implicit message is that the calculational style has the advantage that the formalism used provides major heuristic guidance for the design of the proof.

Key words heuristics, calculational proofs, formal proofs, proof design, proof derivation, avoiding rabbits, formula manipulation.

$\dagger$ Department of Computer Sciences, The University of Texas at Austin, Austin TX 78712 - 1188, USA

The purpose of this note is to show a motivated design of a calculational proof and to give the reader an appreciation for the kind of heuristic guidance that (the properties of) the formalism used can provide. Our example stems from the Nineteenth International Mathematical Olympiad, 1977 (see [0]) and has the advantage that many people have solved it differently. The solution derived here is essentially the one by van de Snepscheut and Bird [1]; it has independently

been designed by Misra [2].

With the natural numbers IN defined as all integers n such that 0n , and using an infix dot to denote function application, we can state the problem as follows:

"A total function that maps natural numbers to natural numbers has the property that

$$ f _ {1} (f _ {2} n) < f _ {1} (n + 1) \tag {0} $$

for all natural n . Show that $f$ is the identity function."

It is only natural, though superfluous, to check that the identity function of type $\mathrm{{IN}} \rightarrow \mathrm{{IN}}$ satisfies (0); it does since $n < n + 1$ .

It is more instructive to try to check that all givens are needed. Certainly we need some- thing like (0), for not any function of type IN→IN is the identity function, and (0) cannot be weakened much either because

$$ f _ {1} (f _ {n}) \leq f _ {1} (n + 1) $$

would admit for any constant function. Also the constraint that maps naturals to naturals is not void: had it been integers to integers", $f \cdot n = n - 1$ would have been admissible.

In other words, our proof has to contain a step that is valid for the natural domain, but not the integer one. Since the naturals are well-founded whereas the integers are not, it is sweetly reasonable to propose

$(\alpha)$ In our proof of

$$ f \cdot n = n \tag {1} $$

for all natural n , we shall try to use mathe-matical induction over the natural numbers.

In following (x), it would be rash to conclude that (1) has to be our induction hypothesis: in view of our obligation to conclude equalities (1) where only inequalities (0) are given, if is sweetly reasonable to (β) We shall try to construct a ping-pong argument in which

$$ n \leq f. n \quad a n d \quad (2) $$

$$ f. n \leq n \tag {3} $$

both for all natural n , are dealt with separately.

In choosing which of the above two to prove by mathematical induction, the choice immediately falls on (2) since the base

$$ 0 \leq f. 0 $$

is an immediate consequence of ${f}_{s}^{\prime }$ type $\mathrm{N} \rightarrow \mathrm{{IN}}$ .

$$ n + 1 \leq f (n + 1) $$

$$ \begin{array}{l} = {\mathrm {a r i t h m e t i c}, \mathrm {h e a d i n g f o r} (0) } \ n < f (n + 1) \ \end{array} $$

$$ \begin{array}{l} \Leftrightarrow \quad {(0) } \ n \leq f (f n) \ \end{array} $$

and here we are stuck, because $n \leq f.n$ is too weak an induction hypothesis to conclude the last result from. So we had better backtrack and look for a stronger induction hypothesis.

Can we conclude a stronger base from the fact that $f$ is of type $IN \rightarrow IN$ ? Well, we can take that fact itself, in order to make it amenable to manipulation, we eliminate the symbol IN by considering the naturals as a subset of the integers and formulate the fact that $f$ is of type $IN \rightarrow IN$ as

$$ \langle \forall n: 0 \leq n \Rightarrow 0 \leq f. n \rangle \tag {4} $$

Asked for which induction hypothesis (4) acts as a proper base, any computing scientist that has designed invariants by replacing constants by variables will come up with the induction hypothesis

$$ \langle \forall n: j \leqslant n \Rightarrow j \leqslant f. n \rangle \tag {5} $$

Concerning the decision to replace both 0's by the induction variable j , we point out that

induction hypothesis $\left\langle {\forall n : j \leq n \Rightarrow 0 \leq f.n}\right\rangle$ would lead to a trivial step and thus prevent the required exploitation of (0). induction hypothesis $\left\langle {\forall n : 0 \leq n \Rightarrow j \leq {f}_{\cdot }n}\right\rangle$ would lead to a step that cannot be proved (5) does the job since

$$ \langle \forall n: n \leq f _ {n} \rangle \Leftarrow \langle \forall j, n: j \leq n \Rightarrow j \leq f _ {n} \rangle \quad . (6) $$

There is a totally different reason why it is more attractive to prove (5) inductively for all $j$ than it is to prove (2) inductively for all $n$ . The reason is that (2) contains the induction variable as argument of (the unknown) function $f$ , whereas (5) contains the induction variable $j$ in perfectly manageable positions.

The base having been taken care of by (4), we now turn to the induction step to prove (5) by mathematical induction over j. To this end we observe for any natural n and j

$$ \begin{array}{l} = \begin{array}{r l} & j + 1 \leq f. n \ & \mathrm {f o r} (0) } \end{array} \ j < f. n \ \Leftrightarrow \quad {0 } \mathrm {w i t h} n := n - 1, \mathrm {i . e .} \ f: (f: (n - 1)) < f. n \quad f o r 1 \leq n } \ j \leqslant f. (f. (n - 1)) \land j \leqslant n \ \Leftrightarrow {e x h y p o t h e s e (5) w i t h n := f. (n - 1) } \ j \leqslant f. (n - 1) \land 1 \leq n \ \Leftrightarrow {e x h y p o t h e s e (5) w i t h n := n - 1 } \ j \leqslant n - 1 \quad \wedge \quad 1 \leqslant n \ = {0 \leq j } \ j + 1 \leq n \ \end{array} $$

In view of (6) we have thus dealt with ping, i.e. (2).

for pong - i.e. $f$ ns n - we observe that mathematical induction over $n$ is (as yet) not indicated because the base is not obvious. To relate (3) to (0)

$$ f _ {1} (f _ {2} n) < f _ {1} (n + 1), $$

we rewrite (3) as

$$ f _ {n} < n + 1, $$

i.e. the given (0) has at both sides of $<$ an f-application more than the demonstran-dum (3). Now this looks very similar to monotonicity! In fact it is.

A usual way of expressing that $f$ is monotonic is that for any $x,y$

$$ x \geq y \Rightarrow f \cdot x \geq f \cdot y $$

by taking the contrapositive, we get for

$$ x < y \Leftrightarrow f _ {x} < f _ {y} \tag {7} $$

Under the assumption of ${f}^{\prime }$ monotonicity, the demonstration of (3) is a walkover: we observe for any natural $n$

$$ \begin{array}{l} f? n \leq n \ = {\mathrm {a r i t h m e t i c}, \mathrm {h e a d i n g f o r} (7) } \ f. n < n + 1 \ \Leftarrow \left{ \begin{array}{l} {(7) w i t h x, y := p _ {n}, n + 1} \ {f. (p _ {n}) < f. (n + 1)} \end{array} \right} \ = \begin{array}{l} {\left{ \begin{array}{l} {(0)} \end{array} \right}} \ {\mathrm {t r u e}} \end{array} \ \end{array} $$

but this still leaves us with the obligation to demonstrate that $f$ is monotonic. (Note that the assumption was safe in the sense that the identity function is, indeed, monotonic.)

Monotonicity of a function $f$ on naturals can be expressed by an expression like (7) with 2 universally quantified dummies, or

$$ \langle \forall x: f. x \leq f (x + 1) \rangle \tag {8} $$

which quantifies over 1 dummy. The latter is usually the most convenient form to demon-strate monotonicity; the former, which includes the consequences of transitivity, is the most convenient characterization for the exploitation of monotonicity.

Remark The above paragraph covers a standard ingredient of the intellectual baggage of professional reasoners about sorting. (End of Remark.)

In order to demonstrate the monotonicity of $f$ ,we prove (8) by observing for any natural

$\left{ \begin{array}{l} p \cdot x \ \left( 2\right) \end{array}\right.$ with $n = p \cdot x}$ $f.\left( {p,x}\right)$ $\leq \left{ \begin{array}{l} {f}_{\left( 0\right) }\left( 0\right) \end{array}\right.$ with $n \mathrel{\text{:=}} x}$

which concludes pong , and thus the whole

*

A few final remarks. Firstly, had we written

$$ \langle \forall n: n \in I N \Rightarrow f. n \in I N \rangle $$

instead of (4), a simple mechanical routine would no longer have sufficed for the generaliza tion to (5). This illustrates the advantage of avoiding special terminology, notations, or symbols (such as IN), i.e. of bandwidth reduction in general.

Secondly we would like to point out that the occurrence of a reductio ad absurdum often indicates that the author has failed to formulate a contrapositive, such as (7).

Acknowledgements I thank van de Snepscheut, Bird, and Misra for their inspiration, and the Tuesday Afternoon Clubs of Austin and of Eindhoven for their comments.

[0] Greitzer, Samuel L., "International Mathematical Olympiads, 1959-1977", Mathematical Association of America, 1978

[1] Sneepscheut, Jan L.A. van de, JAN 161 "A little problem posed by R.S. Bird" d.d. 1989.12.11, California Institute of Technology

[2] Misra, Jayadev, Private Communication Nuenen 11 July 1994