Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarch
New work characterizes language generation in the limit via finite witnesses, proves a full separation-width hierarchy, and formalizes all results in Lean.
The paper fully characterizes when language generation in the limit is possible for arbitrary families over a countable universe: each target must admit a finite positive witness such that targets activated by any finite sample share an infinite common intersection. It defines positive separation width and proves every level of the resulting hierarchy occurs, with countable families admitting singleton witnesses and unions of families with infinite common cores requiring unbounded finite witnesses. The characterization, a universal normalization, and a diagonal capture lemma are machine-checked in the Lean proof assistant, with the development maintained on GitHub.