Elimination of empty and unit productions

TheoremNo empty words without empty productions#✓fully proved

In a context-free grammar in which no production has an empty right-hand side, every nonempty sentential form yields only nonempty words.

theorem Yields.ne_nil_of_forall_output_ne_nil {G : ContextFreeGrammar T}
    (hG : ∀ r ∈ G.rules, r.output ≠ []) :
    ∀ {α : List (Symbol T G.NT)} {w : List T}, Yields G α w → α ≠ [] →
      w ≠ []

Uses 1 · Used by 2

Statement usesYield of a sentential form

Used byPumping lemma for context-free languages · The \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\)

DefinitionNullable nonterminal#✓fully proved

A nonterminal \(A\) of a context-free grammar \(g\) is nullable when \(g\) derives the empty word from \(A\).

def Nullable (g : ContextFreeGrammar T) (A : g.NT) :
    Prop :=
  [] ∈ languageFrom g A

Uses 1 · Used by 7

Statement usesLanguage generated from a nonterminal

Used byThe \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\) · Deleting nullable nonterminals shrinks the denoted language · Soundness of ε-production elimination · Nullable deletions · Completeness of eliminating empty productions · Computed deletions agree with nullable deletions · The nullable nonterminals are computed

DefinitionNullable deletions#✓fully proved

For a context-free grammar \(g\) and a sentential form \(u\), the nullable deletions of \(u\) are the forms obtained from \(u\) by deleting any selection of occurrences of nullable nonterminals, possibly none and possibly all, keeping the remaining symbols in order. They form a finite set.

noncomputable def nullableDeletions (g : ContextFreeGrammar T) :
    List (Symbol T g.NT) → Finset (List (Symbol T g.NT))
  | [] => {[]}
  | Symbol.terminal a :: u =>
    (nullableDeletions g u).image (Symbol.terminal a :: ·)
  | Symbol.nonterminal A :: u =>
    (nullableDeletions g u).image (Symbol.nonterminal A :: ·) ∪
      (if Nullable g A then nullableDeletions g u else ∅)

Uses 1 · Used by 11

Statement usesNullable nonterminal

Used byProductions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\) · Elimination of \(\varepsilon\)-productions · The \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\) · The \(\varepsilon\)-eliminated grammar has no empty productions · Deleting nullable nonterminals shrinks the denoted language · Soundness of ε-production elimination · Productions of the ε-free grammar · Completeness of eliminating empty productions · Computable removal of empty productions agrees with the classical one · Productions of the computable removal of empty productions · Computed deletions agree with nullable deletions

TheoremDeleting nullable nonterminals shrinks the denoted language#✓fully proved

Let \(g\) be a context-free grammar and \(V\) an assignment of a language \(V(A)\) to each nonterminal \(A\) of \(g\) such that the empty word belongs to \(V(A)\) whenever \(A\) is nullable (derives the empty word in \(g\)). If a sentential form \(\alpha'\) is obtained from a sentential form \(u\) by deleting some occurrences of nullable nonterminals, then the language denoted by \(\alpha'\) under \(V\) is contained in the language denoted by \(u\) under \(V\).

theorem evalForm_le_of_mem_nullableDeletions {V : g.NT → Language T}
    (hV : ∀ A, Nullable g A → [] ∈ V A) :
    ∀ {u α' : List (Symbol T g.NT)}, α' ∈ nullableDeletions g u →
      evalForm V α' ≤ evalForm V u

Uses 4 · Used by 1

Statement usesNullable nonterminal · Interpretation of a sentential form · Nullable deletions

Proof usesInterpretation of a grammar symbol

Used bySoundness of ε-production elimination

DefinitionElimination of \(\varepsilon\)-productions#✓fully proved

For a context-free grammar \(g\), the grammar obtained from \(g\) by eliminating \(\varepsilon\)-productions has the same nonterminals and the same initial nonterminal as \(g\). Its productions are the productions \(A \to \alpha'\) such that \(g\) has a production \(A \to \alpha\), the form \(\alpha'\) is obtained from \(\alpha\) by deleting some (possibly no) occurrences of nullable nonterminals (those deriving the empty word in \(g\)), and \(\alpha'\) is nonempty.

noncomputable def epsGrammar (g : ContextFreeGrammar T) :
    ContextFreeGrammar T where
  NT := g.NT
  initial := g.initial
  rules := g.rules.biUnion fun r =>
    ((nullableDeletions g r.output).filter (· ≠ [])).image
      (fun α => ⟨r.input, α⟩)

Uses 1 · Used by 11

Statement usesNullable deletions

Used byProductions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\) · The \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\) · The \(\varepsilon\)-eliminated grammar has no empty productions · Existence of reduced grammars · Soundness of ε-production elimination · Productions of the ε-free grammar · Completeness of eliminating empty productions · Computable removal of empty productions agrees with the classical one · The reduced grammar has no empty and no unit productions · Removing empty productions drops only the empty word · Productions of the computable removal of empty productions

TheoremProductions of the ε-free grammar#✓fully proved

Let \(g\) be a context-free grammar with a production \(A \to u\), and let \(\alpha\) be a nonempty form obtained from \(u\) by deleting some (possibly no) occurrences of nullable nonterminals. Then \(A \to \alpha\) is a production of the grammar obtained from \(g\) by eliminating ε-productions.

theorem mem_epsGrammar_rules {A : g.NT} {u α : List (Symbol T g.NT)}
    (hr : (⟨A, u⟩ : ContextFreeRule T g.NT) ∈ g.rules)
    (hα : α ∈ nullableDeletions g u) (hne : α ≠ []) :
    (⟨A, α⟩ : ContextFreeRule T g.NT) ∈ (epsGrammar g).rules

Uses 2 · Used by 2

Statement usesElimination of \(\varepsilon\)-productions · Nullable deletions

Used byCompleteness of eliminating empty productions · Productions of the computable removal of empty productions

TheoremProductions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\)#✓fully proved

Let \(g\) be a context-free grammar. Every production \(A \to \alpha'\) of the grammar obtained from \(g\) by eliminating \(\varepsilon\)-productions arises from a production \(A \to \alpha\) of \(g\) with the same left-hand side \(A\), such that \(\alpha'\) is obtained from \(\alpha\) by deleting some occurrences of nullable nonterminals and \(\alpha'\) is nonempty.

theorem cases_of_mem_epsGrammar_rules {r' : ContextFreeRule T g.NT}
    (hr : r' ∈ (epsGrammar g).rules) :
    ∃ r ∈ g.rules, r'.input = r.input ∧ r'.output ∈ nullableDeletions g r.output ∧
      r'.output ≠ []

Uses 2 · Used by 3

Statement usesElimination of \(\varepsilon\)-productions · Nullable deletions

Used byThe \(\varepsilon\)-eliminated grammar has no empty productions · Soundness of ε-production elimination · Productions of the computable removal of empty productions

TheoremThe \(\varepsilon\)-eliminated grammar has no empty productions#✓fully proved

For a context-free grammar \(g\), no production of the grammar obtained from \(g\) by eliminating \(\varepsilon\)-productions has empty right-hand side.

theorem epsGrammar_output_ne_nil {r : ContextFreeRule T (epsGrammar g).NT}
    (hr : r ∈ (epsGrammar g).rules) : r.output ≠ []

Uses 3 · Used by 3

Statement usesElimination of \(\varepsilon\)-productions

Proof usesProductions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\) · Nullable deletions

Used byThe \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\) · Existence of reduced grammars · The reduced grammar has no empty and no unit productions

TheoremSoundness of ε-production elimination#✓fully proved

Let \(g\) be a context-free grammar and, for each nonterminal \(A\), let \(L_g(A)\) be the language of words \(g\) derives from \(A\). Then \(L_g\) is a valuation of the grammar obtained from \(g\) by eliminating ε-productions: for every production \(A \to \alpha\) of that grammar, the language of \(\alpha\) under \(L_g\) (the concatenation of the languages of its symbols, a terminal \(a\) denoting \(\{a\}\)) is contained in \(L_g(A)\).

theorem isValuation_epsGrammar :
    IsValuation (epsGrammar g) (languageFrom g)

Uses 9 · Used by 1

Statement usesValuation of a grammar · Elimination of \(\varepsilon\)-productions · Language generated from a nonterminal

Proof usesNullable nonterminal · Productions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\) · Interpretation of a sentential form · Deleting nullable nonterminals shrinks the denoted language · The languages generated from each nonterminal form a valuation · Nullable deletions

Used byThe \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\)

TheoremCompleteness of eliminating empty productions#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) of \(g\) yields a terminal word \(w\) in \(g\), then some form \(\alpha'\) obtained from \(\alpha\) by deleting some occurrences of nullable nonterminals yields \(w\) in the grammar obtained from \(g\) by eliminating \(\varepsilon\)-productions, and \(w\) is empty if \(\alpha'\) is empty.

theorem yields_epsGrammar_of_yields :
    ∀ {α : List (Symbol T g.NT)} {w : List T}, Yields g α w →
      ∃ α' ∈ nullableDeletions g α, Yields (epsGrammar g) α' w ∧
        (α' = [] → w = [])

Uses 8 · Used by 1

Statement usesYield of a sentential form · Elimination of \(\varepsilon\)-productions · Nullable deletions

Proof usesNullable nonterminal · Language generated from a nonterminal · Productions of the ε-free grammar · Yields coincide with derivations of terminal words · Yield through one production

Used byThe \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\)

TheoremThe \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\)#✓fully proved

For a context-free grammar \(g\) and every word \(w\) over its terminals, \(w\) is generated by the grammar obtained from \(g\) by eliminating \(\varepsilon\)-productions if and only if \(w\) is generated by \(g\) and \(w\) is nonempty.

theorem epsGrammar_language {w : List T} :
    w ∈ (epsGrammar g).language ↔ w ∈ g.language ∧ w ≠ []

Uses 11 · Used by 2

Statement usesElimination of \(\varepsilon\)-productions

Proof usesNullable nonterminal · Yield of a sentential form · No empty words without empty productions · The \(\varepsilon\)-eliminated grammar has no empty productions · Soundness of ε-production elimination · Language generated from a nonterminal · Valuations bound the language of a grammar · Language membership through yields · Nullable deletions · Completeness of eliminating empty productions

Used byExistence of reduced grammars · Removing empty productions drops only the empty word

DefinitionReachability by unit productions#✓fully proved

Let \(g\) be a context-free grammar. A nonterminal \(A\) of \(g\) reaches a nonterminal \(B\) by unit productions when there is a chain \(A = A_0, A_1, \dots, A_n = B\) with \(n \ge 0\) such that each \(A_{i-1} \to A_i\) is a production of \(g\). In particular, every nonterminal reaches itself.

def UnitSteps (g : ContextFreeGrammar T) : g.NT → g.NT → Prop :=
  Relation.ReflTransGen
    (fun A B => (⟨A, [Symbol.nonterminal B]⟩ : ContextFreeRule T g.NT) ∈
      g.rules)

Used by 13

Used byProductions of the unit-eliminated grammar come from non-unit productions of \(g\) · Existence of reduced grammars · Soundness of unit-production elimination · Languages along unit chains · Unit chains start at mentioned nonterminals · Productions of the unit-free grammar · Eliminating unit productions · Eliminating unit productions leaves no unit production · Eliminating unit productions creates no new outputs · Eliminating unit productions keeps every yield · Productions of the encoded unit elimination · Unit reachability is computed · The encoded unit elimination denotes the unit-eliminated grammar

DefinitionUnit output#✓fully proved

A sentential form is a unit output when it consists of a single nonterminal.

def IsUnitOutput {N : Type*} (α : List (Symbol T N)) : Prop :=
  ∃ B, α = [Symbol.nonterminal B]

Used by 18

Used byPumping lemma for context-free languages · Binarization of a reduced grammar is in Chomsky normal form · Binarization adds no words · Binarization preserves the language · Binarization has no empty productions · Chomsky normal form theorem · Productions of the unit-eliminated grammar come from non-unit productions of \(g\) · Existence of reduced grammars · Reduced grammars · Soundness of unit-production elimination · Productions of the unit-free grammar · Eliminating unit productions · Eliminating unit productions leaves no unit production · Eliminating unit productions creates no new outputs · Eliminating unit productions keeps every yield · The reduced grammar has no empty and no unit productions · Productions of the encoded unit elimination · The encoded unit elimination denotes the unit-eliminated grammar

DefinitionNonterminals of a sentential form#✓fully proved

For a sentential form \(u\), a finite word of terminal and nonterminal symbols, the nonterminals of \(u\) form the finite set of all nonterminals that occur in \(u\).

noncomputable def formNTs {N : Type*} (u : List (Symbol T N)) : Finset N :=
  (u.filterMap fun s => match s with
    | Symbol.terminal _ => none
    | Symbol.nonterminal A => some A).toFinset

Used by 6

Used byPumping lemma for context-free languages · Set of nonterminals mentioned by a grammar · Unit chains start at mentioned nonterminals · Productions of the unit-free grammar · Eliminating unit productions keeps every yield · Productions of the encoded unit elimination

DefinitionSet of nonterminals mentioned by a grammar#✓fully proved

The nonterminals mentioned by a context-free grammar \(g\) form the finite set consisting of the initial nonterminal of \(g\), the left-hand side of every production of \(g\), and every nonterminal occurring in the right-hand side of a production of \(g\).

noncomputable def grammarNTs (g : ContextFreeGrammar T) : Finset g.NT :=
  insert g.initial
    (g.rules.biUnion fun r => insert r.input (formNTs r.output))

Uses 1 · Used by 8

Statement usesNonterminals of a sentential form

Used byPumping lemma for context-free languages · Productions of the unit-eliminated grammar come from non-unit productions of \(g\) · Unit chains start at mentioned nonterminals · Productions of the unit-free grammar · Eliminating unit productions · Eliminating unit productions keeps every yield · Productions of the encoded unit elimination · The encoded unit elimination denotes the unit-eliminated grammar

TheoremUnit chains start at mentioned nonterminals#✓fully proved

Let \(g\) be a context-free grammar and let \(B\) be reachable from \(A\) by a chain of zero or more unit productions of \(g\). If \(B\) is the left-hand side of some production of \(g\), then \(A\) is among the nonterminals mentioned by \(g\) (its initial nonterminal, the left-hand sides of its productions, and the nonterminals in their right-hand sides).

theorem mem_grammarNTs_of_unitSteps {A B : g.NT}
    (hsteps : UnitSteps g A B)
    (hB : ∃ α, (⟨B, α⟩ : ContextFreeRule T g.NT) ∈ g.rules) :
    A ∈ grammarNTs g

Uses 3 · Used by 2

Statement usesReachability by unit productions · Set of nonterminals mentioned by a grammar

Proof usesNonterminals of a sentential form

Used byEliminating unit productions keeps every yield · Productions of the encoded unit elimination

DefinitionEliminating unit productions#✓fully proved

A unit production is one whose output is a single nonterminal. For a context-free grammar \(g\), the grammar obtained by eliminating unit productions has the same nonterminals and the same start symbol as \(g\). Its productions are the \(A \to \alpha\) such that \(A\) is a nonterminal mentioned by \(g\) (its start symbol or one occurring in a production of \(g\)), \(g\) has a production \(B \to \alpha\) that is not a unit production, and \(A\) reaches \(B\) by a chain of zero or more unit productions of \(g\).

noncomputable def unitGrammar (g : ContextFreeGrammar T) :
    ContextFreeGrammar T where
  NT := g.NT
  initial := g.initial
  rules := (grammarNTs g).biUnion fun A => (grammarNTs g).biUnion fun B =>
    (g.rules.filter fun r =>
      r.input = B ∧ ¬ IsUnitOutput r.output ∧ UnitSteps g A B).image
        (fun r => ⟨A, r.output⟩)

Uses 3 · Used by 12

Statement usesUnit output · Reachability by unit productions · Set of nonterminals mentioned by a grammar

Used byProductions of the unit-eliminated grammar come from non-unit productions of \(g\) · Existence of reduced grammars · Soundness of unit-production elimination · Productions of the unit-free grammar · Eliminating unit productions preserves the language · Eliminating unit productions leaves no unit production · Eliminating unit productions creates no new outputs · Eliminating unit productions keeps every yield · The reduced grammar has no empty and no unit productions · The reduced grammar generates the language minus the empty word · Productions of the encoded unit elimination · The encoded unit elimination denotes the unit-eliminated grammar

TheoremProductions of the unit-free grammar#✓fully proved

Let \(g\) be a context-free grammar, let \(B\) be reachable from \(A\) by a chain of zero or more unit productions of \(g\), and let \(B \to \beta\) be a production of \(g\) whose right-hand side \(\beta\) is not a single nonterminal. If \(A\) is among the nonterminals mentioned by \(g\), then \(A \to \beta\) is a production of the grammar obtained from \(g\) by eliminating unit productions.

theorem mem_unitGrammar_rules {A B : g.NT} {r : ContextFreeRule T g.NT}
    (hsteps : UnitSteps g A B) (hr : r ∈ g.rules) (hinput : r.input = B)
    (hunit : ¬ IsUnitOutput r.output) (hA : A ∈ grammarNTs g) :
    (⟨A, r.output⟩ : ContextFreeRule T g.NT) ∈ (unitGrammar g).rules

Uses 5 · Used by 2

Statement usesUnit output · Reachability by unit productions · Set of nonterminals mentioned by a grammar · Eliminating unit productions

Proof usesNonterminals of a sentential form

Used byEliminating unit productions keeps every yield · Productions of the encoded unit elimination

TheoremProductions of the unit-eliminated grammar come from non-unit productions of \(g\)#✓fully proved

Let \(g\) be a context-free grammar. For every production \(A \to \beta\) of the grammar obtained from \(g\) by eliminating unit productions, there are a nonterminal \(B\) and a production \(B \to \beta\) of \(g\) such that \(\beta\) is not a single nonterminal and \(B\) is reachable from \(A\) by a possibly empty chain of unit productions of \(g\).

theorem cases_of_mem_unitGrammar_rules {r' : ContextFreeRule T g.NT}
    (hr : r' ∈ (unitGrammar g).rules) :
    ∃ (B : g.NT) (r : ContextFreeRule T g.NT), r ∈ g.rules ∧
      r.input = B ∧ ¬ IsUnitOutput r.output ∧ UnitSteps g r'.input B ∧
      r'.output = r.output

Uses 4 · Used by 5

Statement usesUnit output · Reachability by unit productions · Eliminating unit productions

Proof usesSet of nonterminals mentioned by a grammar

Used byExistence of reduced grammars · Soundness of unit-production elimination · Eliminating unit productions leaves no unit production · Eliminating unit productions creates no new outputs · Productions of the encoded unit elimination

TheoremEliminating unit productions leaves no unit production#✓fully proved

For every context-free grammar \(g\), no production of the grammar obtained from \(g\) by eliminating unit productions has an output consisting of a single nonterminal.

theorem unitGrammar_not_isUnitOutput {r : ContextFreeRule T g.NT}
    (hr : r ∈ (unitGrammar g).rules) : ¬ IsUnitOutput r.output

Uses 4 · Used by 2

Statement usesUnit output · Eliminating unit productions

Proof usesReachability by unit productions · Productions of the unit-eliminated grammar come from non-unit productions of \(g\)

Used byExistence of reduced grammars · The reduced grammar has no empty and no unit productions

TheoremEliminating unit productions creates no new outputs#✓fully proved

Let \(g\) be a context-free grammar. For every production of the grammar obtained from \(g\) by eliminating unit productions, some production of \(g\) has the same output.

In particular, empty outputs are not created.

theorem unitGrammar_output_of_mem {r' : ContextFreeRule T g.NT}
    (hr : r' ∈ (unitGrammar g).rules) :
    ∃ r ∈ g.rules, r.output = r'.output

Uses 4 · Used by 1

Statement usesEliminating unit productions

Proof usesUnit output · Reachability by unit productions · Productions of the unit-eliminated grammar come from non-unit productions of \(g\)

Used byThe reduced grammar has no empty and no unit productions

TheoremLanguages along unit chains#✓fully proved

Let \(g\) be a context-free grammar and, for each nonterminal \(A\), let \(L_g(A)\) be the language of words \(g\) derives from \(A\). If \(B\) is reachable from \(A\) by a chain of zero or more unit productions \(A \to A_1 \to \dots \to B\) of \(g\), then \(L_g(B) \subseteq L_g(A)\).

theorem languageFrom_le_of_unitSteps {A B : g.NT}
    (hsteps : UnitSteps g A B) : languageFrom g B ≤ languageFrom g A

Uses 4 · Used by 1

Statement usesReachability by unit productions · Language generated from a nonterminal

Proof usesInterpretation of a sentential form · The languages generated from each nonterminal form a valuation

Used bySoundness of unit-production elimination

TheoremSoundness of unit-production elimination#✓fully proved

Let \(g\) be a context-free grammar and, for each nonterminal \(A\), let \(L_g(A)\) be the language of words \(g\) derives from \(A\). Then \(L_g\) is a valuation of the grammar obtained from \(g\) by eliminating unit productions: for every production \(A \to \alpha\) of that grammar, the language of \(\alpha\) under \(L_g\) (the concatenation of the languages of its symbols, a terminal \(a\) denoting \(\{a\}\)) is contained in \(L_g(A)\).

theorem isValuation_unitGrammar :
    IsValuation (unitGrammar g) (languageFrom g)

Uses 9 · Used by 1

Statement usesValuation of a grammar · Language generated from a nonterminal · Eliminating unit productions

Proof usesUnit output · Reachability by unit productions · Productions of the unit-eliminated grammar come from non-unit productions of \(g\) · Interpretation of a sentential form · The languages generated from each nonterminal form a valuation · Languages along unit chains

Used byEliminating unit productions preserves the language

TheoremEliminating unit productions keeps every yield#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) of \(g\) yields a terminal word \(w\) in \(g\), then \(\alpha\) yields \(w\) in the grammar obtained from \(g\) by eliminating unit productions.

theorem yields_unitGrammar_of_yields {α : List (Symbol T g.NT)}
    {w : List T} (h : Yields g α w) : Yields (unitGrammar g) α w

Uses 10 · Used by 1

Statement usesYield of a sentential form · Eliminating unit productions

Proof usesUnit output · Reachability by unit productions · Concatenation of yields · Nonterminals of a sentential form · Set of nonterminals mentioned by a grammar · Unit chains start at mentioned nonterminals · Productions of the unit-free grammar · Yield through one production

Used byEliminating unit productions preserves the language

TheoremEliminating unit productions preserves the language#✓fully proved

For every context-free grammar \(g\), the grammar obtained from \(g\) by eliminating unit productions generates the same language as \(g\).

theorem unitGrammar_language : (unitGrammar g).language = g.language

Uses 7 · Used by 2

Statement usesEliminating unit productions

Proof usesYield of a sentential form · Soundness of unit-production elimination · Language generated from a nonterminal · Valuations bound the language of a grammar · Language membership through yields · Eliminating unit productions keeps every yield

Used byExistence of reduced grammars · The reduced grammar generates the language minus the empty word

DefinitionReduced grammars#✓fully proved

A context-free grammar is reduced when no production has empty right-hand side and no production has a single nonterminal as its right-hand side.

This is the sense used for the pumping lemma and normal forms. It does not assert that every nonterminal is reachable or productive.

def IsReduced (g : ContextFreeGrammar T) : Prop :=
  (∀ r ∈ g.rules, r.output ≠ []) ∧
    ∀ r ∈ g.rules, ¬ IsUnitOutput r.output

Uses 1 · Used by 7

Statement usesUnit output

Used byPumping lemma for context-free languages · Binarization of a reduced grammar is in Chomsky normal form · Binarization adds no words · Binarization preserves the language · Binarization has no empty productions · Chomsky normal form theorem · The reduced grammar has no empty and no unit productions

TheoremExistence of reduced grammars#✓fully proved

For every context-free grammar \(g\) over an alphabet \(T\) there is a context-free grammar \(g'\) over \(T\) that generates exactly the nonempty words generated by \(g\), such that no production of \(g'\) has empty right-hand side and no production of \(g'\) has a single nonterminal as its right-hand side.

theorem exists_reduced_grammar (g : ContextFreeGrammar T) :
    ∃ g' : ContextFreeGrammar T,
      (∀ w, w ∈ g'.language ↔ w ∈ g.language ∧ w ≠ []) ∧
      (∀ r ∈ g'.rules, r.output ≠ []) ∧
      (∀ r ∈ g'.rules, ¬ IsUnitOutput r.output)

Uses 9 · Used by 2

Statement usesUnit output

Proof usesReachability by unit productions · Productions of the unit-eliminated grammar come from non-unit productions of \(g\) · Elimination of \(\varepsilon\)-productions · The \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\) · The \(\varepsilon\)-eliminated grammar has no empty productions · Eliminating unit productions · Eliminating unit productions preserves the language · Eliminating unit productions leaves no unit production

Used byPumping lemma for context-free languages · Chomsky normal form theorem

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.