LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pendingjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact 2DYCK PCFG prefix laws and positive paired-prefix mass

Statement

Fix $p \in (0, 1)$ . Independently expand each nonterminal of the grammar $S \to (S) S$ , $S \to [S] S$ , $S \to ϵ$ with respective probabilities $p / 2, p / 2, 1 - p$ , and read the yield from left to right. Equivalently, start with an empty bracket stack and repeatedly choose an opening bracket of either type with probability $p / 2$ each, pushing its type; with probability $1 - p$ , close the top bracket when the stack is nonempty, or emit $e o s$ and stop when it is empty. This defines a probability law on finite words followed by $e o s$ and on infinite bracket streams. For a valid bracket prefix $x$ , let $o (x), c (x)$ and $h (x) = o (x) - c (x)$ denote its opening count, closing count and final stack height. Its cylinder probability is

w_{p} (x) = (p / 2)^{o (x)} (1 - p)^{c (x)} .

For every $k \geq 0$ , let $s_{p, k} = \sum_{∣ x ∣ = k} w_{p} (x)$ , summing over valid prefixes, and define $D_{p, k} (x) = w_{p} (x) / s_{p, k}$ . Thus $D_{p, k}$ conditions only on having emitted at least $k$ bracket tokens, without conditioning on eventual termination or exact total length. The target after a sampled prefix is its ordinary next token in the same process. At positive height its law assigns $p / 2$ to each opening type and $1 - p$ to the matching closing type.

For $k \geq 3$ , let $E_{k}$ consist of prefixes whose last three symbols are an opening of type $a$ , an opening of type $b$ , and the closing of type $b$ , with $a, b$ independently ranging over the two types. These prefixes have positive final height and end in a closing bracket. Flipping the opening type $a$ at position $k - 2$ is a fixed-point-free involution of $E_{k}$ into equal-mass pairs; paired prefixes differ only at this nonfinal position and their top unmatched opening types are opposite. Moreover,

D_{p, k} (E_{k}) = p^{2} (1 - p) \frac{s_{p, k - 3}}{s_{p, k}} \geq p^{2} (1 - p) > 0.

The finite-word mass of a typed Dyck word of length $2 m$ is $(p / 2)^{m} (1 - p)^{m + 1}$ . The total finite-word mass is $q_{p} = 1$ for $p \leq 1 / 2$ and $q_{p} = (1 - p) / p$ for $p > 1 / 2$ . After conditioning on eventual termination, the finite-word probability law and all its prefix laws are exactly those of the preceding process with parameter $a = p q_{p} = \min (p, 1 - p)$ ; consequently its survival-conditioned prefixes have the same pairing bound $a^{2} (1 - a)$ . Conditioning instead on exact word length $2 m$ yields the uniform law on typed Dyck words of that length, independently of $p$ ; that conditioning is different and does not retain the displayed next-token probabilities.

Statement references

Hahn, §6, Theorem 6 and footnote 4: PCFG and the positive-prefix-mass obligation

Facts & Assumptions

Given: The independent grammar choices, stack process, valid prefixes and conditioning conventions in the Statement.

Proof

1.1givenconstructalgebra

In a left-to-right grammar expansion, expanding the current $S$ nontrivially emits its opening bracket and leaves an inner $S$ , its matching closing bracket, and a following $S$ . Choosing $ϵ$ finishes the current $S$ and either emits the pending matching close or, when no close is pending, ends the word. Thus each token is generated by precisely the stack transition stated above. The remaining choices after any finite emitted prefix are fresh independent choices. This constructs the stream law directly, including on nonterminating samples. Each valid prefix uniquely specifies the transition choices so far: every opening requires its type choice and every closing requires an epsilon choice. Their product is $w_{p} (x)$ . In particular $s_{p, k}$ is the probability of reaching $k$ bracket tokens, is positive (all-open prefixes have positive probability), and is nonincreasing in $k$ . Conditioning on reaching $k$ does not constrain the fresh choice after the prefix.

1.2givenconstructalgebra

The grammar is unambiguous: a nonempty Dyck word has a unique first opening, its matching closing, and the resulting inside and following Dyck words, which recursively determine the derivation. A word with $m$ bracket pairs has $m$ nonempty choices and $m + 1$ epsilon leaves, proving its stated finite-word mass. To calculate total termination mass, the probabilities of trees having height below successive finite bounds start at $q_{0} = 0$ and satisfy $q_{j + 1} = 1 - p + p q_{j}^{2}$ . Their increasing limit is the probability of a finite tree: every finite binary tree has finite height, and an infinite finitely branching tree cannot have bounded height. The limit is the least fixed point in $[0, 1]$ , since iteration from zero stays below any nonnegative fixed point. The roots are $1$ and $(1 - p) / p$ , giving the stated $q_{p}$ . The stream is finite exactly when the derivation is finite: every nonempty expansion emits an opening and any derivation with only finitely many nonempty expansions has only finitely many nodes.

2.1step 1.1givenconstructalgebra

Each prefix in $E_{k}$ is uniquely $u a b \overline{b}$ , where $u$ is a valid prefix of length $k - 3$ . Such an extension is always valid, has height $h (u) + 1$ , and has the $a$ -opening as its top unmatched opening. Its cylinder weight is $w_{p} (u) (p / 2)^{2} (1 - p)$ . Summing the four choices of $a, b$ and then all $u$ gives $p^{2} (1 - p) s_{p, k - 3}$ . Divide by $s_{p, k}$ and use monotonicity from step 1.1 to obtain the bound. Flipping $a$ changes no count, leaves the suffix pattern valid, and changes only position $k - 2$ ; applying the flip twice restores the prefix. There are no fixed points, so its orbits are disjoint equal-mass pairs with swapped closing targets.

3.1step 1.1step 2.1step 1.2algebra∎

After a valid prefix of height $h$ , the left-to-right residual derivation contains exactly $h + 1$ still independent $S$ subtrees (and $h$ pending closing brackets). Its probability of eventual termination is therefore $q_{p}^{h + 1}$ . Consequently the termination-conditioned prefix cylinder is $w_{p} (x) q_{p}^{h (x) + 1} / q_{p} = (p q_{p} / 2)^{o (x)} ((1 - p) / q_{p})^{c (x)}$ . The fixed-point equation gives $(1 - p) / q_{p} = 1 - p q_{p}$ . This is exactly $w_{a} (x)$ with $a = p q_{p}$ . The finite-word laws likewise agree, either by the same calculation including the final epsilon or directly from step 1.2. Applying step 2.1 with $a$ gives its pairing bound. Finally all typed Dyck words of a fixed length have the same mass by step 1.2 and there are finitely many of them, proving the uniform exact-length law and the asserted distinction of conditioning.

Used by

Hard and soft attention limits for formal-language prediction Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Hahn, Theoretical Limitations of Self-Attention in Neural Sequence Models, §6, Theorem 6 and footnote 4 (standard reference, not scraped)