1274

For the record: Yossi Shiloach’s Algorithm

EWD1274 · 1995–2000 · PDF · Source language: English. · Local OCR-derived source needs manual review.

For the record: Yossi Shiloach's Algorithm

We are given a positive integer $N$ and two, say, integer functions $A$ and $B$ on the integers, which have both period $N$ . i.e.

A. $k = A.\left( {k + N}\right)$ and $B.k = B.\left( {k + N}\right)$ for all $k$ , and are asked to design an algorithm determining whether they are the same function but for a possible shift of the argument,more precisely,the value of the boolean variable should be made to satisfy the postcondition

R: eq $\equiv \langle \exists i\therefore \left\langle {\forall k : A.\left( {i + k}\right) = B.k}\right\rangle \rangle$

Our first remark is that in the above formalization of the postcondition, the symmetry in A and B has been destroyed by the introduction of i . We can restore the symmetry by intra- ducing a j as well , and rewrite

R: eq $\equiv$ 〈3i,j:<A.(i+k)=B.(j+k)〉

Our next remark is that thanks to the periodicity of $A$ and $B$ , the

universal quantification can be confined to $N$ consecutive values of $k$ :

R: eq

$$ \langle \forall k: 0 \leq k < N: A. (i + k) = B. (j + k) \rangle $$

$$ > \quad . $$

In the rest of this text, the symmetry

between the pairs $\left( {A,i}\right)$ and ${\left( B,j\right) }^{4}$

will be maintained.

We first analyse the case that

$$ e q := \mathrm {f r u e} $$

would establish $R$ . In that case, the

the algorithm would have to establish

for some $i,j\;$ the truth of

${R}^{\prime } : \;\left{ {\forall k : 0 \leq k < N : A.\left( {i + k}\right) = B.\left( {j + k}\right) }\right}$

since the $N$ terms of this quantified

expression are independent, their

truths have to be 'verified individually.

We adopt the standard solution, i.e.

we introduce a variable, $h$ say,

that satisfies

$P : \langle \forall k : 0 \leq k < h : A.\left( {i + k}\right) = B.\left( {j + k}\right) \rangle \land 0 \leq h$

and make the (standard) observations that

$h = 0 \Rightarrow P$ (ii) the guarded command

$$ A. (i + h) = B. (j + h) \rightarrow h := h + 1 $$

maintains the truth of $P$ ,and

(iii) $P \land N \leq h \land {eq} \Rightarrow R$ ,

which leads to the program skeleton

$$ \begin{array}{l} \begin{array}{l} \mathrm {I l v a r h , i , j : i n t} \end{array} \ ; h, i, j := 0, \dots {P } \ ; \underline {{d o}} h < N \rightarrow \ i f A. (i + h) = B. (j + h) \rightarrow h := h + 1 f i \ o d {R ^ {\prime} } \ ; e q := t r u e \ \left{ \begin{array}{l} R \end{array} \right} \ \end{array} $$

If this program skeleton does not abort, it establishes eq $\equiv$ true , as if should. If it aborts because of finding

$$ A. (i + h) \neq B. (j + h) $$

this can be for two reasons: either

another $i,j$ - combination is needed to

establish ${R}^{\prime },$ or eq $\equiv$ false should hold

in the final state. With this in mind we

shall try to supply the missing alternative

$$ A _ {i} (i + h) \neq B _ {j} (j + h) \rightarrow \dots \dots $$

At the moment this alternative is selected, the truth of $P$ tells us that $h$ equalities have been established, and the values of $i, j$ determine which. An assignment to $i$ or $j$ in general falsifies $P$ and thereby destroys this information (which was time-wise expensive to collect when $h$ is large). The question is therefore whether we can save some of it, i.e. from the situation pictorially represented by

$A.\left( {i + h - 1}\right)$

A.(i+h)

[\frac{B.J}{h}\frac{B.\left( {j + h - 1}\right) }{h}]

B. $\left( {j + h}\right)$

Shiloach's invention has been to impose -if not already present- a total order $<$ on the values compared, i.e

$A.\left( {i + h}\right) \neq B.\left( {j + h}\right) \equiv A.\left( {i + h}\right) < B.\left( {j + h}\right) < B.\left( {j + h}\right) < A.\left( {i + h}\right) .$

Let us focus on the situation in which the left conjunct holds, i.e.

$A.\left( {i + b - 1}\right)$

A.(i + h)

[\frac{B.J}{h}\frac{B\left( {j + h - 1}\right) }{h}]

B. (j+h)

for now we see a situation in which the

notion of "the lexical order" of strings is a relevant concept. (For two different strings, their lexical order is defined as the order of their elements in the leftmost position in which they differ.) Defining the string SA.i of length N by

(and SB. j similarly), we observe that (i) because of the periodicity of the function A , SA.i defines A completely, and (ii) the situation we were focussing - given by Pw A.(i + h) < B.(j + h) - implies in terms of the lexical order between strings

$$ \langle \forall k: 0 \leqslant k < h + 1: S A. (i + k) < S B. (j + k) \rangle $$

The nice thing about this conclusion about i and j is that it is still useful when simplified and weakened to a conclusion about i only, viz.

$$ \langle \forall k: 0 \leq k < h + 1: S A (i + k) < B B \rangle $$

where BB is the lexical maximum of

$$ B B = \langle \uparrow k: S B. k \rangle $$

Remark After the introduction of the lexical maxima, the function of the program to be designed can be described by the assignment statement

$$ e q := A A = B B $$

(End of Remark.)

Our last conclusion about $i$ suggests that we consider

[{0}^{2} + \frac{1}{2} \cdot {k}^{2} = 1 + {k}^{2}]

and observe

$\therefore Q$ 为 ${AE}$ 中点 $\because {OQ} ⫫ \frac{1}{2}{BE}$ (ii) the guarded command

$$ A. (i + h) < B. (j + h) \rightarrow i := i + h + 1 $$

maintains the truth of QA and

(iii) ${QA} \land N \leq i\; \land \left( {{eq} = f{a}^{l}\operatorname{se}}\right) \Rightarrow R$

[ad (ii). As given, the guarded command falsifies $P$ ,but the assignment $h : = 0$ remedies this.

ad(iii). From $QA \land N \leq i$ we can conclude $AA < BB$ , which implies $AA \neq BB$ .]

With QB analogously defined by

QB: $\left\langle {\forall k : 0 \leq k < j : {SB}.k < {HA}}\right\rangle \land 0 \leq j\;,\;$

merging our results now yields the program

$$ \begin{array}{l} l [ \mathrm {v a r} h, i, j: i n t \ ; h, i, j := 0, 0, 0 \left{\mathrm {i n v .} P \wedge Q A \wedge Q B \right} \ ; \underline {{d o}} h ^ {c} < N \land i < N \land j < N \rightarrow \ i f A. (i + h) = B. (j + h) \rightarrow h := h + 1 \ [ ] A. (i + h) < B. (\tilde {j} + h) \rightarrow i, h := i + h + 1, 0 \ [ B. (j + h) < A. (i + h) \rightarrow j, h := j + h + 1, 0 \ p _ {i} \ \mathrm {o d} \ ; e q := N \leq h \ ] ] \ \end{array} $$

This program terminates because the repeatable statement increases the value of $h + i + j$ each time by 1 while the guard of the repetition bounds this value from above. The form of the final assignment to eq is justified by the observation that after initiali-zation at most 1 of the conjuncts of the guard is false

Austin, 16 June 1998

prof. dr Edsger W.Dykstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188, USA