HOME

On W.H.J. Feijen's solution for the lexicographic minimum of a circular list

Show original manuscript

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 Ci

Ci = (C[i], C[i+1], ..., C[i+N-1])
in which all subscripts are reduced modulo N. We are asked to design a program determining an integer value k satisfying the relation
R: 0 ≤ k < N and (∀i: 0 ≤ i < N: Ci GE Ck) ,
in which "GE" should be read as "lexicographically greater or equal than".

*              *
*

The lexicographic minimum CC is defined by the following two relations.

(∀i: 0 ≤ i < N: Ci GE CC) (0)
(∃i: 0 ≤ i < N: Ci EQ CC) (1)
From the transitivity of the lexicographic ordering we conclude
(∀p, q:: Cp GE Cq or Cq GT CC) (3)
Note. When, in a quantification, the range is obvious, we allow ourselves its omission. Hence the "::". (End of note)

*              *
*

Let P(k,n) be defined as:

P: 0 ≤ k < n and (∀i; 0 ≤ i < n: Ci GT CC or i = k) (4)
We observe immediately
(P and n ≥ N) ⇒ R (5)
(∀i: 0 ≤ i < h: Ci 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) ⇒ (Qa or Qb or Qc) (8)
with the mutually exclusive terms
Qa: (∀i: 0 ≤ i < N: Ck+i = Cn+i (8a)
Qb: (∀i: 0 ≤ i < l: Ck+i LT Cn+i ∧ l ≥ 0 (8b)
Qc: (∀i: 0 ≤ i < N: Ck+i GT Cn+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
and is left invariant by the following three guarded commands.
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: CI GT CC)
Hence, on account of (4) the invariance of P is guaranteed. The assignment l:= 0 ensures the invariance of Q
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: Ci GT CC) ∧ l ≥ 0 .
With h = max(n, k+l+1) we conclude from the last result and P
(∀i: 0 ≤ i < h: Ci GT CC)
and, thanks to (6), the invariance of P is guaranteed. The assignment l:= 0 ensures the invariance of Q .

*              *
*

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: Ci EQ CC)
Together with —what follows from P—
(∀i: k < i < n: Ci GT CC)
we conclude Ck EQ CC, i.e. R .

2) P ∧ Qb ∧ k+l+1 ≥ N

From Qb we conclude, as before,

(∀i: n ≤ i < n+l+1: Ci GT CC);
because n > k, n+l+1 > k+l+1; because k+l+1 ≥ N we conclude, together with P
(∀i: 0 ≤ i < N: Ci 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: Ci GT CC);
because k+l+1 ≥ N, we conclude, together with P
(∀i: 0 ≤ i < N: Ci GT CC);
this together with (1) implies false, and false ⇒ R.

(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 2015-04-11 .