Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Measuring well quasi-ordered finitary powersets

Sergio Abriola, Simon Halfon, Aliaume Lopez, Sylvain Schmitz, Philippe Schnoebelen, Isa Vialard

TL;DR

This work investigates the ordinal invariants of the finitary powerset $P_f(A)$ of a well-quasi-order $A$ under the Hoare embedding. It demonstrates that the invariants of $P_f(A)$ are not functionally determined by $\mathbf{o}(A)$, $\mathbf{h}(A)$, and $\mathbf{w}(A)$, and establishes tight upper and lower bounds for these invariants, namely $1+\mathbf{o}(A) \le \mathbf{o}(P_f(A)) \le 2^{\mathbf{o}(A)}$, $1+\mathbf{h}(A) \le \mathbf{h}(P_f(A)) \le 2^{\mathbf{h}(A)}$, and $\mathbf{w}(P_f(A)) \ge 2^{\mathbf{w}(A)}$ with no general upper bound. To overcome non-functionality, the authors introduce weakened invariants and define a broad class of elementary wqos for which these invariants can be computed compositionally through standard constructors, including $P_f$. They prove a central result that for elementary $E$, $\mathbf{h}(P_f(E)) = \underline{\mathbf{o}}(E)$, and provide a concrete rewrite-based framework and algorithmic tools to compute these invariants from normal forms. The tightness results are established via carefully constructed families $\mathcal{H}_{\alpha}$ and $\mathcal{P}_{\alpha}$, demonstrating when the established bounds are attained. Overall, the paper offers a robust compositional approach to analyzing Pf constructions within a large and well-behaved class of wqos, with implications for complexity bounds in related verification and ordering problems.

Abstract

The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences. We study these ordinal invariants for the finitary powerset, i.e., the collection Pf(A) of finite subsets of a wqo A ordered with the Hoare embedding relation. We show that the invariants of Pf(A) cannot be expressed as a function of the invariants of A, and provide tight upper and lower bounds for them. We then focus on a family of well-behaved wqos, for which these invariants can be computed compositionally, using a newly defined ordinal invariant called the approximate maximal order type. This family is built from multiplicatively indecomposable ordinals, using classical operations such as disjoint unions, products, finite words, finite multisets, and the finitary powerset construction.

Measuring well quasi-ordered finitary powersets

TL;DR

This work investigates the ordinal invariants of the finitary powerset of a well-quasi-order under the Hoare embedding. It demonstrates that the invariants of are not functionally determined by , , and , and establishes tight upper and lower bounds for these invariants, namely , , and with no general upper bound. To overcome non-functionality, the authors introduce weakened invariants and define a broad class of elementary wqos for which these invariants can be computed compositionally through standard constructors, including . They prove a central result that for elementary , , and provide a concrete rewrite-based framework and algorithmic tools to compute these invariants from normal forms. The tightness results are established via carefully constructed families and , demonstrating when the established bounds are attained. Overall, the paper offers a robust compositional approach to analyzing Pf constructions within a large and well-behaved class of wqos, with implications for complexity bounds in related verification and ordering problems.

Abstract

The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences. We study these ordinal invariants for the finitary powerset, i.e., the collection Pf(A) of finite subsets of a wqo A ordered with the Hoare embedding relation. We show that the invariants of Pf(A) cannot be expressed as a function of the invariants of A, and provide tight upper and lower bounds for them. We then focus on a family of well-behaved wqos, for which these invariants can be computed compositionally, using a newly defined ordinal invariant called the approximate maximal order type. This family is built from multiplicatively indecomposable ordinals, using classical operations such as disjoint unions, products, finite words, finite multisets, and the finitary powerset construction.
Paper Structure (20 sections, 40 theorems, 23 equations, 3 figures, 6 tables)

This paper contains 20 sections, 40 theorems, 23 equations, 3 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Basics
  3. Upper and lower bounds for $\operatorname{\mathsf{P_f}}(A)$
  4. Maximal Order Type of $\operatorname{\mathsf{P_f}}(A)$
  5. Height of $\operatorname{\mathsf{P_f}}(A)$
  6. Width of $\operatorname{\mathsf{P_f}}(A)$
  7. Tightness of the Bounds
  8. Tight lower bound for $\operatorname{\mathbf{w}}(\operatorname{\mathsf{P_f}}(A))$ and upper bound for $\operatorname{\mathbf{o}}(\operatorname{\mathsf{P_f}}(A))$
  9. Tight upper bounds for $\operatorname{\mathbf{h}}(\operatorname{\mathsf{P_f}}(A))$
  10. An algebra of well-behaved wqos
  11. Maximal order type and width of elementary wqos
  12. Height of elementary wqos
  13. Proving \ref{['lem:fam:h-pf-oinf']}.
  14. Summary
  15. Conclusion
  16. ...and 5 more sections

Key Result

Theorem 2.4

For any $\mathsf{wqo}$$A$, $\operatorname{\mathbf{o}}(A) \leq \operatorname{\mathbf{h}}(A) \otimes \operatorname{\mathbf{w}}(A)$.

Figures (3)

  • Figure 1: Definition of the notations used in \ref{['tab:fam:la-famille']}.
  • Figure 2: $\mathcal{H}_{\omega^1}\stackrel{def}{=} \Gamma_1 + \Gamma_2 + \cdots$
  • Figure 3: Rewrite rules for elementary wqos

Theorems & Definitions (94)

  • Definition 1.0: Elementary
  • Definition 2.1: Ordinal invariants
  • Definition 2.2
  • Theorem 2.4: kriz90b
  • Corollary 2.5
  • Definition 2.6: Augmentation
  • Definition 2.7: Substructure
  • Definition 2.8: Reflection
  • Lemma 2.9
  • Lemma 2.10
  • ...and 84 more