The longest plateau and other stories

The longest plateau and other stories

For a sequence $f\left( {i : 0 \leq i < N}\right) \;$ we call

$$ f (i: x \leq i < x + k) \quad \mathrm {w i t h} \quad 0 \leq x \leq x + k \leq N $$

a segment of length $k$ . (Note that the empty

sequence - i.e. $N = 0$ - contains a segment of length 0 .)

We are interested in programs msl - for maximum

segment length - that determine the maximum length of a segment satisfying some criterion B.

With the abbreviation $b$ defined by

$$ b. x. y \equiv B. f (i: x \leq i < y) \vee x = y $$

the functional specification of $m$ is

[\left{ {N : \left\lbrack {N : i : k : p}\right\rbrack : f\left( {i : 0 \leq k < p}\right) }\right} ]

；I[]c:int

$$ ; m s l {\mathcal {R}: c = (\max x, y: 0 \leq x \leq y \leq N \land b. x. y: y - x) } $$

1

]

Note. In the definition of $b$ ,the disjoint $x = y$ has been added so as to ensure that in $R$ The right-hand side is defined. From $c = 0$ we can conclude that no non-empty segment satisfies $B$ . (End of Note.)

For our first approximation we obtain the invariant $P$ by replacing in $R$ the constant $N$ by a variable and restricting its range:

${P}_{0}\colon c = \left( {\underline{\max }x,y;0 \leq x \leq y \leq n \land b.x.y;y - x}\right) \land 0 \leq n \leq N$

with the relevant properties $\left\lbrack {\left( {c,n}\right) = \left( {0,0}\right) \Rightarrow {P}{0}}\right\rbrack$ and $\left\lbrack {{P}{0} \land n = N \Rightarrow R}\right\rbrack$ . This leads to our first approxi- mation of ${ms1} :$

$$ \begin{array}{l} \left[ n: \mathrm {i n t}; c, n := 0, 0 \right. {P o } \ ; \underline {{d o}} n \neq N \rightarrow {P _ {0} \wedge n \neq N } c, n := E, n + 1 {P _ {0} } o d \ {P _ {0} \wedge n = N, h e n c e } \ ] \left{ \begin{array}{l} \mathcal {R} \end{array} \right} \ \end{array} $$

where E should be such as to justify the annotation. Remark Without apology we omit the justification for our decision to increase n each time by 1 . (End of Remark.)

In order to determine $E$ we observe under the validity of $P \land n \neq N$

$$ w p (c, n = E, n + 1 ^ {\prime \prime}, P o) $$

$$ = {\mathrm {A x i o m o f A s s i g n m e n t}, \mathrm {d e f i n i t i o n o f P o} } $$

$$ E = (\max x, y: 0 \leq x \leq y \leq n + 1 \land b. x. y: y - x) \land 0 \leq n + 1 \leq N $$

$$ = {\mathrm {p r o p e r t i e s} \mathrm {o f} M A X } $$

$$ \begin{array}{l} E = (\max x, y: 0 \leq x \leq y \leq n \land b. x. y: y - x) \underline {{\max}} \ (\max x: 0 \leq x \leq n + 1 \land b. x. (n + 1): n + 1 - x) \ \end{array} $$

$$ \begin{array}{l} \land 0 \leq n + 1 \leq N \ = {\mathrm {P O} \land n \neq N; \mathrm {p r o p e r t i e s o f M A X a n d M I N} } \ E = c \max n + 1 - (\min x: 0 \leq x \leq n + 1 \land b. x. (n + 1): x) \ = {\mathrm {s i n c e} [ b. (n + 1). b (n + 1) ] } \ E = c \max _ {n + 1} - (\min x: 0 \leq x \land b. x. (n + 1): x) \ \end{array} $$

$$ E W D 9 4 2 - 2 $$

This suggests a program with a further variable, $h$ say, to record the value of the above MIN-ex-pression, and with the invariant $P_{0} \land P_{1}$ , where $P_{1}$ is given by

$$ P _ {1}: \quad h = (\min x: 0 \leq x \land b. x. n: x) $$

Our second approximation thus becomes $P$ being initialized by virtue of b.0.0 -

$$ \left[ n, h: i n t; c, n, h := 0, 0, 0 \left{\rho_ {0} \wedge \rho_ {1} \right} \right. $$

$$ \begin{array}{l} i d o n \neq N \rightarrow {P _ {0} \wedge P _ {1} \wedge n \neq N } h := E _ {1} \ {P _ {0} \wedge P _ {1} ^ {n} _ {n + 1} \wedge n \neq N } \ ; c, n := c \max _ {n + 1 - h} n + 1 {P _ {0} \wedge P _ {1} } \ \end{array} $$

od

1

in which $E_{1}$ is defined as the solution of $h: P_{n + 1}^{n}$ or, equivalently, as the smallest natural solution

We observe that, with $P2$ given by

$$ P _ {2}: \quad n - h \leq c $$

$$ \begin{array}{l} \mathrm {(i)} \quad w p \left(" c, n := c \max n + 1 - h, n + 1 ^ {\prime \prime}, P _ {2}\right) \ = {\mathrm {A x i o m o f A s s i g n e m e n t , d e f i n i t i o n o f} P _ {2} } \ n + 1 - h \leq c \max n + 1 - h \ = {\mathrm {p r o p e r t i e s} \mathrm {o f} \underline {{\max}} } \ t r u e \ \end{array} $$

$$ \left[ (c, n, h) = (0, 0, 0) \Rightarrow P _ {2} \right] $$

hence, the invariant $P \circ {P}{1}$ of our second approxi- mation may be replaced by ${P}{1} \land {P}{1} \land {P}{2}$ . Note that,in general, ${P}{2}$ is falsified by $h : = {E}{1}$

In view of the definition of $E_{1}$ as the smallest natural solution of $x\colon b.x.(n + 1)$ the Linear Search Theorem tells us to implement $h = E_1$ by

$$ h := 0; \underline {{d o}} \rightarrow b. h. (n + 1) \rightarrow h := h + 1 \underline {{o d}} $$

which, not counting the evaluations of $b$ ,would lead to a quadratic algorithm. If, however, ${E}{1}$ is an ascending function of $n$ , $h : = {E}{1}$ could be implemented by

$$ \underline {{d o}} \rightarrow b. h. (n + 1) \rightarrow h := h + 1 \quad o d $$

which, not counting the evaluations of $b$ ,would lead to a linear algorithm. This observation is a strong suggestion to explore the consequences of

Monotonicity Assumption The smallest natural solution of $x$ : b.x.n is an ascending function of $n$ . (End of Monotonicity Assumption.)

as this might lead to a class of fast algorithms. In the rest of this note, the Monotonicity Assumption is made.

Under the monotonicity assumption, $h := E_1$ never decreases $h$ ; hence $h := E_1$ maintains $P_2$ . So, let us investigate what the precondition $P_2$ i.e. $n - h \leq c$ allows us to conclude about the adjustment of $c$ , viz.

$$ c := c \max _ {n + 1 - h} $$

The adjustment leaves c unchanged if initially n+1-h ≤c or, equivalently, n-h<c . In view of the initial validity of $P2$ , $n - h = c$ is the only remain- ing initial possibility , in which case $c$ is increased by 1 . Hence the adjustment could be coded

(0) $\begin{array}{l} n - h < c \rightarrow s\mathrm{{kip}} \ n - h = c \rightarrow c \mathrel{\text{:=}} c + 1 \end{array}$

It is nice to know that $c$ will be increased by 1 at a time. Let us now turn to a possible optimization: suppose we can think of a $Q$ such that

(i) $Q$ is stable, i.e. is maintained by the repeated statements and, hence, when once true, remains true, and (ii) is such that $Q$ implies in conjunction with with the precondition of (0) that $n - h < c$ holds. In that case, $c$ has reached its final value as soon as $Q$ holds and, hence, we can strengthen the guard $n \neq N$ to $n \neq N \land \neg Q$ , thereby possibly causing termination after fewer iterations.

From the preconditions, POI $n \neq N$ implies

Q: $N - h \leq c$

meets requirement (ii). If also meets requirement

(i) since, the repeated statements don't decrease c and under the monotonicity assumption don't decrease h and ,hence, don't falsify Q . (The stability conclusion re Q is our last exploitation

EWD942-5

of the monotonicity assumption.) So, without in- fluencing the final value of $c$ , we may replace the guard by $n \neq N \land N - h > c$ . But this can now be simplified: in conjunction with invariant $P_{2}$ -i.e. $n - h \leq c$ - $N - h > c$ implies $n \neq N$ , which conjunct can therefore be omitted. (This is our last usage of $P_{2}$ .)

Collecting the above, we come -under the monoloni-city assumption- to our third approximation for

$$ \begin{array}{l} \llbracket n, h: i n t; c, n, h := 0, 0, 0 \ ; \underline {{d _ {0}}} N - h > c \rightarrow h := E _ {1} \ i f n - h < c \rightarrow s k i p \ ] n - h = c \rightarrow c := c + 1 \ f _ {i} \ ; n := n + 1 \ \end{array} $$

od

1

Comment I have hesitated about the order in which to introduce P2 and the Monotonicity Assumption, because it is only under the latter that the former becomes of interest. Because P2 does not depend on the monotonicity assumption I have finally decided to introduce it first. (End of Comment.)

The monotonicity assumption is now interesting enough to be explored a little further, in particular we would like to have manageable criteria for determining whether it is satisfied. Fortunately we have a strong theorem, easily expressed in terms of our original predicate $\mathcal{B}$ on strings -now with $B \phi$ -Theorem0 The Monotonicity Assumption $\equiv$

$$ (A X, Y: B. (X Y): B. X) $$

Proof

(i) LHS RHS

In the following, quantifications are constrained by $0 \leq x < k \leq n < m \leq N$ . The Monotonicity Assumption = {definition} the minimal natural solution of $x$ : b.x.n is an ascending function of $n$ $= {$ definition of minimal natural solution $}$ $\Leftrightarrow {$ predicate calculus [\left( {A,k,n,m : \left( {{Ax} : 7{b}{x}.n \Rightarrow 7{b}{x}.m}\right) }\right) ] $= {$ predicate calculus $}$ $\left( {A,k,n,m : \left( {{Ax} : b.x.m \Rightarrow b.x.n}\right) }\right)$ $\Leftarrow \left{ \begin{array}{l} \text{ definition of }B \ \text{ (A) }\;Y : B.\left( {X,Y}\right) : B.X) \end{array}\right.$

(ii) ${LHS} \Leftarrow {RHS}$

From $\neg$ RHS we conclude that we can choose an $X$ and $Y$ such that $\neg B.X$ and $B.(XY)$ .

Choose no, n1 and f such that

$$ p (i: 0 \leq i < n 0) = X \quad a n d \quad p (i: n 0 \leq i < n 1) = Y. $$

From $\neg \mathrm{B}.\mathrm{X} \land \mathrm{B}.\left( {\mathrm{{XY}}\text{)}}\right)$ we conclude -on account of the definition of $b - 7$ b.o.no $\land$ b.o.n1,and that $Y$ is not empty,i.e. ${n0} < {n1}$ . That is,the minimal natural solution of $x : b.x.{no}$ exceeds 0,that of $x : b.x.{n1}$ equals 0 . Hence the Monotonicity Assumpa- tion is not satisfied. (End of Proof.)

Comment I don't like the above proof, which caused me a lot of trouble to write down. The fact that I had to prove an equivalence by mutual implication does not bother me, as this is not unusual when dealing with minimal solutions. What somehow annoys me very much is that the two halves are written in such very different styles. (End of Comment.)

Though I have reservations about the above proof. I like the theorem very much, because (i) it expresses an equivalence, in particular also tells us when the Monotonicity Assumption is not satisfied, and (ii) its right-hand side

(A $X,Y,B.\left( {XY}\right) : B.X)$

is so neat that there must be some nice theory about predicates satisfying (1), nice enough to be useful.

Let us call predicates $B$ satisfies (1) "right-strengthening". Then we can formulate Theorem 1. Disjunction and conjunction of two

EWD942-8

right -strengthening predicates are both right-streng

Proof

$\left( {{AX},Y;{Bo}.\left( {XY}\right) ;{Bo}.X}\right) \land \left( {{AX},Y;{Bi}.\left( {XY}\right) ;{Bi}.X}\right)$

[\left{ \begin{array}{ll} \text{predicate calculus } \ \end{array}\right} ]

$\left( {A \times Y,B}\right) = \left( {{XY} \cup B}\right) = \left( {X \cup Y}\right) \cup \left( {Y \cup B}\right) .$

(A) $X,Y : {BO}.\left( {XY}\right) \land {BI}.\left( {XY}\right) : {BO}.X \land {BI}.X$ )

(End of Proof)

Remark. A segment is called a "slope" if it is ascending or descending. Everybody who ever made a mess of it when trying to solve W.H.J. Feigen's problem of determining the maximum slope length - and there are many such people - will appreciate the insight captured by the above theorem. (End of Remark.)

For right-strengthening B, string X and "charac-

B. $(x, y) \Rightarrow B, X$

that is, there exists a boolean function $d$ of a string and a character such that

$B.\left( {x,y}\right) \equiv B.X\;A.D.X.y$

• the weakest d being

$d.x.y \equiv B.\left( {x,y}\right) v \cap B.X$

By induction on the length of the string we conclude

Theorem 2. Consider

(A) $\because B \cdot X \equiv \left( {\underline{A}{Y}{y}Z : {Y}{y}Z = X : d.Y.y}\right) \vee X = \phi$ );

EWD942-9

then (i) for any given d, there exists a right-strengthening B satisfying (2), and (ii) for any given right-shreNGTHening $B$ ,there exists a d satisfies ${P}_{2}$ .

Also Theorem 2 gives much satisfaction; it is useful to know because, in case of Freedom, it makes sense to choose one's d most conveniently.

At last we should be ready for the famous Problem of the longest Plateau. [I must confess to observe with great pleasure how long I have managed to postpone this stage.]

A plateau is defined as a segment all whose elements are equal. We recommend for d

$$ d. Y. y \equiv y = h e a d. (Y y) $$

i.e. we write b.x.y as

$$ b. x. y = (\underline {{A}} _ {j}: x \leq j < y: f. x = f. j) $$

From our third approximation we derive

$$ \left[ n, h: \mathrm {i n t}; c, n, h := 0, 0, 0 \right. $$

$$ \begin{array}{l} ; \underline {{d o}} N - h > c \ \rightarrow i f f. h = f. n \rightarrow s k i p [ ] f. h \neq f. n \rightarrow h := n f _ {i} \ ; \mathrm {i f} n - h < c \rightarrow s k i p ] n - h = c \rightarrow c := c + 1 p _ {i} \ ; n := n + 1 \ \end{array} $$

$$ o d $$

$$ 3 1 $$

Let us study our solution a bit further: what is the initial condition under which an iteration increases $c$ ? To this purpose we evaluate

$$ \begin{array}{l} w p (” i f \rho_ {h} = f _ {n} \rightarrow s k i p) [ \rho_ {h} \neq f _ {n} \rightarrow h := n \rho_ {i} ^ {\prime \prime}, n - h = c) \ = {\text {s e m a n t i c s} } \ \end{array} $$

$$ (f, h = f, n \land n - h = c) \lor (f, h \neq f, n \land 0 = c) $$

The condition $0 = c$ is so strong that the second disjunct never occurs: in fact, $P3$ - to all intents and purposes its negation-

[{P}_{3}\text{:}\;f\left( n\right) = f.n \vee 0 < c]

is a further invariant. (P3 is implied by

$$ (n, h, c) = (0, 0, 0) \quad v \quad 0 < c $$

the invariance of which is straightforward to establish.)

The invariance of $P3$ allows the annotation

$$ f \cdot h \neq f \cdot n \rightarrow {0 < c } h := n {n - h < c } $$

and hence the option of adjusting c can be con- fined to the first alternative:

$$ \left[ n, h: \mathrm {i n t}; c, n, h := 0, 0, 0 \right. $$

$$ \begin{array}{l} ; \underline {{d o}} N - h > c \rightarrow i f f. h = f. n \rightarrow i f n - h < c \rightarrow s k i p \ \vert n - h = c \rightarrow c := c + 1 \ \end{array} $$

p

$$ \mathrm {i f} f \cdot h \neq f \cdot n \rightarrow h := n $$

$$ f _ {i}: n := n + 1 $$

ad

31

The condition for increase of $c$

$$ f \cdot h = f \cdot n \wedge n - h = c $$

is equivalent to

$$ f. (n - c) = f. n \wedge n - h = c $$

and we could ask ourselves under which circum- stance the first conjunct -which does not contain h - implies the second, for then the test $n - h = c$ is no longer needed and we may be able to dispense with h altogether . In view of $P2$ it suffices to demonstrate the weaker

(3) $f\left( {n - c}\right) = f.n \Rightarrow n - h \geq c$

The right-hand side is equivalent to $h \leq n - c$ and $h$ being the smallest natural solution of $x$ : b.x.n, we can prove (3) provided we can show

$$ f. (n - c) = f. n \Rightarrow b. (n - c). n $$

$- n - c \geq 0$ being trivially invariant- , i.e.

$$ f _ {n} (n - c) = f _ {n} \Rightarrow (\underline {{A}} j: n - c \leq j < n: f _ {n} (n - c) = f _ {j}) $$

This implication holds for on $f$ in which equal values are nowhere separated by different ones. Let us call such an "equality compact".

Replacing the guard N-hxC by the original $n\neq N$ , we can eliminate for equality-compact

[ n: int ; c, n := 0, 0

$$ \begin{array}{l} i \underline {{\underline {{d o}}}} n \neq N \rightarrow i f f (n - c) = f. n \rightarrow c, n := c + 1, n + 1 \ | f. (n - c) \neq f. n \rightarrow n := n + 1 \ p _ {i} \ \end{array} $$

$$ \underline {{o d}} $$

1

This is the program David Gries gives on p.203 of "The Science of Programming". (He restricts himself to ordered $f^{\prime}$ -ascending or descending-, which is a special case of equality-compact $p$ ; for unclear reasons he has chosen to restrict himself to the case $N \geq 1$ .)

So much for the problem of The Longest Plateau.

In retrospect I should have defined the function

$$ g \quad b y $$

$$ g. n = \mathrm {t h e s m a l l e s t n a t u r a l s o l u t i o n o f} x: b. x. n; $$

and instead of " $h \mathrel{\text{:=}} E$ " rather " $h \mathrel{\text{:=}} g \cdot {\left( n + 1\right) }^{n}$ . I could then have used $g$ in arguments as well. (End of In retrospect.)

Wasn't this fun?

Austin, 10 October 1985

prof. $d\mathrm{r}$ . Edsger W. Dgksstra

Department of Computer Sciences The University of Texas at Austin

Austin, TX 78712-1188

$$ u s A $$