Language generation from infinite samples needs finite evidence sizes
Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarch
Formal Languages and Automata TheoryMachine Learning
Summary
The paper studies how to generate new correct examples from an infinite language when given only endless positive examples. The authors find that this is possible exactly when each correct example has a small, finite piece of evidence pointing to it, and these pieces overlap infinitely among examples seen so far. They introduce a measure called positive separation width to describe how large these finite evidence pieces must be, showing that various sizes of evidence are needed in different cases. The work uses formal verification in a proof assistant called Lean to confirm all parts of their findings.
language generation in the limitinfinite languagefinite witnesspositive presentationnormalizationseparation widthcombinatorial dataLean proof assistantcountable familiesdiagonal capture lemma
Authors
Xiaoyu Li, Andi Han, Jiaojiao Jiang, Junbin Gao
Abstract
Language generation in the limit asks for valid unseen elements from every exhaustive positive presentation of an unknown infinite language. We characterize this task for arbitrary families over a countable universe. Generation is possible exactly when each target can be assigned a finite positive witness so that the targets activated by any finite sample have an infinite common intersection. The necessary direction follows from a universal normalization: a search through unconfirmed histories converts any successful generator into one depending only on the observed set. We then ask how large compatible witnesses must be. Positive separation width records the smallest uniform size bound, with two further levels for unbounded finite witnesses and the absence of any compatible finite-witness assignment. Every level occurs. Countable families admit singleton witnesses, explicit families realize every finite width, and a union of two families with infinite common cores requires unbounded finite witnesses. Finally, countable-support and finite-profile obstructions explain why local combinatorial data cannot determine generation in the limit. The characterization and full width hierarchy are checked in Lean, including the simplified normalization and a direct diagonal capture lemma. The accompanying Lean development is maintained at https://github.com/xiaoyulics/language-generation-characterization