1197

A termination argument

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

A termination argument

Consider a cyclic arrangement of a set of integer variables. Any pair $x, y$ of these variables such that $x$ is the clockwise neighbour of $y$ enables a "move" if $x < y$ : the move then consists of adding 1 to $x$ and subtracting 1 from $y$ , i.e. in guarded command notation

$x < y \rightarrow x,y \mathrel{\text{:=}} x + 1,y - 1\;$

We leave for the reader to prove

(1) (no move is possible) (all variables have the same value).

A game consists of an initialization of the variables, followed by a sequence of moves until no move is possible. Since a move leaves the number of variables and also the sum of their values unchanged, we conclude

(2) in a game, the average of the values is constant.

(In passing we note that if this average is not an integer, the game therefore fails to terminate.)

A slightly more sophisticated theorem is

(3) an enabled move sooner or later takes place.

Proof Consider an enabled move, i.e. a pair $x,y$ such that $x < y$ . Rearrange the variables in a string, starting with $x$ and ending with $y$ , by "cutting". The cycle between $x$ and $y$ , and then "straightening" it. The other moves then correspond to the pairs that are neighbours in the string. Of those moves now observe

(i) that -since each of them moves the centre of gravity of the values over a fixed amount towards $y$ - only a finite number of them can take place before (the values form an ascending sequence and) no more of them are possible, and (ii) that none of them falsifies $x < y$ . Hence the occurrence of an enabled move is not be postponed indefinitely. (End of Proof.)

Looking for (a component of) a variant function, there is no point in looking at the sum of the values, since that sum is constant. However, the sum $S$ of the squares of the values -obviously bounded from below-might be of inter-

est. We observe for the change ${\Delta S}$ of $S$ under move (0)

$$ \begin{array}{l} \Delta S \ = \left{ \begin{array}{l l} \mathrm {d e f . o f} S & \mathrm {a n d o f m o v e (0)} \ (x + 1) ^ {2} + (y - 1) ^ {2} & - (x ^ {2} + y ^ {2}) \end{array} \right. \ = \begin{array}{l} {{\mathrm {a l g e b r a} }} \ {2 \cdot (x + 1 - y)} \end{array} \ \end{array} $$

that is, there are two kinds of moves:

$$ (4) \quad x + 1 < y \rightarrow x, y := x + 1, y - 1 $$

under which ${S}^{\prime }$ is decreased by at least 2 , and -after simplification-

$$ (5) \quad x + 1 = y \rightarrow x, y := y, x $$

under which s remains constant: for

For the rest of this note, we confine our attention to games such that after initialization the average of the values of the variables is integer; from (2) we conclude that this then holds all through the game. For such a game we can assert

(6) if a move is possible, maximum and minimum differ by at least 2 .

Proof If a move is possible - see (1) not all values are equal, i.e. the maximum exceeds the average, which exceeds the minimum. All three being integer, the maximum exceeds the minimum by at least 2. (End of Proof.)

From (6) we conclude

(7) if a move is possible, sooner or later

Proof For any two distinct variables $p$ and $q$ we define as "the separators" the variables situated on the cycle between $p$ and $q$ on the clockwise path from $p$ to $q$ . Thanks to (6) we can choose $p$ and $q$ such that

$\left( i\right) \;p - q \geq 2$ (ii) for any separator $s$ .. $p > s\wedge s > q$ We observe that (i) and (ii) are main-. tained by moves among the variables on the counter-clockwise path from p to q (p may grow and q may shrink, but that is okay), and also by moves on pairs s,s of separators.

If there are separators, the moves on $s,p$ and on $q,s$ are enabled because of (ii); because of (3), sooner or

later, one of them occurs. If it is of type (4), S is decreased. If it is of type (5), we reduce the number of separators by 1 and restore (i) and (ii) by moving p (clockwise) or q (counterclockwise) over 1 position.

Finally, if there are no separators left, the move on the pair $q,p$ is enabled; because of (i), this move is of type (4) and because of (3), sooner or later it will decrease

And thus we have established that if the average value is integer, the game terminates (and such was our goal).

The above has been written in reaction to a paper I had been asked to reference.

Austin, 23 Januari 1995

profi. dr. Edsger W. Dgksha Department of Computer Sciences The University of Texas at Austin, AustinTX 78712-1188 USA