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.
Ogden's lemma
Statement
If is a context-free language, then there exists an integer such that for every word and every choice of at least marked positions in , there is a decomposition that is -admissible with respect to the marked positions and satisfies
Facts & Assumptions
Given: A context-free language .
By Marked positions and admissible Ogden decompositions, a -admissible decomposition is one in which contains at least one marked position while contains at most marked positions.
By The language generated by a CFG, there exists a context-free grammar generating .
By Every context-free language has an equivalent grammar in Chomsky normal form, that grammar may be replaced by an equivalent grammar in Chomsky normal form.
By Derivations and parse trees correspond, every word in the language of a CFG is the yield of some parse tree for that grammar.
By Parse trees and their yields, a parse tree records the production used at each internal node and its yield is read from the terminal leaves from left to right.
Proof
Choose a context-free grammar with by [L2], then replace it by an equivalent Chomsky-normal-form grammar by [L3]. Set . Let and mark at least positions of . Because , the word is nonempty, so by [L4] fix a parse tree for in the CNF grammar .
Starting at the root of , build a path to a marked leaf by always moving to a child whose subtree contains the larger number of marked positions; when both children contain marked positions, choose one of the heavier children. Call such a node a branch point. Each time the path passes through a branch point, the chosen child still contains at least half of the marked positions seen at that node. Therefore, if there were at most branch points on the path, the terminal leaf at the end would still lie below at least marked positions, impossible for one leaf. So the path contains at least branch points.
Among the last branch points on that path, choose two with the same variable label , with the upper one above the lower one. Let the lower -subtree yield , and let the material in the upper -subtree to the left and right of the lower subtree yield and , so that the whole word is . The upper branch point has marked material outside the lower subtree, so the concatenation contains a marked position. Also, if the upper -subtree contained more than marked positions, then repeating the branch-point-halving argument inside that subtree would produce more than branch points below it on the chosen path, contradicting that we selected the upper among the last branch points. Hence contains at most marked positions. By [L1], the decomposition is -admissible.
The upper occurrence of derives the lower one by a derivation segment , and the lower subtree derives . Repeating or deleting that segment while keeping the rest of the parse tree fixed produces derivations of for every . Therefore every such word lies in .
Hence the integer satisfies Ogden's lemma for .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)