The Saddleback Search

The Saddleback Search

The origin of this algorithm is unknown; its name has been invented by David Gries. It solves a problem that can be stated in many variations; we shall first solve it in one of its straightforward versions and then discuss several variations.

We are given an integer function $f$ of two na-tural arguments that is increasing in both its arguements and takes on the value $F$ at least once. Saddleback Search has to locate such an occur-rence, more precisely, the occurrence with the smallest value of the first argument. Because $f$ is increasing in both its arguments, this is at the same time the occurrence with the largest value of the second argument. Thus we are lead to the following formal specification

1[F: int; $f\left( {i,j : 0 \leq i \land 0 \leq j}\right)$ array of int

$$ {(a, b, c): 0 \leq i < i i \wedge 0 \leq j < j j: p _ {i, j} < p _ {i, i j} \wedge p _ {i, j} < p _ {i, i j}) \wedge $$

$$ f. X. Y = F \land (\underline {{A}} i, j: 0 \leq i < X \vee j > Y: f. i. j \neq F) 3 $$

$$ ; \prod x, y: i n t $$

$$ ; S a d d k e b a c k S e a r c h $$

$$ {R: x, y = X, Y } $$

$$ ] ] $$

$$ 1 1 $$

The analogy with the Linear Search now suggests to approach X from below and Y from above, i.e. to iterate with the invariant P , given by

$P : \;0 \leq x \leq X \land y \geq Y$

our first approximation of Saddleback Search keeps the analogy to the linear Search as close as pos-sible:

"establish P"

$\therefore \underline{do} x < X \rightarrow x : = x + 1{P} \parallel y > Y \rightarrow y = y - 1{P}$ od ${R} .$ We note that this program differs in two respects from the corresponding approximation -see EWD930- of the Linear Search: firstly -on account of the conjunct $y \geq r -$ the initialisation cannot be done independently of $f$ (" $y \mathrel{\text{:=}} t \infty$ " is not acceptable) and secondly the repetition here is nondeterministic.

In order to relate our inequalities involving $X$ and $Y$ to $f$ ,we observe the

[\text{Lem}n \quad x \leq X \land y \geq Y \equiv ]

Proof. $x \leq {X}^{ - } \land y \geq Y$ $\Rightarrow \left{ {\left( {\underline{A}i,j : 0 \leq i < X \vee j > Y : {p}{i,j} \neq F}\right) }\right.$ $\left( {\underline{A}i,j : 0 \leq i < x \vee j > y : {p}{i,j} \neq F}\right)$ $\Rightarrow \left{ {\left{ {{f}_{i}x,y = F \land {X \geq 0}}\right} }\right.$ $X \geq x \land Y \leq y$ (End o)

With the above Lemma in our hands we now tackle the guards of the repetition, strengthened by the invariant:

$$ p _ {\wedge} x < X $$

$$ = {\mathrm {a r i t h m e t i c a n d d e f i n i t i o n o f} P } $$

$$ P \wedge x + 1 \leq X \wedge y \geq Y $$

$$ = {\mathrm {L e m m a} } $$

$$ P \wedge (A _ {i j}: 0 \leq i < x + 1 \vee j > y: f _ {i j} \neq F) $$

$$ = {\mathrm {d e f i n i t i o n o f} P, \mathrm {L e m m a a n d p r e d i c a t e c a l c u l u s} } $$

$$ P \wedge (\underline {{A}} j: 0 \leq j \leq y: f _ {X} j \neq F) $$

$$ \Leftarrow {f \mathrm {i s i n c r e a s i n g i n i t s s e c o n d a r g u m e n t} } $$

$$ P \land P. x. y < F, $$

and

$$ \begin{array}{l} P \land y > X \ = {\mathrm {a r i t h m e t i c a n d d e f i n i t i o n o f} P } \ P \land x \leq X \land y - 1 \geq Y \ = {\mathrm {L e m m a} } \ P \hat {=} (A i, j: 0 \leq i < x v j > y - 1: P. i, j \neq F) \ = {\mathrm {d e f i n i t i o n} P, \mathrm {l e m m a}, \mathrm {a n d p r e d i c a t e c a l c u l u s} } \ P \wedge (\exists i: i \geq x: P. i. y \neq F) \ \Leftrightarrow {f _ {i} \mathrm {i s i n c r e a s i n g i n i t s f i r s t a r g u m e n t} } \ P \vdash f. x. y > F \ \end{array} $$

Hence we find ourselves invited to consider the second approximation with the (conditionally)

strengtthened guards

"establish P"

$$ ; \underline {{d o}} f. x. y < F \rightarrow x := x + 1 {P 3 } ] f. x. y > F \rightarrow y := y - 1 {P 3 } \underline {{d}} $$

for which we have to check that, though the guards have been strengthened, the final conclusion

R is still justified. Indeed:

$$ \begin{array}{l} P \land F. x. y \geq F \land F. x. y \leq F \ = {\mathrm {a r i t h m e t i c} } \ P \wedge P \cdot x \cdot y = F \ = {\mathrm {d e f i n i t i o n} P \mathrm {a n d} X, Y } \ \end{array} $$

$$ x, y = X, Y $$

Because $f$ is increasing in both arguments,

$$ \begin{array}{r l}&{x, y := 0, 0}\&{; \underline {{d o}} \quad \mathrm {f . x . y < F} \rightarrow \mathrm {y := y + 1} \quad \underline {{o d}} \quad {\mathrm {P} }}\&{; \underline {{d o}} \quad \mathrm {f . x . y < F} \rightarrow \mathrm {x := x + 1}}\&{\quad \overline {{\mathbb {I}}} \quad \mathrm {f . x . y > F} \rightarrow \mathrm {y := y - 1}}\&{\underline {{o d}} \quad {\mathrm {R} }}\end{array} $$

Convergence of the first repetition is guaranteed by the fact that $f_{x.y}$ is increasing in its second component.

We observed at the beginning that the occurrence of $F$ with the smallest value of the first argument is also that with the largest value of the second argument. Consequently we could also have defined $x, y$ as the solution of $x, y: (f.x.y = F)$ with the minimum value for $x - y$ :

$$ p. X. Y = F \land (A _ {i, j}: 0 \leq i \land j \leq 0 \land i - j < X - Y: p. i, j \neq F). $$

The disadvantage of this definition is that, for the proof of our Lemma, another appeal to $f$ 's double monotonicity would be required. It has the advantage that a first approximation -viz. to investigate values of $f$ x.y for increasing values of x-y - would have been a more direct analogue of the linear search. The approach has a further heuristic virtue.

Under the invariant $x - y \leq x - y$ ,the search would continue until $x - y = X - Y$ . But those two condi. tions do not imply

$$ x, y = X, Y \equiv x - y = X - Y \land x \leq X \land y \geq Y $$

• a nice litthe theorem I did not know - and we are thus led to the stronger invariant $x \leq x \land y \geq Y$ . (I did this derivation as well, and it was kind of nice; it was essentially the case analysis needed in the proof of the Lemma, that put me off.)

The first variation is Saddleback Count, which, instead of locating an occurrence, counts the number of occurrences. It does so in the order of increasing $x - y$ . Formally specified

[F: int; $p\left( {i,j : 0 \leq i \land 0 \leq j}\right)$ array of int

$$ {(A, i, j, i i, j j): 0 \leq i < i i \wedge 0 \leq j < j j: P _ {i. j} < P _ {i i. j} \wedge P _ {i. j} < P _ {i. j j}) \wedge $$

$$ K = (\underline {{N}} (i, j): 0 \leq i \land 0 \leq j: P _ {i j} = F) } $$

； $1\left\lbrack {k : \text{int}}\right\rbrack$

; Saddleback Count

$$ {R: k = k } $$

71

${a}{1}^{2} + {a}{2}^{2} + {a}_{3}^{2}$ 64

The invariant $P$ is given by

$$ P: k = (\underline {{N}} (i, j): 0 \leq i < x \vee j > y: P. i. j = F) $$

or,equivalently

$$ E W D 9 3 4 - 5 $$

$P : \;k + \left( {\underline{N}\left( {i,j}\right) : i \geq x \land 0 \leq j \leq y : p\text{.}i,j = F}\right) = k$

A solution for Saddleback Count is

$$ \begin{array}{l} 1 5 x, y: i n t \ ; x, y, k := 0, 0, 0; \underline {{\mathrm {d o}}} F. x. y < F \rightarrow y := y + 1 \underline {{\mathrm {o d}}} {P } \ i \underline {{\underline {{d o}}}} y \geqslant 0 \rightarrow i f f. x. y < F \rightarrow x := x + 1 \ [ P. x. y > F \rightarrow y := y - 1 \ [ f. x. y = F \rightarrow x, y, k := x + 1, y - 1, k + 1 \ \left{ \begin{array}{l} P _ {i} \ P _ {j} \end{array} \right} \ \operatorname {o d} {R } \ \end{array} $$

XI{R}

which, I trust, now requires no further explanation.

A next variation is that in the declaration of $p$ the first argument is bounded by $0 \leq i < I$ and/or the second argument is bound by $0 \leq j < J$ .

0≤i<1 : this bound has no influence on the text of Saddleback Search; for Saddleback Count the guard y≥o of the last repetition has to be replaced by the stronger xI a y≥o so as to prevent "index out of bounds". The proper repor- malation of the invariants is left as an exercise to the reader.

$0 \leq j < J$ : in Saddleback Search $P$ is established by $x,y \mathrel{\text{:=}} 0,\mathrm{\;J} - 1$ ,in Saddleback Count

$$ E W D 9 3 4 - 6 $$

The next variation to consider is a weakening of the monotonicity requirements on $f$ from increasing to ascending.

Saddleback Search is also okay for an f that is ascending in its first and increasing in its second argument. If $p$ is only given to be ascending in both arguments, the program for bounded second argument is still okay, but for unbounded second argument the establishment of $p$ has to be effected by

$$ ; \underline {{\underline {{d o}}}} F. x. y \leqslant F \rightarrow y := y + 1 \quad \mathrm {o d} $$

and $f$ has to be such that this repetition converges, i.e., for increasing $y$ ,f.o.y has to grow

In the case of Saddleback Count we have in any case to insist that $k$ exists (i.e. is finite), which is the case if both arguments are bounded from above or $f_{x.y}$ grows beyond $F$ for in-creasing $x + y$ . If, in addition, $F$ is increasing in one of its arguments, its second one, say, it suffices to modify the third guarded command of the alternative construct from

$$ p \cdot x \cdot y = F \rightarrow x, y, k := x + 1, y - 1, k + 1 $$

into

$$ f. x. y = F \rightarrow x, k := x + 1, k + 1 $$

(the original being an optimization of the latter which is valid if $p$ is increasing in its first argument).

For Saddleback Count applied to an f given to be ascending in both unbounded arguments and p.x.y growing beyond F for increasing x+y, we strengthen the invariant to PwQ with P (as before) given by

$$ P: \quad k + (\underline {{N}} (i, j): i \geq x \land 0 \leq j \leq y: f _ {i, j} = F) = K $$

and $Q$ given by

$$ Q: \quad (\underline {{A}} i: x \leq i < z: f. i. y \leq F) $$

Invariant Q states the relevant property of z which has been introduced for the purpose of efficiency. Note that neither $x \coloneqq x + 1$ nor $y \coloneqq y - 1$ falsifies Q, nor $z \coloneqq z \max x$ .

$$ \mathbb {I} _ {x, y, z: i n t} $$

$$ ; x, y, z, k := 0, 0, 0, 0; \underline {{d o}} f. x. y \leq F \rightarrow y := y + 1 \underline {{d}} {P \wedge Q } $$

$$ ; \underline {{d o}} y \geq 0 \rightarrow $$

$$ \begin{array}{l} i f f. x. y < F \rightarrow x := x + 1 {P \wedge Q } \ \mathrm {I I} f \cdot x \cdot y > F \rightarrow y := y - 1 \quad (P \land Q) \ | f. x. y = F \rightarrow z := 2 \max x {Q ^ {\prime}: (\underline {{A}} i: x \leq i < 2: f. i. y = F) } \ ; \underline {{d o}} f. 2. y = F \rightarrow z := z + 1 \underline {{o d}} {Q ^ {\prime} \wedge f. 2. y \neq F } \ ; y, k := y - 1, k + 2 - x {P \wedge Q } \ \end{array} $$

${P}_{i}$

$\frac{a - b}{a + b} = \frac{c - d}{c + d}$

J

We finally mention that it may be worthwhile to replace the linear searches by logarithmic ones. We could replace, for instance,

$$ \mathrm {d o} f. x. y \leqslant F \rightarrow y := y + 1 \mathrm {o d} $$

by

$$ i f f. x. y > F \rightarrow s k i p $$

$$ \iiint_ {D} f. x. y \leqslant F \rightarrow $$

$$ 1 1 [ v: i n t; v := 1 {f. x. y \leq F a n d v i s p o w e r o f 2 } $$

$$ ; \underline {{\underline {{d o}}}} F \geq f. x. (y + v) \rightarrow v := 2 * v \underline {{o d}} $$

$$ {F. x. y \leq F < F. x. (y + v) a n d v i s p o w e r o f 2 } $$

$$ ; \underline {{d o}} v \neq 1 \rightarrow v := v / 2 $$

$$ \begin{array}{l} i f f \cdot x. (y + v) \leq F \rightarrow y := y + v \ [ F < f. x. (y + v) \rightarrow s k i p \ f _ {1} \ \mathrm {o d}; y := y + 1 \quad {f. x. (y - 1) \leq F < f. x. y } \ \end{array} $$

1

The other three linear searches can be treated similarly. Note that the worst case remains linear, viz. when in the original execution we have a long execution of alternations of $x := x + 1$ and $y := y - 1$ .

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

Austin 5 Sep. 1985