Ascending functions and The Welfare Crook

Ascending functions and The Welfare Crook

I was very familiar with the definitions of "increasing" and "ascending":

(0) ( $f$ is increasing) $\equiv \left( {\underline{A}x,y : x < y \Rightarrow f.x < f.y}\right)$ (1) $\left( {f\text{ is ascending}}\right) \equiv \left( {\underline{A}x,y : x < y \Rightarrow f.x \leq f.y}\right)$

from which two it directly follows that an increasing Function is ascending as well. I here offer the al-. ternatives

(2) $\left( {f\text{ is increasing}}\right) \equiv \left( {\underline{\exists }x,y : x < y \equiv f.x < p.y}\right)$ (3) $\left( {f\text{ is ascending}}\right) \equiv \left( {\underline{A}{x}_{1}y\therefore x < y \Leftarrow f.x < f.y}\right)$

Proof of (3)

$$ \begin{array}{l} (f i s a s c e n d i n g) \ = {(1), r e n a m i n g t h e d u m m i e s } \ (A x, y: \quad y < x \Rightarrow f. y \leq f. x) \ = {\mathrm {L e i b n i z} } \ (\underline {{A}} x, y: y < x \Rightarrow f. y \leq f. x) \land \ (\exists x, y: \quad y = x \Rightarrow f. y \leq f. x) \ = {\mathrm {p r e d . c a l c .} } \ \underline {{(A x , y)}}: y \leq x \Rightarrow f. y \leq f. x) \ = {p r e d. c a l c. a n d 7 (b \leq a) \equiv a < b } \ (\underline {{A}} x, y: \quad x < y \Leftrightarrow f. x < f. y) \ \end{array} $$

(End of Proof of (3).)

Formula (2) now immediately follows.

The problem of The Welfare Crook - see David Gries "The Science of Programming" - is to locate the smallest value common to three ascending sequences. Here we shall solve the problem in the style of EWD1029. For the sake of brevity we shall use $a, b, c \leq d, e, f$ to denote

$$ a \leq d \land b \leq e \land c \leq f $$

and similarly for other relational operators. Our program operates on the variable triple $i,j,k$ and has to establish $R$ ,given by

$$ R: \quad i, j, k = I, J, K $$

Our first approximation

$$ t e x t o: i, j, k := I, J, K {R } $$

however, has to be rejected, because I,J,K is given implicitly. It is given that

(i) $I,J,K$ is a triple of natural numbers

Exploiting (i) we derive in the (absolutely) stan- dard manner

$$ \mathrm {t e x t 1 :} {0, 0, 0 \leq I, J, K } $$

$$ \begin{array}{l} i, j, k := 0, 0, 0 {0, 0, 0 \leq i, j, k \land i, j, k \leq I, J, K } \ i \neq I \rightarrow i = i + 1 \ [ j \neq J \rightarrow j := j + 1 \ 0 k \neq k \rightarrow k = k + 1 \ \operatorname {o d} {R } \ \end{array} $$

For the termination argument, $(I + J + K) \cdot (i + j + k)$ is the (truly!) obvious candidate. Still the triple $I, J, K$ occurs. We are given that

(ii) $I,J,K$ is associated with the triple $f,g,h$ of ascending functions.

Knowing that, as far as invariance and termination are concerned, guards may be strengthened, and aware of (3) as characterization of a function being ascending, we are invited to observe

$$ \begin{array}{l} i \ne I \ \Lleftarrow {\mathrm {i n v i e w o p} (3) \mathrm {a n d} i \leq I } \ i < I \ \Leftrightarrow {(3), \mathrm {s e e N o t e i n P o s t s c r i p t} } \ f _ {i} < f. I \ \end{array} $$

and similarly for the other two cases. This leads to

[\text{text}{2} : { 0,0,0 \leq {I}{1}{J}{1}K} ]

$$ \begin{array}{l} i, j, k := 0, 0, 0 {0, 0, 0 \leq i, j, k \land i, j, k \leq I, J, K } \ ; \underline {{d o}} f. i < f. I \rightarrow i := i + 1 \ \mathrm {I} g; j < g. J \rightarrow j := j + 1 \ ] h. k < h. k \rightarrow k := k + 1 \ \underline {{o d}} \ \end{array} $$

Note that, the guards having been strengthened, we can no longer assert ${R}$ as postcondition. What has been given about $f.I,g.J$ ,and $h.K$ ? Well, that they are equal. Instead of formulating that as the existence of an $X$ such that $f.I,g.J,h.K \equiv X,X,X,$

we abstain from the introduction of $X$ - "Omit needless identifiers"?- and state that we are given

$$ (i i i) \quad f: I, g. J, h. K = g J, h. K, f. I $$

which invites us to observe

$$ f _ {i} < f _ {I} $$

$$ \begin{array}{l} = {(i i i) } \ f _ {i} < g. J \ \end{array} $$

$$ \begin{array}{l} \Leftrightarrow {\mathrm {s e m i - r a b b i t} } \ p _ {i} < g; j \land g; j \leqslant g; j \ \Leftrightarrow {g \mathrm {i s a s c e n d i n g , s e e N o t e i n P o s t s c r i p t} } \ f _ {i} < g \cdot j \land j \leq J \ \end{array} $$

and cyclically for the two other programs. This leads

$$ \begin{array}{l} t e x t {3}: {0, 0, 0 \leq I, J, K } \ i, j, k := 0, 0, 0 {0, 0, 0 < i, j, k \land i, j, k \leq I, J, K } \ ; \underline {{\underline {{d o}}}} f. i < g. j \rightarrow i := i + 1 \ \mathrm {I} g \cdot j < h \cdot k \rightarrow j := j + 1 \ ] h. k < f. i \rightarrow k := k + 1 \ \mathrm {o d} {i, j, k \leq I, J, K \land f. i, g. j, h. k = g. j, h. k, f. i } \ \end{array} $$

(Replacing in the last conjunct $= {by} \geq$ does not

change its value.) So we may conclude $R$ from

the above post condition, we are given

$$ \mathrm {(i v)} f. i, g. j, h. k = g. j, h. k, f. i \Rightarrow i, j, k \geq I, J, K \mathrm {f o r a l l} i, j, k $$

which pins I,J,K down as locating the first common

value of the three sequences. (See Post ${}^{2}$ script.)

The "semi-rabbit" refers to the use of the theorem

$$ (4) \quad a < c \Leftrightarrow a < b \land b \leq c $$

which should have a name but doesn't. Here we appeal to it because it is a way of isolating $J$ in a conjunct -viz $g.j \notin g.J$ - with which we can cope. (In EWD1016 -6 we appealed to it because the inequality "a<b" had to be used.) Theorem (4) deserves a name and a little theory about when its use is indicated.

Postscript Relation (1) is an ugly relic from one of my previous incarnations and should be forgotten as soon as possible. Omitting universal quantification over $x, y$ :

• function application preserves $=$ (known as the Rule of Leibniz), i.e

$$ \begin{array}{l} x = y \Rightarrow f _ {x} = f _ {y} \quad \mathrm {o r , e q u i v a l e n t l y ,} \ x \neq y \iff f _ {x} \neq f _ {y} \ \end{array} $$

• application of an increasing function $f$ preserves $<$ (and $>$ ),i.e.

$$ \begin{array}{l} x < y \Rightarrow f. x < f. y \qquad \mathrm {o r , e q u i v a l e n t l y .} \ x \leq y \Leftrightarrow f \cdot x \leq f \cdot y \ \end{array} $$

• application of an ascending function $p$ preserves $\leq$ (and $\geq$ ),i.e.

$$ \begin{array}{l} x \leq y \Rightarrow f \cdot x \leq f \cdot y \quad o r, e q u i v a l e n t l y, \ x < y \Leftarrow f. x < f. y \ \end{array} $$

The reader can find the analogous characterization of "decreasing" and "descending", which, due to their "antimonotonicity", cannot be formulated in terms of just preservation.

Note It is the above characterization of ascendingness that has been used in the observations leading to text2 and text3. (End of Note.)

(End of Postscript.)

Post'script The above was written at a moment that I was not aware of WF107 (though I had seen it before the summer) which is also directly inspired by the linear search as we have described it in EWD1029 and which, consequently, shows more than superficial similarity. Fegen decomposes what has been given about I,J,K differently, the main distinctions being that

he does not make a very distinct point of the fact that the functions $f, g, h$ are ascending - (with hesitation) he introduces (and uses) a name for the smallest common value.

His final argument that text2 establishes R requires 10 steps (and, understandably, he is not satisfied)

He first defines $X$ as the smallest common value and then $I, J, K$ as the "locations" of its "first" occurrences. (This is only a sketch: he does this impeccably.)

In a way, my gain has been obtained by means of the sin of omission: I have not analysed the circumstances under which the equations

(5) $I, J, K: (iii)$ and $I, J, K: (iv)$

have a common solution. e.g. when $I, J, K: {i}$ is solvable: the existence of a common solution then relies on $f, g, h$ being a triple of ascending functions.

Warning The program called "text2" can not be taken as the existence proof of a common solution of (5): replace (iv) by false! (End of Warning.) (End of Post'script.)

Ref:

W.H.J. Fegen WF107: "The Welfare Crook taken as an exercise in problem decomposition

Austin, 11 Oct. 1988

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