Computable reduction of context-free grammars

TheoremA form yielding the empty word contains no terminal#✓fully proved

Let \(G\) be a context-free grammar over terminals \(T\) and let \(\alpha\) be a sentential form of \(G\). If \(\alpha\) yields the empty word in \(G\), then no terminal symbol \(a \in T\) occurs in \(\alpha\).

theorem Yields.terminal_not_mem {G : ContextFreeGrammar T} {α : List (Symbol T G.NT)}
    (h : Yields G α []) {a : T} : Symbol.terminal a ∉ α

Uses 1 · Used by 1

Statement usesYield of a sentential form

Used byYields of the empty word need only terminal-free productions

25 fully proved

Nullable nonterminals

DefinitionProductions without terminals of an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\), the encoded grammar with the same start nonterminal whose productions are the productions of \(g\), in their order, whose right-hand sides contain no terminal.

def noTerminals (g : EncodedCFG T) : EncodedCFG T :=
  ⟨g.start, g.rules.filter fun e => e.2.all Sum.isLeft⟩

Uses 1 · Used by 6

Statement usesEncoded context-free grammars

Used byTerminal-free productions yield only the empty word · The nullable nonterminals are computed · Computed nullable nonterminals of an encoded grammar · Reduction is primitive recursive · Yields of the empty word need only terminal-free productions · Yields in the terminal-free subgrammar are yields of the grammar

DefinitionComputed nullable nonterminals of an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\), the list of generating nonterminals of the encoded grammar that has the start nonterminal of \(g\) and, as productions, the productions of \(g\) whose right-hand sides contain no terminal.

A nonterminal is in this list exactly when it derives the empty word in the grammar denoted by \(g\).

def nullable (g : EncodedCFG T) : List ℕ :=
  g.noTerminals.generating

Uses 3 · Used by 5

Statement usesEncoded context-free grammars · Generating nonterminals · Productions without terminals of an encoded grammar

Used byRemoving empty productions from an encoded grammar · Productions of the computable removal of empty productions · Computed deletions agree with nullable deletions · The nullable nonterminals are computed · Reduction is primitive recursive

TheoremYields of the empty word need only terminal-free productions#✓fully proved

Let \(g\) be an encoded context-free grammar and \(\alpha\) a sentential form of the grammar \(g\) denotes. If \(\alpha\) yields the empty word in that grammar, then \(\alpha\) also yields the empty word in the grammar denoted by the encoded grammar consisting of the productions of \(g\) that contain no terminal.

theorem yields_noTerminals {g : EncodedCFG T} {α : List (Symbol T g.toCFG.NT)}
    (h : Yields g.toCFG α []) : Yields g.noTerminals.toCFG α []

Uses 7 · Used by 1

Statement usesEncoded context-free grammars · Productions without terminals of an encoded grammar · Grammar denoted by an encoding · Yield of a sentential form

Proof usesDecoding a production · Decoding a grammar symbol · A form yielding the empty word contains no terminal

Used byThe nullable nonterminals are computed

TheoremTerminal-free productions yield only the empty word#✓fully proved

Let \(g\) be an encoded context-free grammar and consider the grammar of its productions without terminals. If a sentential form \(\alpha\) that contains no terminal yields a word \(w\) in that grammar, then \(w\) is the empty word.

theorem eq_nil_of_yields_noTerminals {g : EncodedCFG T} {α : List (Symbol T g.noTerminals.toCFG.NT)}
    {w : List T}
    (h : Yields g.noTerminals.toCFG α w) (hα : ∀ a, Symbol.terminal a ∉ α) : w = []

Uses 6 · Used by 1

Statement usesEncoded context-free grammars · Productions without terminals of an encoded grammar · Grammar denoted by an encoding · Yield of a sentential form

Proof usesDecoding a production · Decoding a grammar symbol

Used byThe nullable nonterminals are computed

TheoremYields in the terminal-free subgrammar are yields of the grammar#✓fully proved

Let \(g\) be an encoded context-free grammar, \(\alpha\) a sentential form and \(w\) a word. If \(\alpha\) yields \(w\) in the grammar denoted by the encoded grammar consisting of the productions of \(g\) that contain no terminal, then \(\alpha\) yields \(w\) in the grammar \(g\) denotes.

theorem yields_of_yields_noTerminals {g : EncodedCFG T}
    {α : List (Symbol T g.noTerminals.toCFG.NT)} {w : List T}
    (h : Yields g.noTerminals.toCFG α w) : Yields g.toCFG α w

Uses 6 · Used by 1

Statement usesEncoded context-free grammars · Productions without terminals of an encoded grammar · Grammar denoted by an encoding · Yield of a sentential form

Proof usesDecoding a production · Decoding a grammar symbol

Used byThe nullable nonterminals are computed

TheoremThe nullable nonterminals are computed#✓fully proved

For every encoded context-free grammar \(g\) and every natural number \(A\), \(A\) belongs to the computed list of nullable nonterminals of \(g\) (the generating nonterminals of the productions of \(g\) without terminals) if and only if \(A\) is nullable in the grammar denoted by \(g\), that is, \(A\) derives the empty word.

theorem mem_nullable_iff {g : EncodedCFG T} {A : ℕ} : A ∈ g.nullable ↔ Nullable g.toCFG A

Uses 17 · Used by 1

Statement usesEncoded context-free grammars · Computed nullable nonterminals of an encoded grammar · Grammar denoted by an encoding · Nullable nonterminal

Proof usesTerminal-free productions yield only the empty word · Soundness of the productive-nonterminal iteration · Generating nonterminals · Language of an encoded grammar · Productions without terminals of an encoded grammar · Completeness of the generating-nonterminal computation · Yields of the empty word need only terminal-free productions · Yields in the terminal-free subgrammar are yields of the grammar · Yield of a sentential form · Yields are derivable · Language generated from a nonterminal · Yields coincide with derivations of terminal words · Derivable terminal words are yields

Used byComputed deletions agree with nullable deletions

Removing empty productions

DefinitionDeleting nonterminals from an encoded right-hand side#✓fully proved

Let \(N\) be a list of natural numbers and \(u\) an encoded right-hand side, that is, a word whose letters are nonterminals \(i \in \mathbb{N}\) or terminals. The result is the list of all words obtained from \(u\) by deleting some of the occurrences of nonterminals that belong to \(N\) (possibly none, possibly all) and keeping every other letter in order; each choice of deleted occurrences contributes one entry of the list.

def deletions (N : List ℕ) (u : List (ℕ ⊕ T)) : List (List (ℕ ⊕ T)) :=
  u.foldr (fun s acc => acc.map (s :: ·) ++
    cond (Sum.elim (Decidability.memB N) (fun _ => false) s) acc []) [[]]

Uses 1 · Used by 4

Statement usesBoolean membership test for lists of natural numbers

Used byRemoving empty productions from an encoded grammar · Productions of the computable removal of empty productions · Computed deletions agree with nullable deletions · Reduction is primitive recursive

TheoremComputed deletions agree with nullable deletions#✓fully proved

Let \(g\) be an encoded context-free grammar. For every encoded word \(u\) and every sentential form \(\alpha\) of the grammar denoted by \(g\), \(\alpha\) is obtained from the decoding of \(u\) by deleting some occurrences of nullable nonterminals of the grammar denoted by \(g\) if and only if \(\alpha\) is the decoding of a word obtained from \(u\) by deleting some occurrences of nonterminals in the computed list of nullable nonterminals of \(g\).

theorem mem_nullableDeletions_iff {g : EncodedCFG T} :
    ∀ (u : List (ℕ ⊕ T)) (α : List (Symbol T ℕ)),
      α ∈ nullableDeletions g.toCFG (u.map decodeSymbol) ↔
        ∃ v ∈ deletions g.nullable u, v.map decodeSymbol = α

Uses 9 · Used by 1

Statement usesEncoded context-free grammars · Decoding a grammar symbol · Deleting nonterminals from an encoded right-hand side · Computed nullable nonterminals of an encoded grammar · Grammar denoted by an encoding · Nullable deletions

Proof usesBoolean membership test for lists of natural numbers · The nullable nonterminals are computed · Nullable nonterminal

Used byProductions of the computable removal of empty productions

DefinitionRemoving empty productions from an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\), the encoded grammar with the same start nonterminal whose productions are, for each production \(A \to u\) of \(g\), the productions \(A \to v\) for every nonempty word \(v\) obtained from \(u\) by deleting some occurrences of nonterminals in the computed list of nullable nonterminals of \(g\).

def epsElim (g : EncodedCFG T) : EncodedCFG T :=
  let N := g.nullable
  ⟨g.start, g.rules.flatMap fun e =>
    ((deletions N e.2).filter fun v => decide (0 < v.length)).map (e.1, ·)⟩

Uses 3 · Used by 7

Statement usesEncoded context-free grammars · Deleting nonterminals from an encoded right-hand side · Computed nullable nonterminals of an encoded grammar

Used byComputable 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 · The reduced grammar generates the language minus the empty word · Productions of the computable removal of empty productions · Reduction is primitive recursive · Reduction of an encoded grammar

TheoremProductions of the computable removal of empty productions#✓fully proved

For every encoded context-free grammar \(g\), a production is a production of the grammar denoted by the encoded grammar obtained from \(g\) by removing empty productions if and only if it is a production of the grammar obtained from the grammar denoted by \(g\) by eliminating empty productions.

theorem mem_epsElim_rules {g : EncodedCFG T} {r : ContextFreeRule T ℕ} :
    r ∈ g.epsElim.toCFG.rules ↔ r ∈ (epsGrammar g.toCFG).rules

Uses 12 · Used by 2

Statement usesEncoded context-free grammars · Removing empty productions from an encoded grammar · Grammar denoted by an encoding · Elimination of \(\varepsilon\)-productions

Proof usesDecoding a production · Decoding a grammar symbol · Deleting nonterminals from an encoded right-hand side · Computed deletions agree with nullable deletions · Computed nullable nonterminals of an encoded grammar · Productions of the \(\varepsilon\)-eliminated grammar come from productions of \(g\) · Productions of the ε-free grammar · Nullable deletions

Used byComputable removal of empty productions agrees with the classical one · The reduced grammar has no empty and no unit productions

TheoremComputable removal of empty productions agrees with the classical one#✓fully proved

For every encoded context-free grammar \(g\), the grammar denoted by the encoded grammar obtained from \(g\) by removing empty productions is equal to the grammar obtained from the grammar denoted by \(g\) by eliminating empty productions: from each production, all productions obtained by deleting some occurrences of nullable nonterminals from its output, except those with empty output.

theorem epsElim_toCFG (g : EncodedCFG T) : g.epsElim.toCFG = epsGrammar g.toCFG

Uses 7 · Used by 1

Statement usesEncoded context-free grammars · Removing empty productions from an encoded grammar · Grammar denoted by an encoding · Elimination of \(\varepsilon\)-productions

Proof usesDecoding a production · Productions of the computable removal of empty productions · Nullable deletions

Used byRemoving empty productions drops only the empty word

TheoremRemoving empty productions drops only the empty word#✓fully proved

For every encoded context-free grammar \(g\), the language of the encoded grammar obtained from \(g\) by removing empty productions consists of the nonempty words of the language of \(g\).

theorem language_epsElim (g : EncodedCFG T) :
    g.epsElim.language = {w | w ∈ g.language ∧ w ≠ []}

Uses 7 · Used by 1

Statement usesEncoded context-free grammars · Removing empty productions from an encoded grammar · Language of an encoded grammar

Proof usesComputable removal of empty productions agrees with the classical one · Grammar denoted by an encoding · Elimination of \(\varepsilon\)-productions · The \(\varepsilon\)-eliminated grammar generates the nonempty words of \(g\)

Used byThe reduced grammar generates the language minus the empty word

Removing unit productions

DefinitionNonterminals of an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\), the list obtained by duplicate removal from the list made of the start nonterminal of \(g\) followed, for each production of \(g\) in order, by its left-hand side and then the nonterminals of its right-hand side in order. It lists without repetitions the nonterminals that \(g\) mentions.

def ntList (g : EncodedCFG T) : List ℕ :=
  dedupB (g.start :: g.rules.flatMap fun e => e.1 :: e.2.filterMap Sum.getLeft?)

Uses 2 · Used by 5

Statement usesDuplicate removal for lists of natural numbers · Encoded context-free grammars

Used byProductions of the encoded unit elimination · Unit reachability is computed · Reduction is primitive recursive · Unit elimination for encoded grammars · Nonterminals reachable by unit productions in an encoded grammar

DefinitionTarget of a unit right-hand side#✓fully proved

For an encoded right-hand side \(u\), a list whose entries are nonterminals \(i \in \mathbb{N}\) or terminals, the optional value is \(B\) when \(u\) consists of the single nonterminal \(B\), and there is no value otherwise.

def unitTarget (u : List (ℕ ⊕ T)) : Option ℕ :=
  cond (decide (u.length = 1)) (u.head?.bind Sum.getLeft?) none

Used by 5

Used byProductions of the encoded unit elimination · Unit reachability is computed · Reduction is primitive recursive · Unit elimination for encoded grammars · One round of unit reachability

DefinitionOne round of unit reachability#✓fully proved

For an encoded context-free grammar \(g\), a natural number \(A\) and a list \(S\) of natural numbers, the list consisting of \(A\) followed, for each production of \(g\) in order whose left-hand side lies in \(S\) and whose right-hand side is a single nonterminal \(B\), by that nonterminal \(B\).

def unitStep (g : EncodedCFG T) (A : ℕ) (S : List ℕ) : List ℕ :=
  A :: g.rules.filterMap fun e => cond (Decidability.memB S e.1) (unitTarget e.2) none

Uses 3 · Used by 3

Statement usesBoolean membership test for lists of natural numbers · Encoded context-free grammars · Target of a unit right-hand side

Used byUnit reachability is computed · Reduction is primitive recursive · Nonterminals reachable by unit productions in an encoded grammar

DefinitionNonterminals reachable by unit productions in an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\) and a natural number \(A\), let \(n\) be the number of distinct nonterminals mentioned in \(g\) (the start, the left-hand sides, and the nonterminals on right-hand sides). The list is obtained from the empty list by applying one round of unit reachability from \(A\) exactly \(n + 1\) times.

Its entries are exactly the nonterminals \(B\) reachable from \(A\) by a possibly empty chain of unit productions \(A \to \dots \to B\) of \(g\); in particular \(A\) itself is an entry.

def unitReach (g : EncodedCFG T) (A : ℕ) : List ℕ :=
  (g.unitStep A)^[(A :: g.ntList).length] []

Uses 3 · Used by 4

Statement usesEncoded context-free grammars · Nonterminals of an encoded grammar · One round of unit reachability

Used byProductions of the encoded unit elimination · Unit reachability is computed · Reduction is primitive recursive · Unit elimination for encoded grammars

TheoremUnit reachability is computed#✓fully proved

Let \(g\) be an encoded context-free grammar and let \(A\) and \(B\) be natural numbers. Then \(B\) belongs to the computed list of nonterminals reachable from \(A\) by unit productions of \(g\) if and only if there are \(k \ge 0\) and nonterminals \(A = C_0, C_1, \dots, C_k = B\) such that \(C_{i-1} \to C_i\) is a production of the grammar denoted by \(g\) for every \(i\) with \(1 \le i \le k\).

theorem mem_unitReach_iff {g : EncodedCFG T} {A B : ℕ} :
    B ∈ g.unitReach A ↔ UnitSteps g.toCFG A B

Uses 14 · Used by 1

Statement usesEncoded context-free grammars · Grammar denoted by an encoding · Nonterminals reachable by unit productions in an encoded grammar · Reachability by unit productions

Proof usesDuplicate removal for lists of natural numbers · Bounded monotone rounds on lists close off · Boolean membership test for lists of natural numbers · Decoding a production · Decoding a grammar symbol · Encoding a production · Encoding a grammar symbol · Nonterminals of an encoded grammar · One round of unit reachability · Target of a unit right-hand side

Used byProductions of the encoded unit elimination

DefinitionUnit elimination for encoded grammars#✓fully proved

For an encoded context-free grammar \(g\), the encoded grammar with the start nonterminal of \(g\) whose productions are listed as follows: for each nonterminal \(A\) in the list of nonterminals of \(g\), and for each production \(B \to u\) of \(g\) in order such that \(B\) is in the computed list of nonterminals reachable from \(A\) by unit productions and \(u\) is not a single nonterminal, the production \(A \to u\).

def unitElim (g : EncodedCFG T) : EncodedCFG T :=
  ⟨g.start, g.ntList.flatMap fun A =>
    let R := g.unitReach A
    g.rules.filterMap fun e =>
      cond (Decidability.memB R e.1 && !(unitTarget e.2).isSome) (some (A, e.2)) none⟩

Uses 5 · Used by 6

Statement usesBoolean membership test for lists of natural numbers · Encoded context-free grammars · Nonterminals of an encoded grammar · Nonterminals reachable by unit productions in an encoded grammar · Target of a unit right-hand side

Used byThe 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 · Reduction is primitive recursive · Reduction of an encoded grammar · The encoded unit elimination denotes the unit-eliminated grammar

TheoremProductions of the encoded unit elimination#✓fully proved

Let \(g\) be an encoded context-free grammar over terminals \(T\) and let \(r\) be a production with terminals in \(T\) and nonterminals in \(\mathbb{N}\). Then \(r\) is a production of the grammar denoted by the encoded unit elimination of \(g\) if and only if \(r\) is a production of the grammar obtained from the grammar denoted by \(g\) by eliminating unit productions.

theorem mem_unitElim_rules {g : EncodedCFG T} {r : ContextFreeRule T ℕ} :
    r ∈ g.unitElim.toCFG.rules ↔ r ∈ (unitGrammar g.toCFG).rules

Uses 20 · Used by 1

Statement usesEncoded context-free grammars · Grammar denoted by an encoding · Unit elimination for encoded grammars · Eliminating unit productions

Proof usesDuplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Decoding a production · Decoding a grammar symbol · Encoding a grammar symbol · Unit reachability is computed · Nonterminals of an encoded grammar · Nonterminals reachable by unit productions in an encoded grammar · Target of a unit right-hand side · Unit output · Reachability by unit productions · Productions of the unit-eliminated grammar come from non-unit productions of \(g\) · Nonterminals of a sentential form · Set of nonterminals mentioned by a grammar · Unit chains start at mentioned nonterminals · Productions of the unit-free grammar

Used byThe encoded unit elimination denotes the unit-eliminated grammar

TheoremThe encoded unit elimination denotes the unit-eliminated grammar#✓fully proved

For every encoded context-free grammar \(g\), the grammar denoted by the encoded unit elimination of \(g\) is equal to the grammar obtained from the grammar denoted by \(g\) by eliminating unit productions.

theorem unitElim_toCFG (g : EncodedCFG T) : g.unitElim.toCFG = unitGrammar g.toCFG

Uses 9 · Used by 2

Statement usesEncoded context-free grammars · Grammar denoted by an encoding · Unit elimination for encoded grammars · Eliminating unit productions

Proof usesDecoding a production · Productions of the encoded unit elimination · Unit output · Reachability by unit productions · Set of nonterminals mentioned by a grammar

Used byThe reduced grammar has no empty and no unit productions · The reduced grammar generates the language minus the empty word

Reduction

DefinitionReduction of an encoded grammar#✓fully proved

For an encoded context-free grammar \(g\), the encoded grammar obtained by first removing the empty productions of \(g\) (encoded \(\varepsilon\)-elimination) and then removing the unit productions of the result (encoded unit elimination).

def reduce (g : EncodedCFG T) : EncodedCFG T :=
  g.epsElim.unitElim

Uses 3 · Used by 3

Statement usesEncoded context-free grammars · Removing empty productions from an encoded grammar · Unit elimination for encoded grammars

Used byThe reduced grammar has no empty and no unit productions · The reduced grammar generates the language minus the empty word · Reduction is primitive recursive

TheoremThe reduced grammar generates the language minus the empty word#✓fully proved

For every encoded context-free grammar \(g\), the language of the reduction of \(g\) (empty productions removed, then unit productions removed) consists of the nonempty words of the language of \(g\).

theorem language_reduce (g : EncodedCFG T) :
    g.reduce.language = {w | w ∈ g.language ∧ w ≠ []}

Uses 10

Statement usesEncoded context-free grammars · Language of an encoded grammar · Reduction of an encoded grammar

Proof usesRemoving empty productions from an encoded grammar · Removing empty productions drops only the empty word · Grammar denoted by an encoding · Unit elimination for encoded grammars · The encoded unit elimination denotes the unit-eliminated grammar · Eliminating unit productions · Eliminating unit productions preserves the language

TheoremThe reduced grammar has no empty and no unit productions#✓fully proved

For every encoded context-free grammar \(g\), every production of the grammar denoted by the reduction of \(g\) (empty productions removed, then unit productions removed) has a nonempty output, and that output is not a single nonterminal.

theorem isReduced_reduce (g : EncodedCFG T) : IsReduced g.reduce.toCFG

Uses 14

Statement usesEncoded context-free grammars · Reduction of an encoded grammar · Grammar denoted by an encoding · Reduced grammars

Proof usesRemoving empty productions from an encoded grammar · Productions of the computable removal of empty productions · Unit elimination for encoded grammars · The encoded unit elimination denotes the unit-eliminated grammar · Unit output · Elimination of \(\varepsilon\)-productions · The \(\varepsilon\)-eliminated grammar has no empty productions · Eliminating unit productions · Eliminating unit productions leaves no unit production · Eliminating unit productions creates no new outputs

Primitive recursiveness

TheoremReduction is primitive recursive#✓fully proved

Let \(T\) be a type of terminals with a primitive recursive encoding. The map sending an encoded context-free grammar \(g\) over \(T\) to its reduction, the encoded grammar obtained from \(g\) by removing empty productions and then unit productions, is primitive recursive, where encoded grammars are encoded as pairs of a start nonterminal and a list of productions.

theorem primrec_reduce : Primrec (reduce (T := T))

Uses 17

Statement usesEncoded context-free grammars · Encoded grammars as pairs · Reduction of an encoded grammar

Proof usesDuplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Deleting nonterminals from an encoded right-hand side · Removing empty productions from an encoded grammar · One round of the generating-nonterminal computation · Generating nonterminals · Productions without terminals of an encoded grammar · Nonterminals of an encoded grammar · Computed nullable nonterminals of an encoded grammar · Acceptable productions · Unit elimination for encoded grammars · Nonterminals reachable by unit productions in an encoded grammar · One round of unit reachability · Target of a unit right-hand side

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.