An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma
1 Mathematisches Institut der Universit¨at M¨unchen
2 Department of Computer Science, University of Wales Swansea†Abstract. Higman’s lemma has a very elegant, non-constructive proof due to Nash-Williams using the so-called minimal-bad-sequence argument. The objective of the present paper is to give a proof that uses the same combinatorial idea, but is constructive. For a two letter alpha- bet this was done by Coquand and Fridlender . Here we present a proof in a theory of inductive definitions that works for arbitrary de- cidable well quasiorders. Introduction
This paper is concerned with Higman’s lemma usually formulated interms of well quasi orders.
If (A, ≤A) is a well quasiorder, then so is the set A∗ of finite sequencesin A, together with the embeddability relation ≤A∗,
where a sequence [a1, . . . , an] is embeddable in [b1, . . . , bm] if there is a strictlyincreasing map f : {1, . . . , n} → {1, . . . , m} such that ai ≤A bf(i) for all i ∈
Among the first proofs of Higman’s lemma which all were non-constructive
the proof of Nash-Williams using the so-called minimal-bad-sequence argumentis considered most elegant. A variant of this proof was translated by Murthy viaFriedman’s A-translation into a constructive proof however resulting ina huge proof whose computational content couldn’t yet be discovered. More di-rect constructive proofs were given by Sch¨
dinal notations up to 0 and is related to an earlier proof by Schmidt theother proofs are carried out in a (proof theoretically stronger) theory of induc-tive definitions. However, their computational content is essentially the same,but does not correspond to that one of Nash-Williams’ proof. (The proof the-oretic strength of the general minimal-bad-sequence argument is Π1−CA
Research supported by the DFG Graduiertenkolleg “Logik in der Informatik”. † Research supported by the British EPSRC.
P. Callaghan et al. (Eds.): TYPES 2000, LNCS 2277, pp. 2002.
was shown by Marcone, however it is open whether the special form used forHigman’s lemma has the same strength .)
The objective of this paper is to present a constructive proof that captures
the combinatorial idea behind Nash-Williams’ proof. For an alphabet A con-sisting of two letters this was done by Coquand and Fridlender Theirproof can quite easily be extended to a finite alphabet. To obtain a proof forarbitrary decidable well quasiorders, more effort is necessary, as we will describein section
A proof of Higman’s lemma which in contrast to all proofs mentioned above
does not require decidability of the given relation ≤A was given by Fridlender. His proof is based on a proof by Veldman that can be found in . In our formulation of Higman’s lemma we will also use an accessibility notion,as it was done in Fridlender’s proof. Basic Definitions and an Inductive Characterization of Well Quasiorders
In the whole paper we assume (A, ≤A) to be a set with a reflexive and transitive,decidable relatio
Definition 1. We use a, b, . . . for letters, i.e., elements of a A,as, bs, . . . for finite sequences of letters, i.e. elements of A∗,v, w, . . . for words, i.e., elements of A∗, 2
vs, ws, . . . for finite sequences of words, i.e., elements of A∗∗ .
By as∗a we denote the sequence obtained from the sequence as by appending theelement a. ws∗w is defined similarly. At some places we add brackets to keep theexpressions legible. However, unary function application will be written withoutbrackets, in general.
For a finite sequence ws of non-empty words let lasts ws denote the finite
sequence consisting of the end-letters of the words of ws, that is
lasts [w1∗a1, . . . , wn∗an] = [a1, . . . , an], n ≥ 0.
1 Whereas transitivity is only required for historical reasons, but is not used in our
proof, decidability plays an essential role. w1 w2 w3 w4 w5
Although of the same kind we distinguish be-tween finite sequences (of letters) and words,because they will play different rolls, as is il-lustrated in the picture on the right.
3 In our picture we have lasts [w1, . . . , w5] = as.
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
Definition 2 (Higman Embedding). The embedding relation on A∗ can be inductively described by the following rules: Definition 3 (Good/Bad). A finite sequence [a1, . . . , an] (respectively an in- finite sequence a1, a2, . . .) of elements in A is good if there exist i < j ≤ n (i < j < ω) such that ai ≤A aj; otherwise it is called bad.
Furthermore, we use the notion good(as, a) if there is an element in as, say
the i-th one, such that (as)i ≤A a. bad(as, a) stands for ¬good(as, a).
Finally, badsubseq(as) determines the first occurring bad subsequence in as:
badsubseq(as)∗a if bad(badsubseq(as), a),Definition 4 (Well Quasiorder). (A, ≤A) is a well quasiorder (wqo) if every infinite sequence of elements in A is good. Definition 5 (The Relation A and Its Accessible Part). The relation bs A as :↔ bs = as∗a for some a ∈ A s.t. bad(as, a).
The accessible part (also called the well-founded part) of the relation
and provides the following induction prfor any formula φ:
∀as. ∀bs A as φ(bs) → φ(as).Definition 6 (Well Quasiorder, Inductive Characterizati). (A, ≤A) is a well quasiorder if acc
4 At some places we use a seemingly stronger induction principle where the premise
A as φ(bs) → φ(as). This principle can be easily
Definitions to should be understood for arbitrary (reflexive and transitive)
relations, not only for our fixed (A, ≤A). We will use them also for (A∗, ≤A∗). Moreover, the operation acc will also be applied to the relations
Towards a Constructive Proof
In order to motivate further definitions we first want to give the idea behindthe constructive proof. This is best done by showing the connection between theclassical and the constructive proof. To this end we shortly recall Nash-Williams’minimal-bad-sequence proof and show how the main steps are captured by theinductive proof. We also include an informal idea of the latter. The steps of the Nash-Williams’ proof:
1. In order to show “wqo(A) implies wqo(A∗)”, assume for contraction that
2. Among all infinite bad sequences we choose (using classical dependent choice)
a minimal bad sequence, i.e., a sequence, say (wi)i<ω, which is minimal withrespect to a lexicographical order on infinite sequences of words (where w1is less or equal w2, if w1 is an initial segment of w2).
3. Since wi = [ ], let wi = vi∗ai for all i. Using Ramsey’s theorem and the
fact that our alphabet A is a well quasiorder, we know that there exists aninfinite subsequence aκ ≤A · · · of the sequence (ai)i<ω. This also
determines a corresponding sequence w1, . . . , wκ
4. The sequence w1, . . . , wκ, v , . . .. must be bad (otherwise (w
would be good), but this contradicts the minimality in 2. In the constructive proof this steps correspond to
2. The minimality argument will be replaced by structural induction on words. 3. Given a bad sequence ws = [w1, . . . , wn] s.t. wi = vi∗ai, we are interested
sponding sequences w1, . . . , wκ, . . . , v . In the proof these sequences
will be computed by the procedure forest which takes ws as input and yieldsa forest labeled by pairs in A∗∗ × A. In the produced forest the right-handcomponents of each path form a weakly ascending subsequence of [a1, . . . , an]
5 In our paper we only deal with this second definition of a well quasiorder since it is
very suitable for a constructive proof. For sake of completeness we give an argumentfor the equivalence of definition and definition To prove that definition impliesdefinition one shows more generally that for all as such that acc
infinite sequence, starting with as, is good. The reverse direction is an instance ofBrouwer’s axiom of bar induction.
6 By maximal length we mean that we only look at those subsequences which are
ascending, but not contained in other ones, for instance our chosen subsequences of[1, 4, 3, 0, 3] are [1, 4], [1, 3, 3] and [0, 3].
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
and the corresponding sequence of form w1, . . . , wκ
read off in the left-hand component of the endnode of such a path. If weextend the sequence ws badly by a word v∗a, then in the existing foresteither new nodes, possibly at several places, are inserted, or a new singletontree with node ws∗v, a is added. Now the informal idea of the inductiveproof is: if in forest ws not infinitely often new nodes could be inserted andif also not infinitely often new trees could be added, then ws could not beextended badly infinitely often. Formally this will be captured by the state-ment: ∀ws. acc
badsubseq(lasts ws) → acc
≺ forest ws → acc A∗ ws
4. The first part of item 4 corresponds to lemma
We proceed with the formal definition of forest and the relation ≺ on forests. Definition 7. We use
for elements in T (A∗∗ × A), i.e., trees labeled by pairs in A∗∗ × A,f, ts for elements in (T (A∗∗ × A))∗, i.e., forests.
The tree with root ws, a and finite sequence of immediate subtrees ts is written
ws, a ts. We use the destructors left and right for pairs and the destructors root
and subtrees for trees, hence root ws, a ts = ws, a and subtrees ws, a ts = ts. For better readability we set:
:= [root t1, . . . , root tn],
lefts [ vs1, a1 , . . . , vsn, an ] := [vs1, . . . , vsn],rights [ vs1, a1 , . . . , vsn, an ] := [a1, . . . , an].Definition 8. Let ws ∈ A∗∗ be a sequence of non-empty words. Then forest ws ∈ T ((A∗∗ × A))∗ is defined recursively by:
if good(badsubseq(lasts ws), a)
(forest ws) ∗ newtree ws∗w, a otherwise,
7 For sake of simplicity we define insertforest by a map operation, i.e., we insert a new
node at every possible place. However, it would already suffice to insert at least onceand it even could be arbitrarily chosen where to insert.
8 In case of a finite alphabet forest ws has only non-branching trees where the right-
hand components of such a tree are constant. So, if in the notion of wehave T0(vs, ws) or R0(vs, ws), in our setting the sequence vs could be read off as theleft-hand component in the endnode of the tree whose right-hand components are 0.
insertforest(f, w, a) = map λt
inserttree(t, w, a) fvs, a insertforest(ts, w, a)
if good(rights (roots ts), a),vs, a (ts ∗ newtree vs∗w, a ) otherwise. Definition 9. Let f and f be forests in T ((A∗∗ × A))∗. Then
f = insertforest(f, w, a) for some w ∈ A∗, a ∈ Af ≺ f :↔ such that f = f and the left-hand component of
each label in f is a bad sequence in A∗∗.Lemma 1. Let ws be a bad sequence of non-empty words. Then in every label of forest ws the left-hand component is a bad sequence. Proof. IND(structure of ws). 1. ws = [ ]. Clear.
2. Assume that every left-hand component of a label in forest ws is bad and
look at the nodes in forest ws∗(w∗a) where ws∗(w∗a) is assumed to be bad.
Case 1: bad(badsubseq(lasts ws), a). Then in forest ws∗(w∗a) only one node
was added, i.e., the node with label ws∗w, a where by assumption ws∗w isbad.
Case 2: good(badsubseq(lasts ws), a). In this cassome nodes of the form
vs∗w, a were inserted in forest ws where vs is a left-hand component of a node in
forest ws which by assumption is bad. Assume good(vs, w), that is, ∃i(vs)i ≤A∗ wand show ⊥.
Case 2.1: (vs)i is a word in ws. Then, by the Higman embedding we obtain
(vs)i ≤A∗ w∗a – contradicting the badness of ws∗(w∗a).
Case 2.2: (vs)i is a word in ws cut by an end letter a0 and by the construction
of the forests it holds a0 ≤A aThen, again by the Higman embedding it follows(vs)i∗a0 ≤A∗ w∗a. Contradiction. Lemma 2. i) acc≺ []. ii) acc≺ f ∧ acc≺ [t] → acc≺ f ∗ t. Proof. i) acc≺ [] holds by definition, since there is no tree in which new nodescould be inserted. ii) Clear, since insertforest is defined by a map-operation.
9 Here, we only sketch the combinatorial part of the proof; a formal proof involves an
10 Note that transitivity is not required.
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
Lemma 3. Assume acc A∗ ws → ∀a. acc≺ [newtree ws, a ].Proof. IND1(acc A∗ ): IH1 : ∀vsA∗ ws, ∀a. acc≺ [newtree vs, a ]. Let a ∈ A. In-
stead of proving acc≺ [newtree ws, a ] we show more generally that this assertionholds for all t with root t = ws, a such that
(a) the subtrees of t form a forest in acc≺ and(b) rights (roots (subtrees t)) is sequence in acc
We do this by main induction on (b) and side induction on (a), i.e., formally
∀t. root t = (ws, a) ∧ subtrees t = ts ∧ as = rights (roots (subtrees t)) →
). Assume that we have an as such that acc
IND3(acc≺ ). Let ts be such that acc≺ ts and fix t such that root t = ws, a ,
subtrees t = ts, and as = rights (roots (subtrees t)).
We have to prove acc≺ [t]. By the definition of acc≺ and ≺ if suffices to show
∀t . [t ] ≺ [t] → acc≺ [t ] where t = inserttree(t, w, a ) = t for some w ∈ A∗, a ∈ Aand all left-hand components of nodes in t are required to be bad. We prove theassertion by case distinction on the definition of inserttree.
Case 1: t = ws, a (ts ∗ newtree ws∗w, a ) for some w and a such that
subtrees t = ts ∗ newtree ws∗w, a ,as∗a
= rights (roots (ts ∗ newtree ws∗w, a )).
Since all left-hand components in t are supposed to be bad, in particular, we havethat ws∗w is bad, i.e., ws∗wA∗ ws. By IH1 we obtain acc≺ [newtree ws∗w, a ],
acc≺ ts ∗ newtree ws∗w, a .A as, we may apply IH2 to as∗a , ts ∗ newtree ws∗w, a
and conclude acc≺ [t ].
Case 2: t = ws, a insertforest(ts, w, a ) where a such that good(as, a ). In
subtrees t = insertforest(ts, w, a ),as
= rights (roots (subtrees t )).
11 It’s intended that [t] lies in the image of the partial function forest, however we
don’t need this restriction in the formulation of the lemma.
Moreover [t ] ≺ [t] implies subtrees t ≺ subtrees t = ts, and by IH3, applied tosubtrees t and t , we end up with acc≺ [t ].
Now, the proof of the general assertion is completed, and we may put as = [ ],
f = [] and t = newtree ws, a . Since we have acc
by lemma we obtain acc A∗ ws → acc≺ [newtree ws, a ]. The Proof of Higman’s Lemma Proposition 1 (Higman’s Lemma). acc ∀ws. as = badsubseq(lasts ws) ∧ f = forest ws → acc A∗ ws.∀ws. bs = badsubseq(lasts ws) ∧ f = forest ws → acc A∗ ws.
IND2(acc≺ ). Let f be s.t acc≺ f and IH2 : ∀f ≺ f, ∀ws. badsubseq(lasts ws) =
as ∧ f = forest ws → acc A∗ ws and assume that we have ws such that as =badsubseq(lasts ws) and f = forest ws. In order to prove acc A∗ ws we fix w s.t. ws∗w is bad and show acc A∗ ws∗w by induction on the structure of w:
IND3(w). 1. acc A∗ ws[] holds by definition of acc A∗ . 2. Now, assume that we have a word of form w∗a. We show acc A∗ ws∗(w∗a)
by case analysis on whether or not bad(as, a).
Case 2.1: bad(as, a). Then we have
= badsubseq(lasts (ws∗(w∗a))),f ∗ newtree ws∗w, a = forest (ws∗(w∗a)).
First, we show acc≺ f ∗ newtree ws∗w, a . By assumption we already have acc≺ fand by IH3 acc A∗ ws∗w. Hence, by lemma we obtain acc≺ [newtree ws∗w, a ]and by lemma we may conclude
acc≺ f ∗ newtree ws∗w, a .
Now we are able to apply IH1 (to as∗a, f ∗ newtree ws∗w, a and ws∗(w∗a)) andend up with acc A∗ ws∗(w∗a).
Case 2.2: good(as, a). In this case it follows
= badsubseq(lasts (ws∗(w∗a))),
insertforest(f, w, a) = forest (ws∗(w∗a)).
By lemma all left-hand components of nodes in insertforest(f, w, a) are bad. Moreover, insertforest(f, w, a) = f since good(as, a) and badsubseq(lasts ws) =
as = rights (roots (forest ws)) imply that indeed at least one node was inserted. Hence, we obtain
insertforest(f, w, a) ≺ f
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
and we may apply IH2 (to insertforest(f, w, a) and ws∗(w∗a)) and concludeacc A∗ ws∗(w∗a).
This completes the proof of the general assertion. Now, by putting as =
[ ], f = [ ] and ws = [ ] and the fact that acc≺ [] holds by definition we obtainacc
Conclusion
We presented a new constructive proof of Higman’s lemma for arbitrary decid-able well quasiorders in a theory of inductive definitions. We hope not only thatthis proof gives more insight in the interplay of classical proofs using a minimalbad sequence argument and constructive proofs, but also that this strategy is ex-tendible to other non-constructive theorems, for instance Kruskal’s tree theoremand the so-called extended Kruskal theorem, also known as Kruskal’s theoremwith gap condition. Both have proofs using a minimal-bad-sequence argument(see resp. ), however no constructive proof at all is known forthe latter. Kruskal’s theorem was proved constructively (see for a proofusing ordinal notations or for an inductive reformulation of this proof,and for a proof not requiring decidability). These proofs, however, arequite involved in comparison with the minimal-bad-sequence proof.
We do not claim that our proof of Higman’s lemma is ‘better’ than the other
constructive proofs mentioned in the introduction, but, as already stated, it usesa different combinatorial idea, hence results in another algorithm. An analysisof these different algorithms is still missing and could give rise to an interestingcase study in machine supported theorem proving. Acknowledgment
I am grateful to Ulrich Berger, Thierry Coquand, and the referees for theirhelpful comments and suggestions on this article, and particularly I would liketo thank Daniel Fridlender for valuable discussions during his Munich visit inJune 2000. The idea to use a tree structure is due to him. References
Thierry Coquand and Daniel Fridlender. A proof of Higman’s lemma by struc-tural induction, 1994.
Daniel Fridlender. Higman’s Lemma in Type Theory. PhD thesis, ChalmersUniversity of Technology and University of G¨
Hig52. Graham Higman. Ordering by divisibility in abstract algebras. Proc. LondonMath. Soc., 2:326–336, 1952.
Mar96. Alberto Marcone. On the logical strength of Nash-Williams’ theorem on trans-
finite sequences. In: Logic: from Foundations to Applications; European logiccolloquium, pp. 327–351, 1996.
MR90. Chetan R. Murthy and James R. Russell. A Constructive proof of Higman’s
Lemma. In Proc. Fifth Symp. on Logic in Comp. Science, pp. 257–267, 1990.
Mur91. Chetan R. Murthy. An Evaluation Semantics for Classical Proofs. In Proc.
Sixth Symp. on Logic in Computer Science, pp. 96–109, 1991.
NW63. Crispin St. J. A. Nash-Williams. On well-quasi-ordering finite trees. Proc.Cambridge Phil. Soc., 59:833–835, 1963.
RW93. Michael Rathjen and Andreas Weiermann. Proof–theoretic investigations on
Kruskal’s theorem. Annals of Pure and Applied Logic, 60:49–88, 1993.
Fred Richman and Gabriel Stolzenberg. Well Quasi–Ordered Sets. Advancesin Math., 97:145–153, 1993.
Monika Seisenberger. Kruskal’s tree theorem in a constructive theory of induc-tive definitions In: Reuniting the Antipodes -Constructive and NonstandardViews of the Continuum. Synthese Library, Kluwer, Dordrecht, forthcoming.
utte and Stephen G. Simpson. Ein in der reinen Zahlentheorie un-
Mathematische Logik und Grundlagenforschung, 25:75–89, 1985.
Sim85. Stephen G. Simpson. Nonprovability of certain combinatorial properties of
finite trees. In L.A. Harrington, et al., eds., Harvey Friedman’s Research on theFoundations of Mathematics, pp. 87–117. North–Holland, Amsterdam, 1985.
Sch79. Diana Schmidt. Well-orderings and their maximal order types, 1979. Habili-
tationsschrift, Mathematisches Institut der Universit¨
Wim Veldman. An intuitionistic proof of Kruskal’s Theorem. Report no. 0017,Department of Mathematics, University of Nijmegen, 2000.
IATA Dangerous Goods Regulations ADDENDUM II Users of the IATA Dangerous Goods Regulations are asked to note the following amendments and corrections to the 54th Edition, effective from 1 January 2013. Where appropriate, changes or amendments to existing text have been highlighted (in yellow - PDF or grey - hardcopy) to help identify the change or amendment. New or Amended Operator Vari
Leila Dargahi Personal Information Date of Birth: 10/31/1979 Place of Birth: Tehran Nationality: Iranian Marital status: Single Address for correspondence Neuroscience Research Center Shahid Beheshti University of Medical Sciences Tehran, Iran Tel: ( +98-21) 22 42 97 68 Fax: ( +98-21) 22 43 20 47 Mobile: ( +98-912) 506 99 30 e-mai Educ
An Inductive Version of Nash-Williams’
was shown by Marcone, however it is open whether the special form used forHigman’s lemma has the same strength .)
The objective of this paper is to present a constructive proof that captures
the combinatorial idea behind Nash-Williams’ proof. For an alphabet A con-sisting of two letters this was done by Coquand and Fridlender Theirproof can quite easily be extended to a finite alphabet. To obtain a proof forarbitrary decidable well quasiorders, more effort is necessary, as we will describein section
A proof of Higman’s lemma which in contrast to all proofs mentioned above
does not require decidability of the given relation ≤A was given by Fridlender. His proof is based on a proof by Veldman that can be found in .
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
Definition 2 (Higman Embedding). The embedding relation on A∗ can be
Definitions to should be understood for arbitrary (reflexive and transitive)
relations, not only for our fixed (A, ≤A). We will use them also for (A∗, ≤A∗).
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
and the corresponding sequence of form w1, . . . , wκ
read off in the left-hand component of the endnode of such a path. If weextend the sequence ws badly by a word v∗a, then in the existing foresteither new nodes, possibly at several places, are inserted, or a new singletontree with node ws∗v, a is added. Now the informal idea of the inductiveproof is: if in forest ws not infinitely often new nodes could be inserted andif also not infinitely often new trees could be added, then ws could not beextended badly infinitely often. Formally this will be captured by the state-ment: ∀ws. acc
badsubseq(lasts ws) → acc
≺ forest ws → acc A∗ ws
4. The first part of item 4 corresponds to lemma
We proceed with the formal definition of forest and the relation ≺ on forests.
insertforest(f, w, a) = map λt
inserttree(t, w, a) f
vs, a insertforest(ts, w, a)
if good(rights (roots ts), a),
vs, a (ts ∗ newtree vs∗w, a ) otherwise.
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
Lemma 3. Assume acc