Papers With

← All papers
First page of A Non-constant Lower Bound for Grammar-Based Compression with Greedy

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

Danny Hucke

cs.DS Sep 10, 2026 · v1 cs.FL
verification formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
The Ω(log n/log log n) lower bound on the Greedy grammar-based compression algorithm's approximation ratio is formally verified in Lean 4.
Abstract
We prove a lower bound of Ω(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.
Problem

The smallest grammar problem asks for a smallest context-free grammar generating a given word. Whether the global grammar-based compression algorithm Greedy admits a non-constant lower bound on its approximation ratio had remained open for over twenty years, with the best prior bound being a constant.

Approach

A construction is built from unary target runs and power-free auxiliary words based on Dejean's 19-uniform morphism, forcing Greedy to perform a specific sequence of substitutions while allowing arbitrary intervening compression. An invariant tracks every grammar fragment across substitution phases, and factor-count arguments bound the size of any final grammar. The lower bound is formally verified in Lean 4.

Results

An Ω(log n/log log n) lower bound is established on the approximation ratio of Greedy, holding for an infinite family of words over alphabets of growing size, for every execution using left-to-right occurrence replacement and arbitrary tie-breaking.