Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarchy
Xiaoyu Li, Andi Han, Jiaojiao Jiang, Junbin Gao
cs.FL
Sep 9, 2026 · v2
cs.LG
TL;DR
The finite-witness characterization and full separation-width hierarchy, including the simplified normalization and diagonal capture lemma, are formalized in Lean.
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
Problem
Language generation in the limit asks a learner to output valid unseen elements from any exhaustive positive presentation of an unknown infinite language. A complete characterization of when ordinary (non-uniform) generation is possible for arbitrary families over a countable universe was open.
Approach
Each target is assigned a finite positive witness, and a language is active at a finite sample when its witness has appeared and the sample is consistent. Generation is shown possible exactly when the intersection of every nonempty active family is infinite. A universal normalization converts any sequence-input generator into a set-driven one via a search through unconfirmed histories. A positive separation-width hierarchy measures required witness sizes, with lower bounds supported by a bounded-capture diagonal lemma.
Results
Generation in the limit holds iff separation width is at most omega; every width level is realized, with countable families needing singleton witnesses and all-infinite-subsets requiring width omega+1. Countable-support and finite-profile obstructions show local combinatorial data cannot determine generation. The characterization, width hierarchy, simplified normalization, and diagonal capture lemma are checked in Lean.