Grammars, parsing and pushdown automata

Grammar basics and derivation forests, Chomsky and Greibach normal forms, ε- and unit-production elimination, CYK and Earley recognizers, leftmost derivations and (inherent) ambiguity, pushdown automata, deterministic context-free languages, and the grammar–PDA equivalence.

• Context-free grammars
• Ambiguity of context-free grammars
• Earley parser
• Elimination of empty and unit productions
• Chomsky normal form
• CYK algorithm
• Greibach normal form
• Pushdown automata
• Pushdown automata and context-free grammars
• Deterministic context-free languages

TheoremRegular languages over a finite alphabet are context-free#✓fully proved

Over a finite alphabet, every regular language is context-free.

Finiteness of the alphabet is necessary: a grammar has finitely many productions, hence mentions only finitely many terminal symbols, but a DFA over an infinite alphabet may accept every one-letter word.

theorem IsRegular.isContextFree [Finite T] {L : Language T} (hL : L.IsRegular) :
    L.IsContextFree

Uses 5

Proof usesValuation of a grammar · Concatenating derivations · Interpretation of a sentential form · Interpretation of a grammar symbol · Valuations bound the language of a grammar

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.