Chomsky normal form

DefinitionChomsky normal form#✓fully proved

A grammar is in Chomsky normal form when every production has output either two nonterminals, a single terminal, or the empty word with the initial nonterminal on the left; and either the initial nonterminal occurs in no output (so an empty production cannot leak the empty word to other nonterminals) or there are no empty outputs at all.

def IsChomskyNormalForm (g : ContextFreeGrammar T) : Prop :=
  (∀ r ∈ g.rules,
    (∃ B C, r.output = [Symbol.nonterminal B, Symbol.nonterminal C]) ∨
    (∃ a, r.output = [Symbol.terminal a]) ∨
    (r.output = [] ∧ r.input = g.initial)) ∧
  ((∀ r ∈ g.rules, Symbol.nonterminal g.initial ∉ r.output) ∨
    ∀ r ∈ g.rules, r.output ≠ [])

Used by 16

Used byBinarization of a reduced grammar is in Chomsky normal form · Adding a fresh start symbol preserves Chomsky normal form · Chomsky normal form theorem · Chomsky normal form for context-free languages · Correctness of one indexed CYK cell · Indexed CYK agrees with the list-table CYK recognizer · Correctness of the indexed CYK recognizer · Correctness of the completed indexed CYK table · Correctness of indexed CYK on encoded grammars · Correctness of the CYK recognizer · Correctness of the CYK table · Forms yielding the empty word under Chomsky normal form · The CYK step · Correctness of the CYK recurrence · Nonterminals in outputs have no empty production · Shape of yields under Chomsky normal form

DefinitionTerminals of a grammar#✓fully proved

For a context-free grammar \(G\), the list of terminals occurring in the outputs of its productions: going through the productions of \(G\) in a fixed but unspecified order, list the terminals of each output from left to right. A terminal may appear more than once.

noncomputable def grammarTerminals (g : ContextFreeGrammar T) : List T :=
  g.rules.toList.flatMap fun r => r.output.filterMap fun s =>
    match s with
    | .terminal a => some a
    | .nonterminal _ => none

Used by 13

Used byLetter numbering for the substitution grammar · Letter decoding for the substitution grammar · Derivations keep the terminals among those of the grammar · Productions of the substitution grammar · Context-free languages are closed under substitution by context-free languages · Binarization of a grammar · Binarization of a reduced grammar is in Chomsky normal form · Binarization adds no words · Binarization preserves the language · Binarization has no empty productions · Head of a binarized output · Decoding basic nonterminals of the binarized grammar · Encoding symbols as basic nonterminals of the binarized grammar

DefinitionEncoding symbols as basic nonterminals of the binarized grammar#✓fully proved

Let \(G\) be a context-free grammar with nonterminals \(N\), and let \(t_0, \dots, t_{k-1}\) be the list of terminals occurring in the production outputs of \(G\). This map sends a symbol of \(G\) to an element of \(N \sqcup \mathbb{N}\): a nonterminal \(A\) goes to \(A\), and a terminal \(a\) goes to the least index \(i\) with \(t_i = a\), or to \(k\) if \(a\) does not occur in the list.

noncomputable def toCnfNT : Symbol T g.NT → g.NT ⊕ ℕ
  | .terminal a => .inr ((grammarTerminals g).idxOf a)
  | .nonterminal A => .inl A

Uses 1 · Used by 5

Statement usesTerminals of a grammar

Used byBinarization of a grammar · Binarization of a reduced grammar is in Chomsky normal form · Binarization adds no words · Binarization preserves the language · Binarization has no empty productions

DefinitionDecoding basic nonterminals of the binarized grammar#✓fully proved

Let \(G\) be a context-free grammar with nonterminals \(N\) and initial nonterminal \(S\), and let \(t_0, \dots, t_{k-1}\) be the list of terminals occurring in the production outputs of \(G\). This map sends an element of \(N \sqcup \mathbb{N}\) (a basic nonterminal of the binarized grammar) to a symbol of \(G\): a nonterminal \(A \in N\) goes to \(A\), an index \(i < k\) goes to the terminal \(t_i\), and an index \(i \ge k\) goes to the nonterminal \(S\).

Indices \(i \ge k\) never arise from encoding nonterminals of \(G\) or terminals occurring in the production outputs of \(G\).

noncomputable def fromCnfNT : g.NT ⊕ ℕ → Symbol T g.NT
  | .inl A => .nonterminal A
  | .inr i => match (grammarTerminals g)[i]? with
    | some a => .terminal a
    | none => .nonterminal g.initial

Uses 1 · Used by 2

Statement usesTerminals of a grammar

Used byBinarization adds no words · Valuation of the binarized grammar by yields

DefinitionHead of a binarized output#✓fully proved

Let \(g\) be a context-free grammar and let \(a_0, a_1, \dots\) be its list of terminals occurring in production outputs. For a list \(\sigma\) of basic symbols (each a nonterminal of \(g\) or a natural number, a terminal wrapper), the head \(h(\sigma)\) is the following form over the nonterminals of the binarized grammar (basic symbols and chain nonterminals \(\langle\tau\rangle\) for lists \(\tau\) of basic symbols): \(h(XY) = XY\) for two basic symbols \(X, Y\); \(h(XYZ\tau) = X\langle YZ\tau\rangle\) for basic symbols \(X, Y, Z\) and a list \(\tau\); \(h(i) = a_i\) for a single natural number \(i\) less than the length of the list; and \(h(\sigma)\) is empty in every other case (the empty list, a single nonterminal of \(g\), or a single out-of-range index).

noncomputable def cnfHead : List (g.NT ⊕ ℕ) →
    List (Symbol T ((g.NT ⊕ ℕ) ⊕ List (g.NT ⊕ ℕ)))
  | [] => []
  | [B] => match B with
    | .inr i => match (grammarTerminals g)[i]? with
      | some a => [Symbol.terminal a]
      | none => []
    | .inl _ => []
  | [B, C] => [Symbol.nonterminal (.inl B), Symbol.nonterminal (.inl C)]
  | B :: C :: D :: σ =>
    [Symbol.nonterminal (.inl B),
      Symbol.nonterminal (.inr (C :: D :: σ))]

Uses 1 · Used by 5

Statement usesTerminals of a grammar

Used byBinarization of a grammar · Binarization of a reduced grammar is in Chomsky normal form · Binarization adds no words · Binarization preserves the language · Binarization has no empty productions

DefinitionBinarization of a grammar#✓fully proved

Let \(g\) be a context-free grammar with nonterminals \(N\) and initial nonterminal \(S\), and let \(t_0, \dots, t_{k-1}\) be the list of terminals occurring in the production outputs of \(g\). Encode each symbol of a production output of \(g\) as a basic symbol in \(N \sqcup \mathbb{N}\): a nonterminal \(A\) as \(A\), and a terminal \(a\) as the least index \(i\) with \(t_i = a\). The binarized grammar of \(g\) has as nonterminals the basic symbols together with a chain nonterminal \(\langle\tau\rangle\) for every list \(\tau\) of basic symbols, and its initial nonterminal is \(S\). For a list \(\sigma\) of basic symbols, its head \(h(\sigma)\) is defined by \(h(XY) = XY\) and \(h(XYZ\tau) = X\langle YZ\tau\rangle\) for basic symbols \(X, Y, Z\) and a list \(\tau\), \(h(i) = t_i\) for a single index \(i < k\), and \(h(\sigma)\) empty in every other case. For every production \(A \to \alpha\) of \(g\), with \(\sigma\) the encoding of \(\alpha\) symbol by symbol, the binarized grammar has the production \(A \to h(\sigma)\), the production \(\langle\tau\rangle \to h(\tau)\) for every suffix \(\tau\) of \(\sigma\) (including \(\sigma\) itself) with at least two entries, and the production \(i \to a\) for every terminal \(a\) occurring in \(\alpha\), where \(i\) is the encoding of \(a\); it has no other productions.

This construction is meant for reduced grammars, which have no empty outputs and no outputs consisting of a single nonterminal: on other grammars such outputs get the empty head, and in general neither the language nor Chomsky normal form is preserved.

@[reducible] noncomputable def cnfGrammar (g : ContextFreeGrammar T) :
    ContextFreeGrammar T where
  NT := (g.NT ⊕ ℕ) ⊕ List (g.NT ⊕ ℕ)
  initial := .inl (.inl g.initial)
  rules := g.rules.biUnion fun r =>
    {⟨.inl (.inl r.input), cnfHead (r.output.map toCnfNT)⟩} ∪
    (((r.output.map toCnfNT).tails.filter fun σ => 2 ≤ σ.length).toFinset.image
      fun σ => ⟨.inr σ, cnfHead σ⟩) ∪
    (((r.output.filterMap fun s => match s with
        | .terminal a => some a
        | .nonterminal _ => none).toFinset.image
      fun a => ⟨.inl (.inr ((grammarTerminals g).idxOf a)),
        [Symbol.terminal a]⟩))

Uses 3 · Used by 5

Statement usesHead of a binarized output · Terminals of a grammar · Encoding symbols as basic nonterminals of the binarized grammar

Used byBinarization 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

DefinitionValuation of the binarized grammar by yields#✓fully proved

Let \(g\) be a context-free grammar and let \(a_0, a_1, \dots\) be its list of terminals occurring in production outputs. A basic symbol is a nonterminal of \(g\) or a natural number (a terminal wrapper); the nonterminals of the binarized grammar are the basic symbols together with a chain nonterminal \(\langle\sigma\rangle\) for every list \(\sigma\) of basic symbols. Decode a basic symbol as a symbol of \(g\): a nonterminal \(A\) of \(g\) as \(A\), a natural number \(i\) less than the length of the list as the terminal \(a_i\), and any other natural number as the initial nonterminal of \(g\). The valuation assigns to a basic symbol \(X\) the set of words that the decoding of \(X\) yields in \(g\), and to a chain nonterminal \(\langle\sigma\rangle\) the set of words that the symbolwise decoding of \(\sigma\) yields in \(g\).

noncomputable def cnfValuation :
    (g.NT ⊕ ℕ) ⊕ List (g.NT ⊕ ℕ) → Language T
  | .inl B => {w | Yields g [fromCnfNT B] w}
  | .inr σ => {w | Yields g (σ.map fromCnfNT) w}

Uses 2 · Used by 1

Statement usesYield of a sentential form · Decoding basic nonterminals of the binarized grammar

Used byBinarization adds no words

TheoremBinarization adds no words#✓fully proved

If a context-free grammar \(g\) is reduced, then every word generated by the binarization of \(g\) is generated by \(g\).

theorem cnfGrammar_language_le_of_reduced (hred : IsReduced g) :
    (cnfGrammar g).language ≤ g.language

Uses 16 · Used by 1

Statement usesReduced grammars · Binarization of a grammar

Proof usesUnit output · Valuation of a grammar · Yield of a sentential form · Concatenation of yields · Splitting a yield over a concatenation · Head of a binarized output · Valuation of the binarized grammar by yields · Interpretation of a sentential form · Decoding basic nonterminals of the binarized grammar · Terminals of a grammar · Valuations bound the language of a grammar · Language membership through yields · Encoding symbols as basic nonterminals of the binarized grammar · Yield through one production

Used byBinarization preserves the language

TheoremBinarization has no empty productions#✓fully proved

If a context-free grammar \(g\) is reduced, then no production of the binarization of \(g\) has the empty word as output.

theorem cnfGrammar_output_ne_nil (hred : IsReduced g) :
    ∀ ρ ∈ (cnfGrammar g).rules, ρ.output ≠ []

Uses 6 · Used by 2

Statement usesReduced grammars · Binarization of a grammar

Proof usesUnit output · Head of a binarized output · Terminals of a grammar · Encoding symbols as basic nonterminals of the binarized grammar

Used byBinarization of a reduced grammar is in Chomsky normal form · Chomsky normal form theorem

TheoremBinarization of a reduced grammar is in Chomsky normal form#✓fully proved

If a context-free grammar \(g\) is reduced, then the binarization of \(g\) is in Chomsky normal form.

theorem cnfGrammar_isChomskyNormalForm (hred : IsReduced g) :
    IsChomskyNormalForm (cnfGrammar g)

Uses 8 · Used by 1

Statement usesChomsky normal form · Reduced grammars · Binarization of a grammar

Proof usesUnit output · Binarization has no empty productions · Head of a binarized output · Terminals of a grammar · Encoding symbols as basic nonterminals of the binarized grammar

Used byChomsky normal form theorem

TheoremBinarization preserves the language#✓fully proved

If a context-free grammar \(g\) is reduced, then the binarization of \(g\) generates exactly the language of \(g\).

theorem cnfGrammar_language_of_reduced (hred : IsReduced g) :
    (cnfGrammar g).language = g.language

Uses 22 · Used by 1

Statement usesReduced grammars · Binarization of a grammar

Proof usesUnit output · Valuation of a grammar · Yield of a sentential form · Concatenation of yields · Splitting a yield over a concatenation · Binarization adds no words · Head of a binarized output · Words of the canonical interpretation are derivable · Interpretation of a sentential form · Derivations shrink interpretations under a valuation · Interpretation after renaming nonterminals · A terminal word denotes its singleton · Terminals of a grammar · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal · Valuations bound the language of a grammar · Renaming the nonterminals of a symbol · Encoding symbols as basic nonterminals of the binarized grammar · Yields coincide with derivations of terminal words · Yield through one production

Used byChomsky normal form theorem

DefinitionGrammar with a fresh nullable start symbol#✓fully proved

Given a context-free grammar \(G\) with nonterminals \(N\) and initial nonterminal \(S\), this is the grammar with nonterminals \(N \cup \{S_0\}\) for a fresh symbol \(S_0\), initial nonterminal \(S_0\), and the following productions: every production of \(G\); the empty production \(S_0 \to \varepsilon\); and \(S_0 \to \alpha\) for every production \(S \to \alpha\) of \(G\).

The new grammar generates the language of \(G\) plus the empty word, and stays in Chomsky normal form when \(G\) is in Chomsky normal form and has no empty outputs.

@[reducible] noncomputable def epsStartGrammar (g : ContextFreeGrammar T) :
    ContextFreeGrammar T where
  NT := Option g.NT
  initial := none
  rules := (g.rules.map
      ⟨mapRule Option.some, mapRule_injective (Option.some_injective _)⟩) ∪
    {⟨none, []⟩} ∪
    ((g.rules.filter fun r => r.input = g.initial).image fun r =>
      ⟨none, r.output.map (mapSymbol Option.some)⟩)

Uses 3 · Used by 5

Statement usesRenaming the nonterminals of a production · Injective renamings are injective on productions · Renaming the nonterminals of a symbol

Used byThe fresh start symbol occurs in no output · Adding a fresh start symbol preserves Chomsky normal form · Language of the grammar with a fresh nullable start symbol · A fresh start symbol is harmless when the empty word is generated · Chomsky normal form theorem

TheoremLanguage of the grammar with a fresh nullable start symbol#✓fully proved

For every context-free grammar \(G\), the grammar obtained from \(G\) by adding a fresh initial nonterminal (with an empty production and copies of the productions of the old initial nonterminal) generates exactly \(L(G) \cup \{\varepsilon\}\), where \(L(G)\) is the language of \(G\) and \(\varepsilon\) is the empty word.

theorem epsStartGrammar_language (g : ContextFreeGrammar T) :
    (epsStartGrammar g).language = insert [] g.language

Uses 17 · Used by 2

Statement usesGrammar with a fresh nullable start symbol

Proof usesValuation of a grammar · Yield of a sentential form · Words of the canonical interpretation are derivable · Interpretation of a sentential form · Derivations shrink interpretations under a valuation · Interpretation after renaming nonterminals · A terminal word denotes its singleton · The languages generated from each nonterminal form a valuation · Language generated from a nonterminal · Valuations bound the language of a grammar · Renaming the nonterminals of a production · Injective renamings are injective on productions · Renaming the nonterminals of a symbol · Language membership through yields · Yields coincide with derivations of terminal words · Yield through one production

Used byA fresh start symbol is harmless when the empty word is generated · Chomsky normal form theorem

TheoremThe fresh start symbol occurs in no output#✓fully proved

For every context-free grammar \(g\), the fresh initial nonterminal of the fresh-start grammar of \(g\) occurs in no production output of the fresh-start grammar.

theorem epsStartGrammar_initial_not_mem_output :
    ∀ ρ ∈ (epsStartGrammar g).rules,
      Symbol.nonterminal (epsStartGrammar g).initial ∉ ρ.output

Uses 4 · Used by 1

Statement usesGrammar with a fresh nullable start symbol

Proof usesRenaming the nonterminals of a production · Injective renamings are injective on productions · Renaming the nonterminals of a symbol

Used byAdding a fresh start symbol preserves Chomsky normal form

TheoremA fresh start symbol is harmless when the empty word is generated#✓fully proved

If the empty word belongs to the language of a context-free grammar \(g\), then the fresh-start grammar of \(g\) generates exactly the language of \(g\).

theorem epsStartGrammar_language_of_mem_nil
    (hε : ([] : List T) ∈ g.language) :
    (epsStartGrammar g).language = g.language

Uses 2

Statement usesGrammar with a fresh nullable start symbol

Proof usesLanguage of the grammar with a fresh nullable start symbol

TheoremAdding a fresh start symbol preserves Chomsky normal form#✓fully proved

If a context-free grammar \(g\) is in Chomsky normal form and no production of \(g\) has empty output, then the fresh-start grammar of \(g\) is in Chomsky normal form.

The no-empty-outputs hypothesis is essential: an existing empty production would be embedded with the old initial nonterminal, not the fresh one, on the left.

theorem epsStartGrammar_isChomskyNormalForm
    (hCNF : IsChomskyNormalForm g)
    (hne : ∀ r ∈ g.rules, r.output ≠ []) :
    IsChomskyNormalForm (epsStartGrammar g)

Uses 6 · Used by 1

Statement usesChomsky normal form · Grammar with a fresh nullable start symbol

Proof usesThe fresh start symbol occurs in no output · Renaming the nonterminals of a production · Injective renamings are injective on productions · Renaming the nonterminals of a symbol

Used byChomsky normal form theorem

TheoremChomsky normal form theorem#✓fully proved

For every context-free grammar \(G\) there is a context-free grammar in Chomsky normal form that generates the same language as \(G\).

theorem exists_chomskyNormalForm (g₀ : ContextFreeGrammar T) :
    ∃ g' : ContextFreeGrammar T, g'.language = g₀.language ∧
      IsChomskyNormalForm g'

Uses 11 · Used by 1

Statement usesChomsky normal form

Proof usesReduced grammars · Unit output · Binarization of a grammar · Binarization of a reduced grammar is in Chomsky normal form · Binarization preserves the language · Binarization has no empty productions · Grammar with a fresh nullable start symbol · Adding a fresh start symbol preserves Chomsky normal form · Language of the grammar with a fresh nullable start symbol · Existence of reduced grammars

Used byChomsky normal form for context-free languages

TheoremChomsky normal form for context-free languages#✓fully proved

Every context-free language \(L\) is generated by some context-free grammar in Chomsky normal form.

theorem IsContextFree.exists_chomskyNormalForm {L : Language T}
    (hL : L.IsContextFree) :
    ∃ g : ContextFreeGrammar T, g.language = L ∧
      IsChomskyNormalForm g

Uses 2

Statement usesChomsky normal form

Proof usesChomsky normal form theorem

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.