PaperlayerView exact revision on arXiv

Source-linked AI summary

Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

Diego Figueira, Santiago Figueira, Sylvain Schmitz, Philippe Schnoebelen

arXiv:1007.2989v3cs.LOcs.CC

TL;DR

Dickson’s Lemma supports termination and finiteness proofs, but deriving useful complexity bounds from those proofs is a recognized challenge. The paper analyzes controlled bad-sequence lengths through a new decomposition approach, improving the hierarchy bounds and establishing their essential tightness.

  • Problem

    Although Dickson’s Lemma is used in termination arguments, deriving useful complexity bounds from it is considered difficult, and bad sequences can be arbitrarily long without control.

    Source: §1 · p. 2

  • Method

    The paper develops a decomposition approach to bound the maximal lengths of controlled bad sequences and classify the bounds by the Fast Growing Hierarchy.

    Source: §1 · p. 3

  • Results

    For linear controls, L_k,f is at level F_k, and the paper reports that its bounds are essentially tight, including for the coarser lexicographic ordering.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The paper provides examples illustrating how bounds on bad-sequence lengths can be used to derive algorithmic upper bounds.

    Source: §9 · p. 19

    Control bounds do not transfer automatically between structures with the same order type; the authors caution that translation between structures must be checked.

    Source: §9 · p. 18

Abstract

from arXiv · show

Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists do not know how to derive complexity upper bounds from such termination proofs, and the existing literature is not very helpful in these matters. We propose a new analysis of the length of bad sequences over (N^k,\leq) and explain how one may derive complexity upper bounds from termination proofs. Our upper bounds improve earlier results and are essentially tight.

1 Introduction

The paper addresses how to obtain meaningful complexity bounds from termination arguments using Dickson’s Lemma. It bounds controlled bad-sequence lengths with an improved, essentially tight hierarchy classification and shows how to apply those bounds.

1 Introduction

  • For linear controls, L_k,f is at level F_k; for f in F_gamma, it is at level F_gamma+k−1, improving the earlier F_k+1 bound for fixed k.The paper also states that its hierarchy bounds are essentially tight, including under the coarser lexicographic ordering.Source: §1 · p. 3
  • The analysis uses finite disjoint unions of powers of N to obtain finer, simpler decompositions from which bad-sequence length bounds can be extracted.The paper presents this richer setting as a way to simplify the problem.Source: §1 · p. 3
  • The paper separates decomposing bad sequences from locating the resulting bound in the Fast Growing Hierarchy, where the control function becomes relevant.Source: §1 · p. 3
  • The framework also accommodates an extended notion of bad sequences parameterized by the length of forbidden increasing subsequences.Source: §1 · p. 3
  • The paper gives examples of using its bounds in practice, while clarifying that these examples do not claim new results.The examples concern algorithms or proofs that do not directly handle bad sequences over (N^k, ≤).Source: §1 · pp. 3–4

2 WQO’s Based on Natural Numbers

This section develops the ordered-set framework used to study bad sequences over finite sums of powers of the natural numbers. It represents such sums by types and uses a well-founded multiset ordering on types for induction.

2 WQO’s Based on Natural Numbers

  • Products and disjoint sums are equipped with their usual product and sum orderings.Source: §2 · p. 4
  • Finite products and finite indexed sums of wqo’s remain wqo’s, yielding Dickson’s Lemma from the wqo property of N.Source: §2 · p. 4
  • The analysis considers finite sums of finite powers of N and represents each such sum by a type: the multiset of its powers’ dimensions.For example, 2 × N^3 + N corresponds to two copies of dimension 3 and one of dimension 1.Source: §2 · p. 4
  • Types can also be represented as functions giving each dimension’s multiplicity, with addition and scalar multiplication defined pointwise.Source: §2 · p. 4
  • The multiset ordering extends inclusion, is well-founded, and supports the paper’s induction over types.Source: §2 · pp. 4–5

3 Long Bad Sequences over Nτ

The section bounds lengths of controlled bad sequences by decomposing them into smaller sequences and applying induction over their structure.

3 Long Bad Sequences over Nτ

  • A t-controlled sequence over Nτ has each element’s infinity norm bounded by f(i+t), and Lτ(t) records the longest such bad sequence.The section assumes an increasing control function f with f(0)>0.Source: §3 · p. 5
  • For τ={1}, a t-controlled bad sequence is decreasing and has length at most f(t), since its first value is below f(t).Because f is increasing, later control constraints add nothing for a decreasing sequence.Source: §3 · p. 5
  • Induction over τ gives upper bounds on Lτ(t), the maximum length of a t-controlled bad sequence over Nτ.The general decomposition separates the first element from a suffix represented over a transformed type.Source: §3 · pp. 5, 7
  • For dimension k, the suffix after the first element is split among regions and becomes a (t+1)-controlled bad sequence over a transformed type.Each region fixes one coordinate, which can then be disregarded to view its subsequence over a lower-dimensional space.Source: §3 · pp. 5–6
  • For k≥2, the decomposition bound need not be an equality because a bad sequence over the transformed type cannot always be merged into one over Nk.A maximal bad sequence can end in the zero tuple; appending a second copy is no longer bad, although the two copies can lie in different regions.Source: §3 · p. 6

4 Long r-Bad Sequences

The section handles sequences that avoid longer increasing subsequences by layering them according to the length of increasing subsequences starting at each index. This reduces their length analysis to ordinary bad sequences.

4 Long r-Bad Sequences

  • Bounding t-controlled r-bad sequences reduces to analyzing plain bad sequences over a transformed type.The paper presents this as a benefit of its sum-of-powers-of-N approach.Source: §4 · pp. 7–8
  • An index is p-good when an increasing subsequence of length p+1 starts there; sequences lacking an increasing subsequence of length r+1 are r-bad.Dickson’s Lemma ensures r-bad sequences are finite, and bounding them is useful when an algorithm does not stop at the first increasing pair.Source: §4 · p. 7
  • The layering uses at most r non-empty layers, and each layer is a bad subsequence.If xi≤xj, then an increasing subsequence starting at xj makes xi one level better, so the two indices cannot share a layer.Source: §4 · p. 8

5 Upper Bound

The paper defines an inductive function M to bound controlled bad-sequence lengths, simplifies its maximizing strategy, and classifies its growth in the Fast Growing Hierarchy.

5 Upper Bound

  • For all τ and t, the inductively defined Mτ(t) bounds Lτ(t), the maximal length of a t-controlled bad sequence.The definition is well-formed because each recursive type is smaller in the multiset ordering.Source: §5 · p. 8

5.1 A Maximizing Strategy for M

  • The maximum in the recurrence for M is attained by choosing the smallest element of τ.This characterization simplifies the definition of M.Source: §5.1 · p. 8

5.2 Classifying M in the Fast Growing Hierarchy

  • If f is in Fγ, then Mr×{k},f is in Fγ+k−1; for linear controls, the paper gives an Fk bound and says its lower bounds make this optimal.The section reports that M{3} is already non-elementary when f(x)=2x+1.Source: §5.2 · pp. 9–10

6 Lower Bound

The section develops lower bounds for controlled bad sequences under lexicographic order, extending them to interleavings and showing that the resulting hierarchy bounds can be tight. A concrete program realizes an Ackermannian number of loop iterations, matching the upper bound.

An Inductive Definition for ℓ

  • The section defines ℓ as the longest controlled r-bad sequence under lexicographic order and gives an exact inductive definition for r = 1.It states that the lower bounds are large enough for L when f = Fγ.Source: §6 · p. 10
  • The longest controlled lexicographic bad sequence is constructed by induction on dimension, segmenting the first coordinate into constant sections whose remaining-coordinate projections are bad sequences.In the worked k = 2, t = 3, f(x) = x + 1 example, the four section lengths are 4, 8, 16, and 32; each later section starts after the previous one ends.Source: §6 · pp. 10–11
  • The lexicographic ordering can yield shorter bad sequences than the product ordering: for f(x) = 2x and t = 1, the cited lengths are 8 and 14 or less, respectively.The length-8 sequence is maximal for lexicographic order; the product-order sequence has length at most 14.Source: §6 · p. 11

Lower Bound for r-Bad Sequences

  • Concatenating r bad sequences with successively higher offsets yields lower bounds for the lengths of r-bad sequences in N^k.For r = 2, the second sequence starts at t + ℓ_{k,f}(t); Proposition 6.3 gives a lower bound for controls Fγ.Source: §6 · p. 12
  • For f = Fγ, the lower bound places ℓ_{r×{k},Fγ} in F_{γ+k−1} \ F_{γ+k−2} when γ ≥ 1 and γ + k ≥ 3.The successor-control case f = F0 instead has a matching A_k lower bound from Friedman (2001), despite the propositions’ FGH bounds differing by one level.Source: §6 · p. 12

Concrete Example

  • For k ≥ 2, the example program can execute its while loop more than A_{k+1}(m) times, matching the F_{k+1} upper bound, where m is the minimum initial counter value.The projection of its configurations onto the first k components is bad; the continuously increasing c component does not contribute to badness.Source: §6 · p. 12

7 Applications

The applications use controlled bad-sequence bounds to analyze termination and algorithmic complexity. They derive hierarchy bounds for disjunctive termination arguments, incrementing counter automata, and Karp–Miller trees, while noting that alternative control choices can shift the bound.

7 Applications

  • Controlling per-step vector growth internally raises the upper bound by one Fast Growing Hierarchy level; controlling vector sum also works, while bitsize control shifts classification from F1 to F2.The internally controlled condition is |x_i|∞ < f^i(t), and the resulting bound is one level higher because λi.f^{i+1}(t) belongs to F_{γ+1} when f belongs to Fγ.Source: §7 · p. 13

7.1 Disjunctive Termination Arguments

  • For k-ary disjunctive termination arguments with linear ranking functions into N, the program’s maximal loop iterations have an F_{k+1} upper bound, and Example 6.6 shows it is tight.The rank control is at most exponential in F2; the same answer holds if linear operations are replaced by polynomial ones.Source: §7.1 · p. 14

7.2 Reachability for Incrementing Counter Automata

  • For fixed counter dimension k, the ICA forward-saturation algorithm runs in F_k; its complexity is primitive-recursive for fixed k and Ackermannian when k is part of the input.The iteration sequence yields a controlled bad sequence, and the control function is independent of the ICA.Source: §7.2 · p. 15

7.3 Coverings for Vector Addition Systems

  • The Karp–Miller algorithm on k-dimensional VASs runs in F_{k+1}, with primitive-recursive complexity for fixed dimensions and Ackermannian complexity when k is input.A branch has length below L_{(k+1)×{k}}(|S|), so the tree and covering sizes are bounded by |∆| raised to that length.Source: §7.3 · pp. 16–17
  • The generic Karp–Miller bound is two FGH levels worse than Howell et al.’s VAS-specific F_{k−1} bound, but the paper’s analysis also applies to certain VAS extensions.The authors name strongly increasing affine nets as an extension where both the Karp–Miller algorithm and an F2 control apply.Source: §7.3 · p. 17

8 Related Work

The related-work discussion contrasts the paper’s decomposition approach with earlier bounds for Dickson’s Lemma and other well-quasi-orders. It emphasizes keeping the control function fixed through decomposition and identifies both the method’s scope and its coarse-grained limitations.

Bounds for N^k

  • For bad sequences over N^k, McAloon (1984) and Clote (1986) use interval and Ramsey arguments, while Friedman (2001) treats successor control without keeping dimension k as a parameter.The paper characterizes these earlier results as more complex or coarser, and notes that Friedman’s proof addresses the specific successor-control case.Source: §8 · p. 17

Beyond N^k

  • For Higman’s Lemma, Cichoń and Tahhan Bittar (1998) use a decomposition whose parameters and controls grow complex; this paper keeps the same fixed control function at each decomposition step.The paper also says its approach handles Higman’s Lemma, as demonstrated in Schmitz and Schnoebelen (2011).Source: §8 · pp. 17–18

Further Pointers

  • The Fast Growing Hierarchy gives coarse bounds and is of limited interest for low-complexity analyses, but the paper presents it as suited to very large algorithmic complexities.The discussion places the work in broad implicit computational complexity and lists applications including well-structured transition systems and Petri-net equivalences.Source: §8 · p. 18

9 Conclusion

The conclusion presents simpler, disjoint-sum decompositions and an explicit classification of upper bounds that keeps the control function as a parameter. It also offers three template applications showing how bounds on bad sequences translate into algorithmic upper bounds.

9 Conclusion

  • The paper aims to improve the limited use of Dickson’s Lemma upper bounds, while noting that optimality in the Fast Growing Hierarchy is a separate concern.Source: §9 · pp. 18–19
  • Equal order types alone do not ensure that a control bound transfers between structures such as N^k and finite multisets.Source: §9 · p. 18
  • The main proof uses a simple decomposition with disjoint sums, while leaving the control function explicit makes the upper-bound classification reusable.Source: §9 · p. 19
  • Three template applications illustrate how upper bounds on bad sequences translate into algorithmic upper bounds.The applications are described as varied examples of how to use the results.Source: §9 · p. 19

A.1 Proof of Theorem 3.2

The proof uses strong reflections and residual quasiorderings to reduce controlled bad-sequence bounds to simpler structures. Induction on the type then bounds the sequence length through its suffix.

A.1 Proof of Theorem 3.2

  • A strong reflection preserves t-control and badness when mapping a sequence from one quasiordering into another.It also does not increase element size.Source: §A.1 · p. 23
  • Reflections compose with disjoint sums and products, allowing reductions to be applied within these constructions.Source: §A.1 · p. 23
  • A residual A/a contains elements not above a, and a bad sequence’s suffix remains bad over the residual of its first element.Source: §A.1 · p. 23
  • Induction on τ bounds the maximal sequence by reducing its suffix to a (t + 1)-controlled bad sequence over the residual of its first element.Source: §A.1 · p. 24

A.2 Proof of Lemma 5.1

The proof establishes monotonicity of M under dominance and uses the least type element to compare residual bounds. Dominance compares ordered type elements while allowing the larger type extra elements.

A.2 Proof of Lemma 5.1

  • Dominance τ ⊑ τ′ means each decreasingly ordered element of τ is dominated by its corresponding element of τ′, which may contain extras.Source: §A.2 · p. 24
  • If τ ⊑ τ′, then Mτ(t) ≤ Mτ′(t), so dominance preserves the ordering of these bounds.Source: §A.2 · p. 25
  • For k = min τ and l ∈ τ, the residual bound using k at t + 1 is at least the bound using l at t + 1.Source: §A.2 · p. 25

A.3 Proof of Proposition 5.2

The appendix places bounds on M in Fast Growing Hierarchy classes by constructing auxiliary functions from the control function. It also gives a lower bound for the lexicographic bad-sequence length at level Fγ+k−1.

A.3 Proof of Proposition 5.2

  • For monotone f in Fγ with f(x) ≥ max(1, x), M_r×{k},f belongs to Fγ+k−1.Source: §A.3 · p. 26
  • The proof places M_r×{k},f in Fγ+k−1 by expressing it through finite substitution from G_k,f and cut-off subtraction.G_k,f is shown to belong to Fγ+k−1.Source: §A.3 · p. 26

A Simpler Version of M

  • G_n,f is monotone and at least x when f is monotone and at least x; the proof also places G_k,f in Fγ+k−1 under the stated Fγ assumptions.Source: A Simpler Version of M · pp. 27–28
  • The proof derives the class bound for M_n,f from a recursive definition using G_n,f and a bounding function in Fγ+n.Source: A Simpler Version of M · p. 30

A.4 Proof of Proposition 6.3

  • ℓ_k,Fγ(t) ≥ Fγ+k−1(t), giving a lower bound on lexicographic controlled bad-sequence length.Source: §A.4 · p. 31
Loading 1007.2989v3…