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.
Deterministic context-free languages are unambiguous
Statement
Every deterministic context-free language has an unambiguous context-free grammar.
Facts & Assumptions
Given: A deterministic context-free language .
By Deterministic pushdown automata and deterministic context-free languages, some DPDA recognizes .
By A DPDA has at most one computation on each input, computations of a DPDA on one marked input are linearly ordered by extension and have at most one maximal computation.
By If a PDA has at most one accepting computation on each word, the standard PDA-to-CFG construction is unambiguous, a PDA with at most one accepting computation on each word yields an unambiguous fragment-variable grammar for the same language.
Proof
Choose a DPDA recognizing by [L1].
Form an equivalent DPDA that records whether the endmarker has been consumed. Before it simulates in a pre-endmarker copy of the state set; a transition consuming enters the post-endmarker copy; and all subsequent -moves remain in that copy. Declare a post-endmarker copy accepting exactly when its underlying state lies in , and delete every outgoing move from those accepting copies. This preserves determinism by [L1]: it only duplicates states and removes moves.
The machine recognizes the same language as . Indeed, an accepting computation of has consumed the marked input and hence reaches a post-endmarker accepting copy in ; conversely, every accepting copy projects to an accepting configuration of . Halting at the first such copy does not change whether that configuration is reachable.
Every accepting computation of is maximal because its accepting states have no outgoing moves. By [L2], there is therefore at most one accepting computation on each marked input.
Applying [L3] to yields an unambiguous context-free grammar generating its language, which is by step 3.1. Therefore every deterministic context-free language is unambiguous.
Depends on
- Ambiguous grammars, unambiguous grammars, and inherently ambiguous languages
- Deterministic pushdown automata and deterministic context-free languages
- A DPDA has at most one computation on each input
- If a PDA has at most one accepting computation on each word, the standard PDA-to-CFG construction is unambiguous
Used by
Dependency tree · two levels
10 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)
- Dexter C. Kozen, Automata and Computability (standard reference, not scraped)
- Alfred V. Aho, COMS W3261 Lecture 8: Pushdown Automata (standard reference, not scraped)
- Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation (standard reference, not scraped)