PaperlayerView exact revision on arXiv

Source-linked AI summary

A Non-constant Lower Bound for Grammar-Based Compression with Greedy

Danny Hucke

arXiv:2609.12106v1cs.DScs.FL

TL;DR

The paper addresses the long-open question of whether Greedy has a nonconstant approximation-ratio lower bound. It constructs words that force substitutions despite intervening compression, proving an Ω(log n / log log n) bound for every execution under the stated replacement and tie-breaking rules.

  • Problem

    Whether global Greedy admits a nonconstant approximation-ratio lower bound remained open for more than twenty years after a constant lower bound was established.

    Source: §1 · p. 1

  • Method

    The construction encodes targets and uses power-free morphic auxiliaries to force substitutions despite arbitrary intervening compression of processed material.

    Source: §1 · p. 1

  • Results

    Greedy has an Ω(log n / log log n) approximation-ratio lower bound on an infinite family, for every execution using left-to-right replacement and arbitrary tie-breaking.

    Source: §1 · pp. 1–2, §5.2 · p. 10

  • Takeaways & Limitations

    The bound reaches the scale connected to addition chains and matches the lower-bound scale established for RePair.

    Source: §1 · p. 1

    The construction’s scale parameters satisfy stated inequalities, including Mh > H + B + 100.

    Source: §3.2 · p. 5

Abstract

from arXiv · show

We prove a lower bound of {\Omega}(log n/ log log n) on the approximation ratio of the global grammar-based compression algorithm Greedy. To our knowledge, the previously best lower bound was a constant, and the existence of a nonconstant lower bound had remained open for more than twenty years. Our bound holds on an infinite family of words of length n, over alphabets of growing size, for every execution using left-to-right occurrence replacement and arbitrary tie-breaking. The lower bound is also formally verified in Lean 4.

1 Introduction

The paper proves a nonconstant lower bound for global Greedy, resolving a question that had remained open for more than twenty years. Its construction forces substitutions despite Greedy’s intermediate compression choices, and the result is formally verified in Lean 4.

1 Introduction

  • Greedy is a global grammar-compression algorithm that repeatedly replaces a repeated factor chosen for the largest immediate reduction in grammar size.The smallest-grammar problem asks for a smallest context-free grammar generating the given word and no other word.Source: §1 · p. 1
  • Greedy has an Ω(log n / log log n) approximation-ratio lower bound, matching the scale previously established for RePair.The authors connect this scale to grammar compression and addition chains.Source: §1 · p. 1
  • The construction forces a sequence of substitutions while allowing arbitrary intervening compression of already processed material.Auxiliary words based on a power-free morphism make the required substitutions preferable to competing substitutions that could change a target.Source: §1 · p. 1
  • The lower bound holds for every execution using left-to-right occurrence replacement and arbitrary choices among maximizing factors.The theorem applies to explicitly specified words over alphabets of size h^2 + 4h, for h = 2r and r ≥ 10.Source: §1 · p. 2
  • The lower bound has been formalized in Lean 4, including the construction, analysis of all complete Greedy executions, and finite morphism calculations.The paper provides proof sources and reproduction instructions in.Source: §1 · p. 2

2 Preliminaries

The preliminaries define the grammar representation and Greedy’s substitution rule, then establish basic properties used in the lower-bound analysis. They also describe a factor-counting argument based on boundaries between children in a derivation tree.

2 Preliminaries

  • An SLP is an acyclic grammar with one production per nonterminal, and its generated word is the terminal expansion of its start symbol.The minimum size of an SLP generating w is denoted g(w).Source: §2 · p. 2
  • Greedy replaces a repeated eligible factor with a fresh nonterminal and a rule for that factor, reducing grammar size according to its occurrence count and length.Factors must have length at least two and at least two nonoverlapping occurrences.Source: §2 · p. 2
  • Greedy selects occurrences from left to right in each old right-hand side, yielding a maximum nonoverlapping set.The text justifies this by showing that choosing the leftmost occurrence does not obstruct later occurrences in an optimal set.Source: §2 · p. 2
  • Maximizing the gain among eligible factors is equivalent to maximizing among maximal eligible factors, and any eligible factor lower-bounds the next chosen gain.The equivalence follows from comparing a factor with a longer one having at least as many occurrences.Source: §2 · pp. 2–3
  • Substitution preserves the generated word and acyclicity, and every execution terminates after at most |w| − 1 rounds.Rounds of gain zero are allowed; the substitutions forced later in the paper have positive gain.Source: §2 · p. 3
  • The factor-counting argument locates each length-L occurrence across a child boundary, so productions’ boundaries can bound the number of distinct factors.The stated lemma allows terminals to be interpreted as either one letter or the empty word.Source: §2 · p. 3

3 The construction

The construction combines carefully chosen target runs with padded morphic auxiliaries and separators to constrain Greedy’s substitutions. A comparison grammar supplies an upper bound on the optimum grammar size against which the resulting output can be measured.

3 The construction

  • The auxiliaries force Greedy to read target lengths in base 64 one digit at a time, while distinct separators prevent substitutions between words.The targets are unary runs with carefully chosen lengths.Source: §3 · p. 3, §3.2 · p. 5

3.1 A power-free auxiliary word

  • The auxiliary word is generated by a 19-uniform morphism, and its iterates are (7/4)+-free with bounded occurrences of short factors.In each µ^2(c), any fixed factor of length 1, 2, or 3 occurs at most 121, 61, or 41 times, respectively.Source: §3.1 · p. 3
  • Padding morphic words with long runs of X limits the gain of eligible factors containing non-X letters, constraining competing substitutions.The bound is obtained by relating such factors to occurrences in the underlying morphic word and bounding short-factor counts within its blocks.Source: §3.1 · p. 4

3.2 Targets, auxiliaries, and separators

  • The targets encode binary length-q factors from a de Bruijn word, whose cyclic sequence contains each binary word of length q exactly once.The construction uses R = h^2 target integers, each positive and less than B^(2h), with their sum at most H.Source: §3.2 · pp. 4–5

3.3 A small comparison grammar

  • A comparison SLP of size at most 600h^2 is built by reusing base-64 prefixes and recursively defining the morphic auxiliaries.The prefix rules use at most 2h rules of length at most 65 per chunk; the construction also yields a lower bound on g(wh) because each terminal must occur literally in a production.Source: §3.3 · pp. 5–6
  • The word length is bounded below by Mh and above using the target and auxiliary lengths, supporting the comparison between the Greedy output and the comparison grammar.The text gives a lower bound |wh| ≥ Mh and states that the total target length is at most H.Source: §3.3 · p. 6

4 The substitutions forced by the auxiliaries

Global Greedy is forced through an ordered sequence of substitutions despite arbitrary intervening compression. An invariant separates processed material from targets and unfinished auxiliaries, while gain comparisons make the next required substitution win.

4.1 An invariant for the whole grammar

  • The invariant assigns each nonprimary, nonstart nonterminal to one processed class and keeps private alphabets disjoint.The active symbol is absent from power-layer rules, and separators occur only between start fragments.Source: §4.1 · p. 7

4.2 All factors affecting an unprocessed fragment lose

  • Only XB remains eligible among active unary factors; competing factors in targets or unfinished auxiliaries have smaller gain.The comparisons are strict, so any other chosen factor avoids both targets and unfinished auxiliaries.Source: §4.2 · p. 8

4.3 Intervening substitutions and progress

  • Intervening substitutions remain confined to processed classes, while XB stays eligible until Greedy selects it.The execution terminates after finitely many substitutions, so a factor that remains eligible must eventually be chosen.Source: §4.3 · pp. 8–9

4 The substitutions forced by the auxiliaries

  • Every execution performs the required substitutions in order, advancing the target fragments phase by phase.The forced sequence creates A1 through Ah in order, even though other substitutions may occur between them.Source: §4 · p. 6, §4.3 · p. 9

5 A lower bound on every final grammar

The proof bounds every final grammar by counting distinct factors in target words while preserving their interpretations through later substitutions. Comparing that output bound with a small grammar yields a nonconstant lower bound on an infinite family.

5.1 Keeping the primary symbols as letters

  • The proof preserves interpretations through later substitutions, then treats primary symbols as terminal letters to obtain a word containing every Us,i.It deletes the primary definitions and erases Ah before applying Theorem 2 to the resulting grammar and interpretation.Source: §5.1 · p. 9

5.2 Counting the factors in the targets

  • Across the h² target words Us,i, there are at least h³/8 distinct factors of length L.Every factor of W of length at least L occurs at most twice; the proof uses this bound to control repeated factor occurrences.Source: §5.2 · pp. 9–10
  • The output-size bound, divided by g(wh) ≤ 600h², establishes a nonconstant lower bound on an infinite family of input lengths.As r grows, h/(4r + 1) tends to infinity.Source: §5.2 · p. 10

A The finite morphism calculation

The appendix separates the finite morphism calculation into synchronization and short-factor counting. Its table concerns synchronization across two consecutive images.

A The finite morphism calculation

  • The proof has two parts: a synchronization argument and a separate short-factor count for the constants used in Theorem 4.The appendix numbers positions from 0 and uses half-open intervals.Source: A The finite morphism calculation · p. 10
  • Table 1 presents synchronization in two consecutive images, with columns for ab referring to µ(a)µ(b) and entries giving starting offsets.Source: Table 1 · p. 11

A.1 Synchronization

Equal length-18 factors in images of words with no equal adjacent letters must begin at positions with the same residue modulo 19. The proof uses matching length-seven prefixes or suffixes to fix that residue.

A.1 Synchronization

  • Equal length-18 factors in µ(x), when x has no equal adjacent letters, start at positions congruent modulo 19.Source: §A.1 · p. 11
  • Matching length-seven prefixes or suffixes in consecutive images fixes the starting residue of an equal factor.The table lists the starting offsets of those prefixes and suffixes in µ(a)µ(b) for a ≠ b.Source: §A.1 · p. 11

A.2 Preservation of power-freeness

The section proves that the morphism preserves (7/4)+-freeness by reducing the check to short representatives and ruling out a violating period in any image. This preservation is established inductively from the one-letter base case.

A.2 Preservation of power-freeness

  • A run of R equalities at period p corresponds exactly to a factor of length p + R and period p, enabling the finite period check.For the short-representative images, only periods 1 through 32 could violate power-freeness.Source: §A.2 · p. 11
  • The check reduces to seven nonempty (7/4)+-free words of length at most three, up to cyclic renaming.Their images have length at most 57, and Table 2 verifies R(p) ≤ ⌊3p/4⌋ for every tested case.Source: §A.2 · p. 11, Table 2 · p. 12
  • A factor violating (7/4)+-freeness in µ(x) would yield a period d in x with 7d < 4k, contradicting x’s power-freeness.The argument uses the factor’s contact with both end µ-blocks to recover period d.Source: §A.2 · p. 12
  • Every µe(0) is (7/4)+-free, establishing preservation of power-freeness by induction.The one-letter word 0 is the base case.Source: §A.2 · p. 12

A.3 Counts of factors of lengths one, two, and three

The section counts occurrences of factors of lengths one, two, and three in the second morphism images. These counts supply the short-factor bounds used in Theorem 4.

A.3 Counts of factors of lengths one, two, and three

  • The count separates occurrences internal to morphism blocks from those crossing block boundaries, and includes overlapping occurrences.Table 3 gives the terms for words of length at most three without equal adjacent letters; other such words have count zero by power-freeness.Source: §A.3 · p. 13, Table 3 · p. 13
  • The maximum occurrence counts in µ²(c), grouped by factor length, are 121, 61, and 41 for lengths one, two, and three, respectively.Cyclic renaming makes the counts for µ²(1) and µ²(2) permutations of those for µ²(0).Source: §A.3 · p. 13

B Lean formalisation

The paper formalises its grammar-based compression results in Lean 4.19.0 using a pinned Mathlib version. The formal development verifies the lower bound and audits theorem dependencies.

B Lean formalisation

  • The formalisation defines straight-line grammars, their size and semantics, and global Greedy with left-to-right nonoverlapping occurrence replacement.It also proves equivalence with the maximal-factor formulation in.Source: B Lean formalisation · p. 14
  • The verified argument covers the cyclic de Bruijn seed, power-freeness preservation, forced substitution phases, distinct-factor counting, and a small comparison grammar.These components yield the quantitative lower bound and its logarithmic form.Source: B Lean formalisation · p. 14
  • The final statements quantify over every terminal execution on the selected inputs, including arbitrary maximizing ties.No admitted proofs or additional axioms are used; the audit permits only Lean’s standard propositional extensionality, classical choice, and quotient soundness axioms.Source: B Lean formalisation · p. 14
Loading 2609.12106v1…