NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
On W.H.J. Feijen's solution for the lexicographic minimum of a circular list.
For a given, non-empty —i.e. with N ≥ 1— list (C[0], C[1], ..., C[N-1]) we consider the N associated sequences C_{i}
Ci = (C[i], C[i+1], ..., C[i+N-1]) |
R: | 0 ≤ k < N and (∀i: 0 ≤ i < N: C_{i} GE C_{k}) , |
* *
*
The lexicographic minimum CC is defined by the following two relations.
(∀i: 0 ≤ i < N: C_{i} GE CC) | (0) | |
(∃i: 0 ≤ i < N: C_{i} EQ CC) | (1) |
(∀p, q:: C_{p} GE C_{q} or C_{q} GT CC) | (3) |
* *
*
Let P(k,n) be defined as:
P: | 0 ≤ k < n and (∀i; 0 ≤ i < n: C_{i} GT CC or i = k) | (4) |
(P and n ≥ N) ⇒ R | (5) | |
(∀i: 0 ≤ i < h: C_{i} GT CC) ⇒ P(h, h+1) | (6) |
* *
*
Let Q(k, n, l) be defined as
Q: | 0 ≤ k < n ∧ (∀i: 0 ≤ i < l: C[k+i] = C[n+i]) | (7) |
Because the lexicographic order of the two sequences with equal leading elements does not change when those leading elements are removed from them, we conclude
Q(k,n,l) ⇒ (Q_{a} or Q_{b} or Q_{c}) | (8) |
Qa: | (∀i: 0 ≤ i < N: C_{k+i} = C_{n+i} | (8a) |
Qb: | (∀i: 0 ≤ i < l: C_{k+i} LT C_{n+i} ∧ l ≥ 0 | (8b) |
Qc: | (∀i: 0 ≤ i < N: C_{k+i} GT C_{n+i} ∧ l ≥ 0 | (8c) |
We furthermore observe that, for l=0, the last term of Q(k, n, l) is vacuously true.
* *
*
We observe that P&ans;Q can be initialized by
k, n, l:= 0, 1, 0 |
1) | C[k + l] = C[n + l] → l:= l + 1 |
This follows immediatly from (4) —l does not occur in P— and (7)
2) | C[k + l] < C[n + l] → {P∧Qb} n, l:= n + l + 1, 0 |
Q and the guard imply together Qb, and note that Qb implies
(∀i: n ≤ i < n+l+1: C_{I} GT CC) |
3) | C[k + l] > C[n + l] → {P∧Qc} n, l:= n + l + 1, 0 |
h:= max(n, k+l+1); | |
k, n, l:= h, h+1, 0 |
Q and the guard imply together Qc, and note that Qc implies
(∀i: k ≤ i < n+l+1: C_{i} GT CC) ∧ l ≥ 0 . |
(∀i: 0 ≤ i < h: C_{i} GT CC) |
* *
*
Finally we show that
(P ∧ Q ∧ k + l + 1 ≥ N) ⇒ R | (9) |
1) | P ∧ Qa ∧ k + l + 1 ≥ N |
From Qa we conclude that the sequence is periodic, and that the period divides n - k; hence
(∃i: k ≤ i < n: C_{i} EQ CC) |
(∀i: k < i < n: C_{i} GT CC) |
2) | P ∧ Qb ∧ k+l+1 ≥ N |
From Qb we conclude, as before,
(∀i: n ≤ i < n+l+1: C_{i} GT CC); |
(∀i: 0 ≤ i < N: C_{i} GT CC or i = k), i.e. R |
3) | P ∧ Qc ∧ k+l+1 ≥ N |
From Qc we conclude, as before,
(∀i: k ≤ i < k+l+1: C_{i} GT CC); |
(∀i: 0 ≤ i < N: C_{i} GT CC); |
(End of Proof of (9).)
Using (5) and (9), we see that the following program establishes R
k, n, l:= 0, 1, 0 | ||||
do n < N and k + l + 1 < N → | ||||
if C[k + l] = C[n + l] → l:= l + 1 {P ∧ Q} | ||||
▯ C[k + l] < C[n + l] → n, l:= n + l + 1, 0 {P ∧ Q} | ||||
▯ C[k + l] > C[n + l] → h:= max(n, k + l + 1); | ||||
k, n, l:= h, h + 1, 0 {P ∧ Q} | ||||
fi {P ∧ Q} | ||||
od {R} |
Termination. The function t = k + n + l increases by at least one at each iteration. Before the first iteration t = 1, before the last one t ≤ 2N - 3, hence 2N - 3 is an upper bound for the number of comparisons.
* *
*
The above is —or will be— described much more beautifully by W.H.J. Feyen, including all the heuristics and acknowledgements. I wrote the above as part of my personal correspondence, for the sake of quick dissemination: I owe everything of the above to ir. W.H.J. Feijen.
29th December 1979 | |
Plataanstraat 5 | |
5671 AL Nuenen | prof.dr.Edsger W.Dijkstra |
The Netherlands | Burroughs Research Fellow |
Transcribed by Martin P.M. van der Burgt
Last revision