The majority vote according to J. Gutknecht

The majority vote according to J. Guthnecht

I recently received from J. Gutknecht (ETH, Zürich) a nice solution to the problem known as "the majority vote", and one of the purposes of this note is just to record it. Its other purpose is to give a formal derivation of it, so that we can see the essence of Gutknecht's invention. Let me quote Gutknecht's statement of the problem:

"Let every inhabitant of a (non-empty) democracy be eligible as president. Let $b(i: o s i < M)$ be a series of ballots. Develop a program that eliminates all but one candidate $x$ , where no candidate eliminated has a majority of votes."

The formal statement of the postcondition to be satisfied by $x$ is

R: $\;\left( {\underline{A}y;y \neq x;\left( {\underline{N}i : 0 \leq i \land i < M}\right. }\right) \left( {b.i = y}\right) * 2 \leq M)$

(Note that it is not required that x has a majority of votes: if none of the candidates has a majority of votes, any value for $x$ satisfies R.)

An obvious candidate for the invariant is

${P}{0} : \;\left( {{A}{y} : y \neq x : \left( {{N}{i} : {0 \leq i \land i} < m : {b}{i} = y}\right) * 2 \leq m}\right)$

since it can be established $m \coloneqq 0$ and $\left\lbrack {m = M \land {P}{0} \Rightarrow R}\right\rbrack$ (by construction of ${P}{0}$ )

What about its invariance under $m \mathrel{\text{:=}} m + 1$ ?

$$ w p. " m := m + 1". P o $$

$$ = {\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 _ {0} } $$

$$ (\underline {{A}} y: y \neq x: (\underline {{N}} i: 0 \leq i \land i < m + 1: y = b. i) * 2 \leq m + 1) $$

$$ \Leftrightarrow {\mathrm {p r o p e r t i e s o f} \underline {{N}}, \mathrm {d e f i n i t i o n o f} P _ {0} } $$

$$ P O \sim (\mathrm {A y}: y \neq x: y \neq b. m) $$

$$ = {t r a d i n g t o (\underline {{A}} y: y = b. m: y = x); \mathrm {o n e - p o i n t r u l e} } $$

$$ P O \wedge x = b. m, $$

which leaves the $x \neq b.m$ to be investigated.

Gutknecht's first invention is the introduction of a variable, s say, which records an upper bound on the number of "seen" votes for any currently eliminated candidate, i.e.

${P}{1} : \;\left( {{A}{y} : y \neq x : \left( {{N}_{i} : {0.5i} \land i < m : y = b.i}\right) \leq s}\right)$

By a calculation very similar to the above, we can establish

$$ [ P _ {1} \wedge x = b. m \Rightarrow w p. ^ {\prime \prime} m := m + 1 ^ {\prime \prime}, P _ {1} ] $$

Since currently eliminated candidates don't have a majority of the votes "seen", we can maintain -and this Gutknecht's second invention- $2 * s \leq m$ or

P2: $s \leq m - s\;$ ,established by $m,s = 0,0\;$ .

${P}_{2}$ is trivially invariant under $m = m + 1$ .

We can now forget about the invariance of ${P}{0}$ because $\left\lbrack {{P}{1} \land {P}{2} \Rightarrow {P}{0}}\right\rbrack$ .

Note We could have derived $P2$ as the weakest solution of $P2: [P1 \land P2 \Rightarrow P0]$ ; then Gutknecht's second invention would have been to replace $P0$ by the conjunction of $P1 \land P2$ . (End of Note.)

Now we return to the investigation how to increase $m$ by 1 under invariance of $P_1 \wedge P_2$ . In the case $x \neq b.m$ . Because - for any $B$

$$ (\underline {{N}} _ {i}: 0 \leq i \land i < m + 1: B _ {i}) \leq (\underline {{N}} _ {i}: 0 \leq i \land i < m: B _ {i}) + 1 $$

$m,s = m + 1,s + 1$ maintains invariant ${P}_{1}$ . For the other conjunct of the invariant we investigate

$$ \begin{array}{l} w p. " m, s := m + 1, s + 1". P _ {2} \ = {\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 _ {2} } \ s + 1 \leq m + 1 - (s + 1) \ = {\mathrm {a r i t h m e t i c} } \ s < m - s \ \end{array} $$

So we can deal with the case $x \neq b.m \land s < m - s$ ;

the only case left is $x \neq b.m \land s = m - s\;$ . Here,

Gutknecht remarked that there is no assign.

ment to x yet, and his third invention is to

consider for this case

Since this assignment obviously maintains $P 2$ ,

we investigate the invariance of ${P}_{1}$

$$ w p. " m, x := m + 1, b. m". P _ {1} $$

$= {$ axiom of assignment, definition of ${P}_{1}}$

$\left( {\underline{a}y : y \neq b.m}\right) .\left( {\underline{N}i : 0 \leq i \land i < m + 1 : y = b.i}\right) \leq s)$

$= {$ properties of $N}$

$\left( {\underline{A}y,y \neq {b.m}\text{;}(\underline{N}i : 0 \leq i \land i < m : y = b.i)\;s}\right)$

$\Leftrightarrow {$ because $x \neq b.m$ ,the second conjunct is

needed ; one-point rule?

${P}_{1} \land \left( {\underline{N}i : 0 \leq i \land i < m : x = b,i}\right) \leq s$

$= \left{ {{exploitation} \mid s = m - s}\right}$

${P}{1} \land \;\left( {{N}{i} : 0 \leq i \land i < m : x = {b}_{i}}\right) \leq m - s$

And, finally, comes Gutknecht's optimism! Let us investigate whether we are lucky and $P_{3}$ , given by

${P}{3}\;\left( {{N}{i} : 0 \leq i \land i < m : x = {b}_{i}}\right) \leq m - s$

is an invariant. It is established by the initializa- tion $m,s = 0,0$ . We investigate our three cases.

$$ \begin{array}{l} x = b. m \rightarrow m := m + 1 \ w p. " m := m + 1". P _ {3} \ {a x i o m o f a s s i g n m e n t, d e f i n i t i o n o f P _ {3} } \ (N i: 0 \leq i \land i < m + 1: x = b. i) \leq m + 1 - s \ = {x = b. m } \ (N i: 0 \leq i \land i < m: x = b. i) + 1 \leq m + 1 - s \ = {\mathrm {a r i t h m e l i c}; \mathrm {d e f i n i t i o n o f} P _ {3} } \ P _ {3} \ \end{array} $$

$$ \begin{array}{l} x \neq b. m \wedge s < m - s \rightarrow m, s := m + 1, s + 1 \ w p. " m, s := m + 1, s + 1". P _ {3} \ = {\mathrm {a x i o m o f a s s i g n m e n t , d e f i n i t i o n o f} P _ {3} } \ (\mathrm {N i}: 0 \leq i \land i < m + 1: x = b. i) \leq (m + 1) - (s + 1) \ \end{array} $$

$$ \begin{array}{l} = {x \neq b. m; a r i t h m e t i c } \ (N _ {i}: 0 \leq i \land i < m: x = b. i) \leq m - s \ = {\mathrm {d e f i n i t i o n} p _ {3} } \ p _ {3} \quad . \ \end{array} $$

$$ \begin{array}{l} = {x \neq b. m; a r i t h m e t i c } \ (N _ {i}: 0 \leq i \land i < m: x = b. i) \leq m - s \ = {\mathrm {d e f i n i t i o n} p _ {3} } \ p _ {3} \quad . \ x \neq b. m \wedge s = m - s \rightarrow m, x := m + 1, b. m \ w p. " m, x := m + 1, b. m", P _ {3} \ = {\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 3 } \ (N i: 0 \leq i \land i < m + 1: b. m = b. i) \leq m + 1 - s \ = {\text {p r o p e r t i e s} \circledast \underline {{\mathbf {N}}}, \text {a r i t h m e t i c} } \ (\underline {{N}} i: 0 \leq i \land i < m: b. m = b. i) \leq m - s \ = {s = m - s } \ (\underline {{N}} i: 0 \leq i \land i < m: b. m = b. i) \leq s \ \Leftrightarrow {\mathrm {I n s t a n t i a t i o n w i t h} y := b. m; b. m \neq x } \ p _ {1} \ \end{array} $$

Thus the invariance of $P_{1} \wedge P_{2} \wedge P_{3}$ has been established, and we have derived the program

$$ \begin{array}{l} \mathrm {I l} \underline {{v a r}} m, s: \mathrm {i n t}; x, m, s := \mathrm {a n y}, 0, 0 \ ; \underline {{d o}} m \neq M \rightarrow \ i f x = b, m \rightarrow m := m + 1 \ [ ] x \neq b. m \rightarrow \ i f s < m - s \rightarrow m, s := m + 1, s + 1 \ [ S = m - s \rightarrow m, x := m + 1, b. m \ f _ {i} \ \end{array} $$

$$ i $$

$$ 3 1 \frac {o d}{d} $$

in which derivation I forgot -as usual!. - to include

$0 \leq m \leq M$ in the invariant; similarly, the proof

The above derivation more than confirms my rule of thumb that the derivation of a non-trivial program is at least 10 times as long as the raw code in which it culminates; my formal manipulations and the identification of Guthnacht's inventions fully confirms that the majority vote algorithm - originally due to Boyer & Moore, be it in a different coding-is not trivial. So does the piece of luck that P3 is invariant. (In his letter to me, Guthnacht adorned his program with 3 lines of problem statement and 5 lines of explanation, which by my standards, is a bit meagre. Hence this note.)

My indebtedness to Gutknecht is obvious.

Austin, Wednesday 25 January 1989

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