The heuristics of a proof by Jan L.A. van de Snepscheut and Richard S. Bird

The heuristics of a proof by Jan L.A. van de

From JAN 161 “A little problem posed by R.S. Bird” d.d. 1989.12.11, I quote the statement of the problem:

"We are given a total function $f$ that maps natural numbers to natural numbers. It has the peculiar property

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

for all $n \geq 0$ . The problem is to show that

Note for the sake of accuracy, in (0) Ian did not use the infix dot to denote function application. (End of Note.)

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

It is more instructive to try to check that all givens are needed. Certainly we need (0) , for it is not the case that any function of type $\mathrm{{IN}} \rightarrow \mathrm{{IN}}$ is the iden- tity function. Also, the constraint that $f$

maps naturals to naturals is not void: had it been integers to integers, f given by $\mathbf{f}.\mathbf{n} = \mathbf{n} - 1$ ,for all integer n, would have satisfied (o). In other words, our proof has to contain a step that is valid for a natural domain,but invalid for an integer one.Because the naturals are well-founded whereas the integers are not,it is sweetly reasonable to propose:

$(\alpha)$ In our proof of

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

for all $n \geq 0$ ,we shall try to use mathe-matica induction over the natural numbers.

In following (x), it would be rash to conclude that (1) has to be our induction hypothesis; comparing (0) and (1), we observe similarities -comparisons of expressions with different depths of fapplication-and a major difference: in the demonstrandum (Y), the relational operator is , in the given (O) it is In view of the obligation to conclude equality where inequalities are given, it is sweetly reasonable to pro-

(3) We shall try to construct a ping-pong argument in which

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

$$ f. n \leqslant n \quad , \tag {3} $$

both for all $n \geq 0$ ,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

$$ p _ {0} \ge 0 $$

is an immediate consequence of $f$ ’s type

$$ \begin{array}{l} f. (n + 1) \geq n + 1 \ = {\mathrm {a r i t h m e t i c} } \ f. (n + 1) > n \ \Leftrightarrow \quad {(0) } \ f. (f. n) \geqslant n \ \end{array} $$

and here we are stuck, for this gives us no opportunity to appeal to the induction hypothesis $\mathbb{P}$ n≥n . So we had better backtrack and look for a stronger in- duction 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 be able to use the given that $f$ is of type $IN \rightarrow IN$ , we formulate it without $IN$ :

$$ \langle \forall n: n \geqslant 0 \Rightarrow f. n \geqslant 0 \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: n \geqslant j \Rightarrow f _ {n} \geqslant j \rangle \quad (5) $$

Remark Concerning the decision to replace both 0's by $j$ ,we point out

induction hypothesis $\left\langle {\forall n : n \geq j \Rightarrow {f}_{1}n \geq 0}\right\rangle$ induction hypothesis $\left\langle {\forall n : n \geq 0 \Rightarrow f.n \geq j}\right\rangle$ leads to a step that cannot be proved (5) does the job since

$$ x \geqslant y \equiv \langle \forall j: y \geqslant j \Rightarrow x \geqslant j \rangle \tag {6} $$

(End of Remark.)

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) inductively over $j$ . To this end we observe for any natural

$$ \begin{array}{l} n \mathrm {a n d} j \ = \begin{array}{l} f. n \geqslant j + 1 \ {\mathrm {a r i t h m e t i c} } \end{array} \ \iff \quad f. n > j \left{ \begin{array}{l} (0) \text {w i t h} n := n - 1, \end{array} \right. \text {i . e .} \ f. n > f. (f. (n - 1)) \quad f o r \quad n \geqslant 1 } \ n \geqslant 1 \land f. (f. (n - 1)) \geqslant j \ \Leftrightarrow {e x h y p. (5) w i t h ^ {\circ} n := f ^ {\cdot} (n - 1) } \ n \geqslant 1 \land f ^ {\prime} (n - 1) \geqslant j \ \Leftrightarrow \quad {e x h y p.: (5) \mathrm {w i t h} n := n - 1 } \ n \geqslant 1, n - 1 \geqslant j \ = {j \geqslant 0 } \ n \geq j + 1 \ \end{array} $$

Thus we have dealt with ping, i.e. (2).

For pong 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 _ {3} (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!

The usual way of expressing that $f$ is monotonic is

$$ \langle \forall x, y: x \geq y \Rightarrow f \cdot x \geq f \cdot y \rangle , $$

which, by taking the contrapositive, yields

$$ \langle \forall x, y: x < y \Leftarrow P _ {x} < P _ {y} \rangle \quad (7) $$

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

$$ f _ {n} \leq n $$

$$ = {\mathrm {a r i t h m e t i c} } $$

$$ f \cdot n < n + 1 $$

$$ \begin{array}{l} \Leftarrow {(\mathrm {7}) \mathrm {w i t h} x, y := f. n, n + 1 } \ f: (f \cdot n) < f: (n + 1) \ = {0 } \ t r u e, \ \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) which quantifies over 2 dummies, or

by

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

which quantifies over a single dummy. The latter is usually the most convenient form to demonstrate 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 stan- dard 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

$$ \begin{array}{r l} & {\leq f. x} \ & {\leq \left{ \begin{array}{l l} {(2)} & {\mathrm {w i t h} n := f. x} \ {f. (f. x)} & \end{array} \right}} \ & {\leq \left{ \begin{array}{l l} {(0)} & {\mathrm {w i t h} n := x} \ {f. (x + 1)} & \end{array} \right},} \end{array} $$

whichever concludes pong , and thus the whole proof.

JAN 161-2 contains Bird's proof of pong. It is about 8 steps long, using that $f$ is increasing rather than just monotonic. I had not set out to simplify their argument, my only intention was to provide the heuristics. The subsequent simplification was a pleasant surprise.

I am grateful to the members of the ATAC with whom this problem has been discussed and whose comments contributed to the design of the above heuristics.

Austin, 6 April 1994

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