Triggered by Higman’s Lemma

Triggered by Higman's Lemma

This EWD is devoted to a proof of Higman's Lemma, because we tried to prove the latter, but failed.

For finite strings of characters from an alphabet we define the length # and the subsequence relation $\equiv$ (in the style of SASL) by

$$ \begin{array}{l} # [ ] = 0 \ # (a: x) = 1 + # x \ [ ] \leq x = t r u e \ (a: x) \in [ ] = f a l s e \ (a: x) \leq (b: y) =\begin{array}{l}i p a = b \rightarrow x \leq y\\vdots a \neq b \rightarrow (a: x) \leq y\end{array}\quad\begin{array}{l}()\( *)\end{array} \ f _ {i} \ \end{array} $$

(It follows -though we shall neither use nor prove it here- that $\underline{\underline{\mathbf{E}}}$ is a partial order, i.e. reflexive, transitive, and antisymmetric.)

We now consider possibly infinite sequences of finite strings (or, if you prefer, functions of type: nat → string) and define on them the predicates "fight" and "bad":

$$ \begin{array}{l} t i g h t. s \equiv \langle \forall i, j: 0 \leq i \land i < j: (# s. i \leq # s. j) \land \neg (s. i \leq s. j) \rangle \ b a d. s \equiv t i g h t. s \wedge (s i s i n f i n i t e) \ \end{array} $$

Higman's Lemma states that there are no

bad sequences if the string characters are taken from a finite alphabet.

We shall prove the contrapositive, i.e. we shall show how the existence of bad sequences implies that the alphabet is infinite. This is done in 2 steps. In the first step we show the existence of a "minimal bad sequence" $t$ , i.e. a bad sequence $t$ such that

(0) $\langle \forall s : \text{bad.s} : \langle \forall k : \text{osk} : \text{s1k} = t1k \Rightarrow # s.k \geqslant t.k \rangle \rangle$ , in which ".1k" denotes the prefix of length $k$ . In the second step we show that each character of the alphabet is the leading character of at most a finite number of strings in $t$ ; hence, $t$ being an infinite sequence of strings, the alphabet is infinite.

The existence of a bad sequence t satisfying (0) is demonstrated by mathematical induction. Consider the induction hypothesis that tin satisfies

$\langle \forall s$ : bad.s: $\langle \forall k: 0 \leqslant k < n: s1k = t1k \Rightarrow # s.k \geqslant # t.k \rangle$

For $n = 0$ ,the first conjunct is vacuously true and the second conjunct reduces to $\langle \exists s : \operatorname{bad}.s\rangle$ , i.e. to the antecedent.

For the step from $n = N$ to $n = N + 1$ ,we leave ${tN}$ as it is,and define $t.N$ by $t.N = z.N$ ,where

${ba}{d}_{1}z \land {21N} = {t1N}\; \land \left\langle {\forall s : {ba}.s : {s1N} = {t1N} : # s.N \geq # z.N}\right\rangle$

The second conjunct of the hypothesis for $n = N$ ,viz. (3s: bad.s: sin=t1N> ensures the existence of at least one such $z$ ,the choice ensures the invariance of the induction hypothesis under $n = n + 1$ . (For the second conjunct, $s = z$ is a witness.) Hence there exists a t that satisfies the induction hypothesis for all n , and hence -from the first conjunct-satisfies (0). That t is a bad sequence follows from it being infinite and the second conjunct:

$$ \begin{array}{l} \langle \forall n:: \langle \exists s: b a d. s: s i n = + 1 n \rangle \rangle \ \Rightarrow \quad \begin{array}{l} {{\mathrm {t h e p r e f i x o f a b a d s e q u e n c e i s t i g h t} }} \ {\langle \forall n: \mathrm {t i g h t . (f i n)} \rangle} \end{array} \ = \left{ \begin{array}{l l} \mathrm {d e f . o f t h i g h t , o f 1 a n d p r e d i c a t e c a l c u l u s} \ \mathrm {t i g h t . t} \end{array} \right. \ \end{array} $$

And this completes the first step.

For the second step we consider a character b that occurs as first character of a string in t . Let u be the (non-empty) subsequence of t obtained by removing from t all strings whose first character differs from b . Our task is to show that u is finite.

We define $h$ to be the smallest value such

that t.h starts with a b ; then u.o = t.h . We define v as the sequence obtained from u by removing from each string in u the first character. We remark

[# {v}{0} = # {t}{h} - 1] - because u is a subsequence of t , it is tight, and therefore v is tight (on account of $(*)$ : all strings o u start with the same b , which is removed from all of them) - showing that $u$ is finite means showing

Let $m$ be the minimum value such that #t.m = #t.h . Because t is tight, $m \leq h$ . Define sequence $w$ as ${t1m}$ ,followed by $v$ . We observe

• ${t}_{1}m$ is high (subsequence of $t$ )
• v is fight (see above) because of the definition of $m$ ,all strings in tim have lengths less than #t.h,i.e. at most #v.o; in shorz

$$ 0 \leq i \wedge i < j \Rightarrow # w. i \leq # w. j $$

because $m \leq h$ ,also in the case

$0 \leq i < m \land m \leq j$ we have $7\left( {w,i \leq w,j}\right)$ , now on account of $\left( {x + }\right) : w.i$ is a t.i of the form a:x with a≠b,wi is of the form with b:y occurring higher up in t; in shor $0 \leq i \land i \leq j \Rightarrow 7\left( {w,i \leq w,j}\right)$

• combining the last two observations, we conclude that $w$ is tight.

showing that $v$ is finite means showing that

About we observe

• ${w}{1m} = {t}{1m}\;\left( {b{y}{\text{construction }}}\right)$ $# {w}{.m} < # {t}{.m}\;\left( {# {w}{.m} = # {v.0},# {v.0} = # + h - 1,# + h = # + m}\right)$

Confronting these two observations with (0), we conclude 2 bad. w ; because of tight. w , we conclude that $W$ is finite. QED

As confessed, we missed this proof. We tried to prove that a nondeterministic algorithm building a tight sequence would terminate and vainly searched for an ordering for which the well-foundedness could be shown in a familiar manner. It was probably that last constraint that did us in.

We did write down the formal definition of $\varepsilon$ and were very aware of the immediate consequences of $()$ and $( *)$ . Following an old habit, we built up a little theory about $\leq$ , viz. that $\varepsilon$ is a partial order, missing the hint that the relation occurring in "fight" is $\neq$ .

The central invention in the above proof is the minimal bad sequence t. Again, I blame myself for not having thought of it. The exploitation of an existential quantification in an antecedent for the construction of a special -usually in some sense extreme - witness is a well

known device, and I knew it. But I did not think of it. Perhaps we should invent a catchy name for it.

The decision, taken on EWDIII-1, to prove the contrapositive was not necessary: a weakening chain showing $P \Rightarrow Q$ can be translated (by syntactic transformation) into a strengthening chain showing $\neg P \Leftarrow \neg Q$ .

I am grateful to David Gries for having brought Higman's Lemma to my attention, and to the members of the ATAC, J.R.Rao in particular, for having discussed this problem with me.

Austin, 23 October 1991

Prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA