Fact-checked by Grok 2 weeks ago

Well-quasi-ordering

In mathematical order theory, a well-quasi-ordering (also denoted wqo) on a set X is a quasi-ordering—a binary relation \leq on X that is reflexive and transitive—such that for every infinite sequence (x_n)_{n=1}^\infty in X, there exist indices i < j with x_i \leq x_j.^[1] This condition ensures the absence of "bad" infinite sequences where no earlier element relates to a later one.^[2] Equivalently, a well-quasi-ordering is well-founded (every nonempty subset has a minimal element, precluding infinite descending chains) and admits no infinite antichains (subsets in which no two distinct elements are comparable).^[1] The theory of well-quasi-orderings originated in the mid-20th century as a generalization of well-orderings to non-antisymmetric relations, with foundational contributions from Graham Higman, Paul Erdős, Richard Rado, Joseph Kruskal, and Crispin Nash-Williams.^[3] Higman introduced key aspects in 1952, proving in the context of abstract algebras that if a quasi-order on a set is well-quasi-ordered, then the set of all finite sequences over that set, ordered by the subsequence (or subword) relation, is also well-quasi-ordered; this result is known as Higman's lemma and forms a cornerstone for inductive arguments on words and structures.^[3] Kruskal extended the idea to trees in 1960, showing that finite trees under the homeomorphic embedding relation (topological minors) form a well-quasi-order.^[1] Further developments include Nash-Williams's 1963 theorem providing a shorter proof that finite trees are well-quasi-ordered under the topological minor relation, and his 1965 extension to infinite trees, yielding broader closure properties.^[4] A landmark application arose in graph theory: Wagner's conjecture, positing that finite graphs are well-quasi-ordered by the minor relation, was affirmatively resolved by Neil Robertson and Paul Seymour in a series of 20+ papers from 1983 to 2004, yielding polynomial-time algorithms for minor-closed graph properties via the graph minors theorem.^[1] These results underscore the theory's depth, as well-quasi-orderings often require intricate proofs despite their intuitive finite-control appeal.^[3] Well-quasi-orderings have profound implications across mathematics and computer science, including termination analyses for term-rewriting systems, decidability in logic, and structural complexity in combinatorics.^[3] For instance, they enable the classification of hereditary graph classes and embeddings in relational structures, while extensions like better-quasi-orderings (which strengthen the property to sequences without infinite descending or antichain-like behaviors) address infinite settings.^[1] The concept's frequent independent rediscovery highlights its natural emergence in diverse fields, from algebra to topology.^[3]

Definitions and Basics

Quasi-orders and Well-quasi-orders

A quasi-order on a set X is a binary relation \leq that is reflexive and transitive, but not necessarily antisymmetric.^[1]^[5] The associated strict quasi-order < is defined by x < y if and only if x \leq y and x \neq y.^[5] A partial order is a special case of a quasi-order that additionally satisfies antisymmetry, meaning x \leq y and y \leq x implies x = y.^[1] A quasi-order \leq on X is a well-quasi-ordering, denoted X is wqo under \leq, if every infinite sequence (x_n)_{n \in \mathbb{N}} in X admits indices i < j such that x_i \leq x_j.^[6]^[7] This condition ensures the absence of infinite strictly descending sequences, where a sequence (x_n) is strictly descending if x_{n+1} < x_n for all n, and the absence of infinite antichains, where an antichain is a subset of pairwise incomparable elements (i.e., x \not\leq y and y \not\leq x for distinct x, y).^[8] These equivalent characterizations—no infinite strictly descending sequences and no infinite antichains—fully define the well-quasi-ordering property.^[8] Well partial orders arise as the antisymmetric special case of well-quasi-orderings.^[1]

Well Partial Orders

A well partial order (wpo) on a set X is a partial order \leq on X such that there are no infinite descending chains and no infinite antichains in (X, \leq).^[9] Equivalently, every infinite sequence (x_i)_{i \in \mathbb{N}} in X admits indices i < j with x_i \leq x_j, meaning there are no bad sequences—infinite sequences without any increasing pair.^[9] Such orders are often denoted as (X, \leq) being a wpo.^[10] Since partial orders are a subclass of quasi-orders, every wpo is a well-quasi-order (wqo), but the converse does not hold: a wqo need not be antisymmetric.^[10] For instance, the universal quasi-order on an infinite set X, defined by x \leq y for all x, y \in X, is a wqo (as every sequence has increasing pairs) but fails antisymmetry, hence is not a partial order or wpo.^[10] A partial order is a wpo if and only if it is well-founded (no infinite descending chains) and has finite width, where the width is the cardinality of the largest antichain.^[9] By Dilworth's theorem, finite width implies the poset decomposes into finitely many chains, which, combined with well-foundedness, ensures the wqo property.^[9] This characterization highlights the structural constraints distinguishing wpos from general wqos, with applications in combinatorics and logic where antisymmetry is essential.^[9]

Historical Context and Motivation

Development History

The concept of well-quasi-ordering traces its origins to early 20th-century algebraic results, with Leonard Eugene Dickson's 1913 lemma serving as a key precursor by establishing that the set of monomials in a polynomial ring over the natural numbers is well-partially-ordered under divisibility, implying finite generation of monomial ideals. This result addressed foundational questions in commutative algebra but lacked a general framework for broader quasi-orders. A pivotal advancement came in 1952 with Graham Higman's lemma, which generalized Dickson's result to show that if a quasi-order is well-quasi-ordered, then the set of finite words over it is also well-quasi-ordered under the subsequence embedding relation. Higman introduced the terminology "well-quasi-ordering" in this context, providing a combinatorial tool for avoiding infinite antichains and descending chains in sequences, with applications to semigroup theory and abstract algebras. In 1960, Joseph B. Kruskal extended these ideas in his tree theorem, proving that the set of finite labeled trees is well-quasi-ordered under homeomorphic embedding when labels come from a well-quasi-ordered set, linking wqo theory to structural combinatorics on trees. This work resolved Vazsonyi's conjecture on infinite families of trees and influenced subsequent developments in embedding orders. The 1980s marked a major expansion through the work of Neil Robertson and Paul D. Seymour, whose graph minors project culminated in proving that the class of finite graphs is well-quasi-ordered under the minor relation, implying that minor-closed graph families have finite forbidden minor characterizations.^[11] Their multi-volume series, beginning in 1983, drew on wqo techniques to resolve long-standing problems in graph theory. Wqo theory also drew influences from proof theory, where ordinal analysis and closure properties intersected with algebraic structures, and from semigroup theory. Extensions like better-quasi-orders, introduced by Crispin Nash-Williams in 1965, strengthened the framework to handle infinite sequences and arrays without bad embeddings, enabling applications beyond finite cases. More recently, foundational results have seen rephrasings and constructive analyses rather than entirely new theorems; for instance, Diana Schmidt's 2020 work provides streamlined proofs of classical results like Higman's and Kruskal's theorems while exploring maximal order types of well-partial orderings.^[12] No major new foundational theorems on wqo have emerged post-2000, though applications in logic and computer science continue to refine the theory.

Key Motivations

One key motivation for studying well-quasi-orders arises from the limitations of well-founded quasi-orders, which, while preventing infinite descending chains, can still harbor infinite antichains—sets of pairwise incomparable elements that complicate analysis in infinite structures. For instance, the set of all finite subsets of the natural numbers under inclusion is well-founded but contains infinite antichains, such as the collection of all singleton sets \{ \{n\} \mid n \in \mathbb{N} \}, where no two elements are comparable. This pathology hinders the application of such orders to constructions like sequences or subsets, as these operations may propagate unbounded incomparability, leading to non-terminating or undecidable processes in combinatorial and algebraic settings.^[13] Well-quasi-orders address this by additionally prohibiting infinite antichains, ensuring that operations such as sums, products, and subsequences preserve the well-quasi-ordering property and remain free of "bad" infinite behaviors. This stability is crucial for theoretical frameworks where infinite objects must be hierarchically organized without introducing pathological incomparabilities, as originally emphasized in the context of divisibility orders in abstract algebras.^[14] In combinatorial contexts, well-quasi-orders provide guarantees against infinite descending chains in sequences or trees, facilitating termination arguments in algorithms and proof systems, such as those involving graph minors or term rewriting.^[15] Algebraically, well-quasi-orders enable the embedding of structures into ordinals, assigning ranks that quantify the "size" or complexity of ordered sets in a precise manner, which is essential for measuring progress in inductive definitions and transfinite constructions. A classic illustration of the need for well-foundedness alone is insufficient comes from the integers under the usual order \leq, which admits an infinite descending sequence -1 > -2 > -3 > \cdots, rendering it unsuitable for applications requiring no infinite descents. These motivations, pioneered by figures like Graham Higman in his work on abstract algebras, underscore the role of well-quasi-orders in taming infinite behaviors across mathematics.^[14]

Examples

Arithmetic and Ordinal Examples

The set of natural numbers \mathbb{N} under the standard ordering \leq exemplifies a well partial order. Every nonempty subset of \mathbb{N} possesses a minimal element, ensuring well-foundedness, while the total order structure precludes infinite antichains, as any two distinct elements are comparable.^[8] In opposition, the integers \mathbb{Z} ordered by \leq fail to constitute a well-quasi-order. The infinite descending chain $0 > -1 > -2 > \cdots demonstrates a lack of well-foundedness, permitting unbounded decrease.^[16] Finite direct products of natural numbers inherit this well partial order structure under componentwise comparison. Specifically, \mathbb{N}^k for finite k is a well partial order, a result known as Dickson's lemma, which guarantees that monomial ideals in polynomial rings are finitely generated and, more generally, that every subset admits only finitely many minimal elements.^[9] Well-ordered sets provide another foundational class of well partial orders. Any such set is well-founded by definition, and its linear ordering ensures that antichains are singletons, eliminating the possibility of infinite antichains.^[8] For a well partial order X, the ordinal type o(X) is the supremum of the order types of its linear extensions. Equivalently, o(X) is the rank of the well-founded tree of finite bad sequences in X. This ordinal measures the hierarchical depth or complexity of X.^[8] The positive rational numbers \mathbb{Q}^+ under divisibility, defined by p \mid q if q = p \cdot n for some positive integer n, do not form a well-quasi-order. The infinite collection of prime numbers constitutes an antichain, as no distinct primes divide one another, violating the finite antichain condition.^[16]

Combinatorial Examples

One prominent combinatorial example of a well-quasi-order arises in the context of finite words over a well-quasi-ordered alphabet \Sigma under the subsequence embedding relation, where a word u embeds into v if there is an order-preserving injection from positions in u to positions in v such that corresponding letters satisfy the order on \Sigma. Higman's lemma establishes that this structure forms a well-quasi-order. For instance, over the singleton alphabet \{a\} with the discrete order, the chain a \prec ab \prec abc \prec \cdots illustrates increasing embeddings, with no infinite antichains or descending chains. A related example generalizes this to finite sequences of natural numbers under embedding, where a sequence (s_1, \dots, s_k) embeds into (t_1, \dots, t_\ell) if there exist indices $1 \leq i_1 < \cdots < i_k \leq \ell such that s_j \leq t_{i_j} for each j. This forms a well-quasi-order, extending Dickson's lemma from fixed-length tuples under componentwise order to variable lengths. In graph theory, the collection of all finite undirected graphs, ordered by the minor relation (where G is a minor of H if G can be obtained from a subgraph of H by contracting edges), constitutes a well-quasi-order, as proven in the Robertson–Seymour theorem.^[17] This result implies that any infinite family of finite graphs contains two where one is a minor of the other, with profound implications for structural graph theory despite the lengthy proof across multiple papers. For trees, consider finite trees with nodes labeled from a well-quasi-ordered set, under homeomorphic embedding (an injective order-preserving map between nodes that preserves ancestry and labels). Kruskal's tree theorem shows that this relation yields a well-quasi-order. Similarly, the set of finite partially ordered sets (posets) whose elements are labeled from a well-quasi-ordered set [Q](/page/Q), ordered by label-preserving order embeddings (injective strictly order-preserving maps respecting labels via \leq_Q), forms a well-quasi-order.^[3] In contrast, extending to infinite structures often fails: for example, the set of infinite words over a finite alphabet under subsequence embedding is not a well-quasi-order.

Properties

Structural Properties

A well-quasi-order (wqo) on a set X is characterized by the absence of infinite strictly descending chains and infinite antichains in the strict order < derived from the quasi-order \leq.^[8] This means that for any sequence (x_n)_{n \in \mathbb{N}} in X, there do not exist indices i_1 < i_2 < \cdots such that x_{i_{k+1}} < x_{i_k} for all k, nor a subsequence where all elements are pairwise incomparable.^[7] The finiteness of the width follows from this property: the size of the largest antichain is finite, as guaranteed by the dual of Mirsky's theorem applied to the well-founded structure.^[18] The lack of infinite descending chains implies that every wqo is well-founded, ensuring that every nonempty subset of X has at least one minimal element with respect to \leq.^[19] Consequently, wqos are closed under taking subsets: if Y \subseteq X and (X, \leq) is a wqo, then the restriction of \leq to Y inherits the same structural absences, making (Y, \leq|_Y) a wqo as well.^[19] An associated ordinal invariant is the rank o(X), defined as the height of the tree of finite bad sequences (sequences with no i < j such that x_i \leq x_j) ordered by initial segment extension, which well-orders this tree due to the wqo property.^[20] Every bad sequence in X is finite, as the existence of an infinite bad sequence would contradict the wqo condition; moreover, o(X) bounds the complexity of this tree structure.^[20] For a wqo of finite width w(X) = n < \infty, the rank satisfies o(X) < \omega^\omega, bounding the complexity of the order structure.^[20]

Sequence Characterizations

A quasi-order (X, \leq) is well-quasi-ordered if and only if every infinite sequence x_0, x_1, x_2, \dots in X admits indices i < j such that x_i \leq x_j.^[21] This characterization captures the dynamic behavior of elements under the order, ensuring that no infinite sequence can avoid "progress" indefinitely.^[19] Equivalently, (X, \leq) is well-quasi-ordered if every infinite sequence contains an infinite non-decreasing subsequence x_{i_0} \leq x_{i_1} \leq x_{i_2} \leq \dots with i_0 < i_1 < i_2 < \dots .^[1] This strengthening highlights the abundance of monotonic structures within any unbounded listing of elements.^[21] Central to these characterizations is the notion of a bad sequence: an infinite sequence x_0, x_1, x_2, \dots in X such that x_i \not\leq x_j for all i < j.^[19] Thus, (X, \leq) is well-quasi-ordered if and only if it admits no infinite bad sequence.^[1] Bad sequences are necessarily finite and maximal in well-quasi-orders, meaning any extension would introduce an increasing pair; their bounded length prevents the construction of infinite descending or incomparable chains.^[22] This finiteness aligns with the absence of infinite antichains, as an infinite bad sequence would form such an antichain.^[21] These sequence properties evoke principles from Ramsey theory, guaranteeing the existence of "good" (non-decreasing) subsequences in any infinite enumeration of elements from a well-quasi-order, regardless of the ordering chosen.^[1] Unlike classical Ramsey results that seek monochromatic cliques, here the focus is on order-preserving progress, ensuring structural coherence in infinite listings.^[19] A sketch of the equivalence between the primary characterization and the absence of infinite antichains proceeds by contradiction: assume an infinite antichain A \subseteq X; enumerate it as a sequence x_0, x_1, \dots , which must be bad since elements are incomparable, yielding an infinite bad sequence and violating the sequence condition. Conversely, an infinite bad sequence directly forms an antichain, forcing increases in any sequence to avoid such pathologies.^[21] This interplay underscores how sequence dynamics enforce the static finiteness of antichains.^[1]

Constructions and Theorems

Basic Constructions

One fundamental property of well-quasi-orders (wqos) is their closure under certain basic operations, allowing the construction of new wqos from existing ones. A hereditary subset of a wqo inherits the well-quasi-ordering: if (Q, \leq_Q) is a wqo and P \subseteq Q, then (P, \leq_P) is a wqo where p \leq_P p' if and only if p, p' \in P and p \leq_Q p'.^[13] Furthermore, the quotient of a wqo by its associated equivalence relation yields a well partial order (wpo): for a quasi-order Q, define x \sim y if and only if x \leq y and y \leq x; the equivalence classes under \sim form a poset that is a wpo if Q is a wqo.^[13] Disjoint unions, or more generally ordered sums, preserve the wqo property. Specifically, if P is a wpo and for each p \in P, Q_p is a wqo, then the sum \sum_{p \in P} Q_p is a wqo, ordered by (p, q) \leq (p', q') if p = p' and q \leq_{Q_p} q', or p < p'. In particular, the disjoint union of finitely many wqos (where components are incomparable) is a wqo, as antichains and descending chains remain finite within each component.^[13] Cartesian products of wqos are wqos under the componentwise order. If (X_i, \leq_i) are wqos for i = 1 to n, then the product \prod_{i=1}^n X_i with (x_1, \dots, x_n) \leq (y_1, \dots, y_n) if and only if x_i \leq_i y_i for all i is a wqo; this is a classical result known as Dickson's lemma in the case of the natural numbers under addition.^[13] For two wqos X and Y, the lexicographic product X \times_{\lex} Y—ordered by (x_1, y_1) \leq (x_2, y_2) if x_1 < x_2 or (x_1 = x_2 and y_1 \leq y_2)—is also a wqo, generalizing the finite product construction.^[23] The set of finite sequences (or tuples) over a wqo forms a wqo under appropriate embeddings. If (X, \leq) is a wqo, then X^{<\omega} = \bigcup_{n < \omega} X^n, the set of all finite sequences from X, is a wqo under the Higman embedding order, where one sequence embeds into another as a subsequence preserving the order.^[19] These constructions relate to ordinal invariants of wqos, where the ordinal o(Q) of a wqo Q is the supremum of ordinals embeddable into Q. For the lexicographic product, o(X \times_{\lex} Y) \geq o(X) \cdot o(Y).^[23]

Fundamental Theorems

One of the foundational results in the theory of well-quasi-orders is Higman's lemma, which establishes that the set of finite words over a well-quasi-ordered alphabet forms a well-quasi-order under the subsequence relation. Specifically, if (A, \leq) is a well-quasi-order, then the set A^* of all finite sequences from A, ordered by the embedding where u \leq v if u is a subsequence of v, is also a well-quasi-order.^[24] This lemma provides a key construction for building well-quasi-orders from simpler ones and has implications for proving termination in term rewriting systems by ensuring no infinite descending chains exist in generated structures. Kruskal's tree theorem extends this idea to tree structures, stating that the set of finite trees labeled by elements from a well-quasi-ordered set, under the homeomorphic embedding relation (where one tree embeds into another preserving labels and ancestry), forms a well-quasi-order.^[3] This result generalizes Higman's lemma to branching structures and is crucial for analyzing ordered families of trees, such as in proof theory and algorithm termination arguments, where it guarantees the finiteness of bad sequences. The Robertson-Seymour theorem applies well-quasi-ordering to graph theory, proving that the set of all finite graphs, ordered by the minor relation (where G \leq H if G is a minor of H), is a well-quasi-order. As a consequence, for any minor-closed family of graphs (i.e., one closed under taking minors and disjoint unions), the set of minimal forbidden minors is finite, leading to structural characterizations and algorithmic decidability for properties like planarity testing within such families. A broader generalization of these results is that embeddings into structures over a well-quasi-ordered base preserve well-quasi-ordering: if the labels form a well-quasi-order, then the poset of finite structures under order-preserving embeddings is well-quasi-ordered.^[3] This principle unifies Higman's and Kruskal's theorems and extends to various relational structures, ensuring that complexity in embeddings does not introduce infinite antichains or descending chains. Better-quasi-orders provide an extension of well-quasi-orders to handle certain infinite descending chains in a controlled manner, where every infinite sequence or array admits a good subsequence without unbounded antichains. Introduced to study transfinite sequences, this notion allows analysis of infinite structures while maintaining combinatorial control, with applications in set theory for uncountable cardinals. These theorems collectively imply termination guarantees for processes generating sequences, trees, or graphs under well-founded embeddings, as the absence of bad infinite sequences ensures all chains are finite or controlled, facilitating decidability and proof automation in logic and computer science.^[3]

Applications

In Combinatorics and Graph Theory

Well-quasi-orderings play a pivotal role in graph theory through their application to the minor relation. The minor relation on the set of finite undirected graphs forms a well-quasi-order, implying that every minor-closed family of graphs admits a finite set of forbidden minors as a characterizing basis. This structural result, known as the finite forbidden minors theorem, ensures that properties definable by excluding finitely many minors can be algorithmically recognized, with profound implications for graph algorithm design and complexity classification. Kruskal's tree theorem establishes that the collection of finite trees labeled over a well-quasi-ordered set is itself well-quasi-ordered under the homeomorphic embedding relation. This theorem extends to bounding tree decompositions in graphs, where graphs of bounded treewidth can be viewed as tree-like structures; consequently, such graphs are well-quasi-ordered under the minor relation, providing bounds on decomposition widths and facilitating proofs of structural graph theorems.^[25] In the theory of partially ordered sets, well-quasi-orderings on classes of interval orders—posets representable by intersecting intervals—yield finite representations for hereditary properties, as the embedding relation on finite interval orders ensures no infinite antichains or descending chains, leading to compact characterizations via forbidden subposets.^[26] Well-quasi-orderings in combinatorics exclude infinite antichains, contributing to results that bound the sizes of certain structures.^[1] Recent advancements extend these ideas to contraction-free graphs; specifically, the class of connected graphs excluding a fixed graph H as a contraction is well-quasi-ordered under the contraction relation if and only if H is a contraction of the diamond graph, broadening the scope beyond minors to include topological contractions.^[27] In combinatorial game theory, impartial games model positions as a well-quasi-ordered set under legal moves, ensuring no infinite descending chains and thus guaranteeing finite game lengths, which supports the analysis of winning strategies and Grundy numbers in games like Nim variants.^[28]

In Computer Science

Well-quasi-orderings (WQOs) play a crucial role in ensuring the termination of term rewriting systems (TRSs), where a WQO on terms guarantees that no infinite reduction sequences exist, as any sequence of terms must eventually stabilize under the ordering.^[29] In particular, the Knuth-Bendix completion procedure relies on embedding orders, which form a WQO on terms, to prove termination by embedding the rewrite relation into a well-founded order, preventing non-terminating computations during critical pair analysis.^[30] This approach extends to recursive path orderings and other simplification orders, where the WQO property ensures the absence of infinite descending chains in term reductions.^[31] Dependency pairs, introduced for automated termination proofs in TRSs, leverage WQOs to analyze potential non-termination cycles by reducing the problem to proving well-foundedness on a set of inequalities derived from rewrite rules. For confluence, WQOs on dependency pairs facilitate relative termination analyses, where embedding the joinability relation into a WQO ensures that overlapping reductions can be resolved without divergence, as seen in modular confluence criteria for constructor-based TRSs. These techniques enable tools like AProVE to certify confluence by verifying WQO properties on approximated dependency graphs.^[32] In the context of infinite data structures, WQOs underpin productivity checks for coinductive types, ensuring that corecursive definitions generate infinite outputs without stalling, by imposing a WQO on approximations of coinductive streams or trees to bound non-productive behaviors.^[33] For instance, continuous types in dependently typed languages use WQO-based guardedness criteria to verify that coinductive producers maintain progress, preventing infinite loops in type checking or evaluation.^[34] Algorithmic meta-theorems for higher-order recursion schemes employ WQOs to decide model-checking problems, where a WQO on configurations compatible with scheme unfoldings bounds the state space, yielding decidable complexity analyses for properties like reachability in higher-order pushdown automata.^[35] Ong's framework demonstrates that modal mu-calculus properties over schemes generated by higher-order recursion are decidable via abstract interpretation under a WQO, with elementary complexity in many cases.^[36] The Dagstuhl Seminar 16031 in 2016 highlighted WQOs' applications in computer science, particularly for verification and automata theory, discussing how WQOs enable decidability in infinite-state systems like vector addition systems and higher-order model checking.^[37] Participants explored WQO-based techniques for automata over infinite alphabets and parameterized verification, bridging order theory with practical tool development.^[38] More recent works, such as the 2020 volume Well-Quasi Orders in Computation, Logic, Language and Reasoning, continue to expand these applications across logic and verification.^[39] In model checking, well-structured transition systems (WSTS) use a WQO on states that is monotonic with respect to transitions to ensure the backward reachability algorithm terminates, avoiding infinite loops by guaranteeing no infinite antichains in predecessor sets.^[40] This framework applies to systems like Petri nets and broadcast protocols, where the WQO prevents exploration of unbounded state spaces without convergence, enabling decidable verification of safety properties.^[41]

References

[1]
[PDF] well-quasi-ordering
A quasi-order is a binary relation E on a set X that is reflexive and tran- sitive. A partial order is an antisymmetric quasi-order. A total order E is a ...
[2]
[PDF] On well-quasi-ordering finite trees
This paper presents a new and shorter proof of the following theorem of Kruskal (2). THEOREM 1. The set of all trees is wqo. If A, B are subsets of Q, a mapping ...
[3]
The theory of well-quasi-ordering: A frequently discovered concept
A partially ordered set is called well-partially-ordered if every subset has at least one, but only a finite number, of minimal elements.
[4]
[PDF] Well-quasi-ordering - Robin Thomas
A quasi-order is (Q,≤), where ≤ is reflexive and transitive. NOTE Let x ≡ y mean x ≤ y and y ≤ x. Then Q/≡ is a partial order. Define x<y to mean x ≤ y and ...
[5]
[PDF] 1 Introduction 2 Well Quasi Orders
Definition 2.1 A set together with an ordering (X, ) is a well quasi ordering (wqo) if for any. sequence x1,x2,... there exists i, j such that i<j and xi xj.
[6]
[PDF] A well-quasi-order for tournaments - Princeton Math
Nash-Williams, that in any infinite set of graphs, one of them is weakly immersed in another (we define weak immersion below). It is tempting to try to ...<|control11|><|separator|>
[7]
[PDF] Well-quasi-orderings and computability theory. - UC Berkeley math
Definition: A well-quasi-ordering (wqo), is quasi-ordering which has no ... maximal order types of the wpo's investigated by Kruskal and. Nash-Williams.
[8]
Dickson's Lemma, Higman's Theorem and Beyond: A survey of ...
... well partial order. In this note, we restrict our attention to some ... no infinite descending chain and no infinite antichain. Hence Lemma 2.5 ...
[9]
[PDF] Algorithmic Complexity of Well-Quasi-Orders
Dec 13, 2017 · A well-quasi-order (wqo) is a qo ⟨A,≤⟩ such that any infinite ... well-partial-order (wpo). Note that quotienting a wqo by the ...<|control11|><|separator|>
[10]
[PDF] Graph Minors. IV. Tree-Width and Well-Quasi-Ordering
Theorem (1.5) was first proved in the original draft of this paper in 1982. Thomas, having heard of our result but not having seen the proof, worked out his ...
[11]
Well-Quasi Orders in Computation, Logic, Language and Reasoning
In stockThis book transfers knowledge between the different areas of logic, mathematics and computer science by delving into the theory of well quasi-orders.
[12]
[PDF] A motivated introduction to better-quasi-orders - arXiv
Nov 22, 2017 · Another approach to super-sequences initiated by Simpson [Sim85] has proved very useful in the theory of better-quasi-orders. We now ...Missing: 1980s | Show results with:1980s
[13]
6 - DOI
No information is available for this page. · Learn whyMissing: Higman 1952 second symmetric group motivation
[14]
well-quasi-order in nLab
May 24, 2017 · 1. Definition. In classical mathematics, a well-quasi-order is a preorder ( P , ≤ ) such that for any infinite sequence x i in P , there exist ...
[15]
[PDF] Well quasi-order in combinatorics: embeddings and homomorphisms
In contrast, (Z, ≤) is not a wqo because it is not well-founded, and (N, |), the natural numbers ordered by divisibility, is not a wqo since the prime numbers ...
[16]
[PDF] Well-Quasi-Orders for Algorithms MPRI Course 2.9.1 – 2017/2018
The Robertson-Seymour Theorem (Robertson and Seymour, 2004) states that (fi- nite, undirected, without self-loops) graphs are well-quasi-ordered under minors.Missing: Marshall Hall
[17]
Graph Minors. XVIII. Tree-decompositions and well-quasi-ordering
This lemma is crucial in the proof of Wagner's conjecture, that the class of all finite graphs is well-quasi-ordered by minors.Missing: original | Show results with:original
[18]
[PDF] rigid borel sets and better quasiorder theory - Web.math.wisc.edu
A well quasiorder (WQO) is a quasiorder which has no infinite descending chains or infinite antichains (where antichain here means pairwise incomparable set).
[19]
[PDF] Well Quasi-Orders and the Functional Interpretation - Thomas Powell
The purpose of this article is to study the role of Gödel's functional interpretation in the extraction of programs from proofs in well quasi-order theory. The ...
[20]
None
### Summary of Ordinal Type o(X) and Rank for Well-Quasi-Orders
[21]
[PDF] Algorithmic Aspects of WQO (Well-Quasi-Ordering) Theory
... closed if x ⩾ y ∈ V implies x ∈ V. (There is a similar notion of downward-closed sets). For B ⊆ X, the upward-closure ↑B of B is {x | x ⩾ b for some b ∈ B}.<|control11|><|separator|>
[22]
[PDF] WELL-QUASI-ORDERING, THE TREE THEOREM, AND ... - TAU
Well-quasi-order. Algebra A. Space containing T(Q) ... 326-336. 2. Joseph Kruskal, Well-partial-order and Rado's conjecture, submitted to the Proc. London.
[23]
[PDF] Measuring well quasi-orders and complexity of verification
Nov 20, 2024 · Lopez, S. Schmitz, Ph. Schnoebelen, I. Vialard, Measuring well quasi-ordered finitary powersets, soon to be submitted to MSCS.
[24]
Ordering by Divisibility in Abstract Algebras - Oxford Academic
Graham Higman; Ordering by Divisibility in Abstract Algebras, Proceedings of the London Mathematical Society, Volume s3-2, Issue 1, 1 January 1952, Pages 3.
[25]
Graph minors. IV. Tree-width and well-quasi-ordering - ScienceDirect
We prove a strengthening of Kruskal's result-Wagner's conjecture is true for all sequences in which G 1 is planar.
[26]
From Well-Quasi-Ordered Sets to Better-Quasi-Ordered Sets
Aug 10, 2025 · ... (s) \ ↓f(t). (See Equation 7.) This map f. ′. is bad and the order type of B. ′. is at most αω. (iv) ⇒ (iii) Trivial. (iii) ⇒ (ii) ...
[27]
[1602.00733] Well-quasi-ordering H-contraction-free graphs - arXiv
Abstract:A well-quasi-order is an order which contains no infinite decreasing sequence and no infinite collection of incomparable elements.
[28]
[PDF] Combinatorial Game Complexity: An Introduction with Poset ... - arXiv
Jun 24, 2015 · Combinatorial games that are not impartial are known as partisan. ... The theory of well-quasi-ordering: A frequently discov- ered concept.
[29]
Well rewrite orderings and well quasi-orderings - ScienceDirect
... well-quasi-ordering are given. A tool based on ... Forgaard, D. Detlefs. An incremental algorithm for proving termination of term rewriting systems.
[30]
[PDF] Termination of Rewriting' - TAU
Clearly, any extension of a well-quasi-ordering is also a well-quasi-ordering. ... Uniform termination of term-rewriting systems: Reeursive decomposition ordering ...
[31]
[PDF] Orderings for term-rewriting systems - SciSpace
prove the termination of term-rewriting systems: ... If there exists any well-quasi-ordering ::::: of ... conjunction \",ith the First Termination Theorem to prove ...
[32]
[PDF] Termination of Term Rewriting: Foundation, Formalization ... - DROPS
Dependency pairs revisited. In ... doi:10.1007/978-3-642-02348-4_21. 26. J.B. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyia's conjecture.
[33]
Stop When You Are Almost-Full | SpringerLink
References. Abel, A.: Termination and productivity checking with continuous types. ... Kruskal, J.B.: Well-quasi-ordering, the Tree Theorem, and Vazsonyi's ...
[34]
Stop When You Are Almost-Full - Adventures in Constructive ...
Aug 7, 2025 · Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture ... We analyze the interpretation of inductive and coinductive types as ...
[35]
[PDF] Higher-Order Model Checking: An Overview
Higher-order recursion schemes, or equivalently the λY- calculus, are an ... the subword ordering, is a well-quasi ordering. A corollary is that the ...
[36]
[PDF] Algorithmic Complexity of Well-Quasi-Orders - ENS-PARIS-SACLAY
sequence of ordinal ranks computed by the decomposition algorithm is (g,n0)-controlled. The algorithm runs in SPACE(gωω2. (n0)). 30/35. Page 115. Vector ...<|control11|><|separator|>
[37]
Dagstuhl Seminar 16031: Well Quasi-Orders in Computer Science
The transfer from sets to functions requires some notions and results of wqo theory in order to define and study the hierarchies and reducibilities that arise ...<|control11|><|separator|>
[38]
[PDF] Well Quasi-Orders in Computer Science - DROPS - Schloss Dagstuhl
This is a survey talk about WQO and BQO theory in reverse mathematics. 3.18 Dimensions of Mobility. Roland Meyer(University of Kaiserslautern, DE). License.
[39]
Well-structured transition systems everywhere! - ScienceDirect.com
... systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In this ...
[40]
Well (and Better) Quasi-Ordered Transition Systems | Cambridge Core
Jan 15, 2014 · The framework combines two concepts, namely (i) transition systems which are monotonic wrt. a well-quasi ordering; and (ii) a scheme for ...