Epsilon Elimination for CFGs

This file computes nullable nonterminals and removes empty productions while preserving the nonempty part of the language.

Main declarations

• computeNullables_iff
• eliminateEmpty_correct

theorem ContextFreeRule.Rewrites.empty {T : Type uT} {N : Type uN} {u : List (Symbol T N)} {r : ContextFreeRule T N} (hu : r.Rewrites u []) : r.output = []

Properties of context-free transformations to the empty string

@[reducible, inline]

abbrev ContextFreeGrammar.NullableNonTerminal {T : Type uT} {g : ContextFreeGrammar T} (n : g.NT) : Prop

NullableNonTerminal n holds if n can be transformed into the empty string

Equations

• ContextFreeGrammar.NullableNonTerminal n = g.Derives [Symbol.nonterminal n] []

@[reducible, inline]

abbrev ContextFreeGrammar.NullableWord {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T g.NT)) : Prop

NullableWord u holds if u can be transformed into the empty string

Equations

• ContextFreeGrammar.NullableWord u = g.Derives u []

theorem ContextFreeGrammar.DerivesIn.empty_of_append_left {T : Type uT} {g : ContextFreeGrammar T} {m : ℕ} {u v : List (Symbol T g.NT)} (huv : g.DerivesIn (u ++ v) [] m) : ∃ k ≤ m, g.DerivesIn u [] k

theorem ContextFreeGrammar.DerivesIn.empty_of_append_right_aux {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} {m : ℕ} (hwm : g.DerivesIn w [] m) (hw : w = u ++ v) : ∃ k ≤ m, g.DerivesIn v [] k

theorem ContextFreeGrammar.DerivesIn.empty_of_append_right {T : Type uT} {g : ContextFreeGrammar T} {m : ℕ} {u v : List (Symbol T g.NT)} (huv : g.DerivesIn (u ++ v) [] m) : ∃ k ≤ m, g.DerivesIn v [] k

theorem ContextFreeGrammar.DerivesIn.empty_of_append {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} {m : ℕ} (huvw : g.DerivesIn (u ++ v ++ w) [] m) : ∃ k ≤ m, g.DerivesIn v [] k

theorem ContextFreeGrammar.NullableWord.empty_of_append {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huvw : NullableWord (u ++ v ++ w)) : NullableWord v

theorem ContextFreeGrammar.NullableWord.empty_of_append_left {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableWord (u ++ v)) : NullableWord u

theorem ContextFreeGrammar.NullableWord.empty_of_append_right {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableWord (u ++ v)) : NullableWord v

theorem ContextFreeGrammar.DerivesIn.mem_nullable {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} {s : Symbol T g.NT} {m : ℕ} (hu : g.DerivesIn u [] m) (hsu : s ∈ u) : ∃ k ≤ m, g.DerivesIn [s] [] k

theorem ContextFreeGrammar.Derives.append_left_trans {T : Type uT} {g : ContextFreeGrammar T} {u v w x : List (Symbol T g.NT)} (huv : g.Derives u v) (hwx : g.Derives w x) : g.Derives (w ++ u) (x ++ v)

theorem ContextFreeGrammar.Produces.input_output {T : Type uT} {g : ContextFreeGrammar T} {r : ContextFreeRule T g.NT} (hrg : r ∈ g.rules) : g.Produces [Symbol.nonterminal r.input] r.output

theorem ContextFreeGrammar.NullableWord.cons_terminal {T : Type uT} {g : ContextFreeGrammar T} {t : T} {u : List (Symbol T g.NT)} : ¬NullableWord (Symbol.terminal t :: u)

theorem ContextFreeGrammar.Derives.of_empty {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} (hu : g.Derives [] u) : u = []

theorem ContextFreeGrammar.symbols_nullable_nullableWord {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T g.NT)) (hu : ∀ a ∈ u, g.Derives [a] []) : NullableWord u

theorem ContextFreeGrammar.DerivesIn.nullable_mem_nonterminal {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} {s : Symbol T g.NT} {m : ℕ} (hu : g.DerivesIn u [] m) (hsu : s ∈ u) : ∃ (n : g.NT), s = Symbol.nonterminal n

theorem ContextFreeGrammar.NullableWord.nullableNonTerminal {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} {s : Symbol T g.NT} (hu : NullableWord u) (hsu : s ∈ u) : ∃ (n : g.NT), s = Symbol.nonterminal n ∧ NullableNonTerminal n

inductive ContextFreeGrammar.NullableRelated {T : Type uT} {g : ContextFreeGrammar T} : List (Symbol T g.NT) → List (Symbol T g.NT) → Prop

NullableRelated u v means that v and u are equal up to interspersed nonterminals, each of which can be transformed to the empty string (i.e. for each additional nonterminal nt, NullableNonterminal nt holds)

• empty_left {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T g.NT)) (hu : NullableWord u) : NullableRelated [] u

  The empty string is NullableRelated to any w, s.t., NullableWord w

• cons_term {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableRelated u v) (t : T) : NullableRelated (Symbol.terminal t :: u) (Symbol.terminal t :: v)

  A terminal symbol t needs to be matched exactly

• cons_nterm_match {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableRelated u v) (n : g.NT) : NullableRelated (Symbol.nonterminal n :: u) (Symbol.nonterminal n :: v)

  A nonterminal symbol n can be matched exactly

• cons_nterm_nullable {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableRelated u v) {n : g.NT} (hn : NullableNonTerminal n) : NullableRelated u (Symbol.nonterminal n :: v)

  A nonterminal symbol n, s.t., NullableNonterminal n on the right, need not be matched

theorem ContextFreeGrammar.NullableRelated.refl {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T g.NT)) : NullableRelated u u

theorem ContextFreeGrammar.NullableRelated.derives {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (huv : NullableRelated u v) : g.Derives v u

theorem ContextFreeGrammar.NullableRelated.empty_nullableWord {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} (hu : NullableRelated [] u) : NullableWord u

theorem ContextFreeGrammar.NullableRelated.empty_right {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} (hu : NullableRelated u []) : u = []

theorem ContextFreeGrammar.NullableRelated.append_nullable_left {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : NullableRelated u v) (hw : NullableWord w) : NullableRelated u (w ++ v)

theorem ContextFreeGrammar.nullable_related_append {T : Type uT} {g : ContextFreeGrammar T} {u₁ u₂ v₁ v₂ : List (Symbol T g.NT)} (hv : NullableRelated v₁ v₂) (hu : NullableRelated u₁ u₂) : NullableRelated (v₁ ++ u₁) (v₂ ++ u₂)

theorem ContextFreeGrammar.NullableRelated.append_split {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huvw : NullableRelated u (v ++ w)) : ∃ (v' : List (Symbol T g.NT)) (w' : List (Symbol T g.NT)), u = v' ++ w' ∧ NullableRelated v' v ∧ NullableRelated w' w

theorem ContextFreeGrammar.NullableRelated.append_split_three {T : Type uT} {g : ContextFreeGrammar T} {u v w x : List (Symbol T g.NT)} (huvwx : NullableRelated u (v ++ w ++ x)) : ∃ (u₁ : List (Symbol T g.NT)) (u₂ : List (Symbol T g.NT)) (u₃ : List (Symbol T g.NT)), u = u₁ ++ u₂ ++ u₃ ∧ NullableRelated u₁ v ∧ NullableRelated u₂ w ∧ NullableRelated u₃ x

def ContextFreeGrammar.symbolIsNullable {T : Type uT} {N : Type uN} [DecidableEq N] (p : Finset N) (s : Symbol T N) : Bool

Check if a symbol is nullable (w.r.t. to set of nullable symbols p), i.e., symbol_is_nullable p s only holds if s is a nonterminal and it is in p

Equations

• ContextFreeGrammar.symbolIsNullable p (Symbol.terminal t) = decide False
• ContextFreeGrammar.symbolIsNullable p (Symbol.nonterminal n) = decide (n ∈ p)

def ContextFreeGrammar.ruleIsNullable {T : Type uT} {N : Type uN} [DecidableEq N] (p : Finset N) (r : ContextFreeRule T N) : Bool

A rule is nullable if all output symbols are nullable

Equations

• ContextFreeGrammar.ruleIsNullable p r = decide (∀ s ∈ r.output, ContextFreeGrammar.symbolIsNullable p s = true)

def ContextFreeGrammar.addIfNullable {T : Type uT} {N : Type uN} [DecidableEq N] (r : ContextFreeRule T N) (p : Finset N) : Finset N

Add the input of a rule as a nullable symbol to p if the rule is nullable

Equations

• ContextFreeGrammar.addIfNullable r p = if ContextFreeGrammar.ruleIsNullable p r = true then insert r.input p else p

theorem ContextFreeGrammar.subset_addIfNullable {T : Type uT} {N : Type uN} [DecidableEq N] (r : ContextFreeRule T N) (p : Finset N) : p ⊆ addIfNullable r p

noncomputable def ContextFreeGrammar.generators {T : Type uT} (g : ContextFreeGrammar T) [DecidableEq g.NT] : Finset g.NT

generators g is the set of all nonterminals that appear in the left hand side of rules of g

Equations

• g.generators = (List.map ContextFreeRule.input g.rules.toList).toFinset

theorem ContextFreeGrammar.input_mem_generators {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} (hrg : r ∈ g.rules) : r.input ∈ g.generators

theorem ContextFreeGrammar.addIfNullable_subset_generators {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {p : Finset g.NT} (hpg : p ⊆ g.generators) (hrg : r ∈ g.rules) : addIfNullable r p ⊆ g.generators

noncomputable def ContextFreeGrammar.addNullables {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) : Finset g.NT

Single round of fixpoint iteration; adds r.input to the set of nullable symbols if all symbols in r.output are nullable

Equations

• One or more equations did not get rendered due to their size.

theorem ContextFreeGrammar.addNullables_subset_generators {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : Finset g.NT} (hpg : p ⊆ g.generators) : addNullables p ⊆ g.generators

theorem ContextFreeGrammar.subset_addNullables {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) : p ⊆ addNullables p

theorem ContextFreeGrammar.generators_limits_nullable {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : Finset g.NT} (hpg : p ⊆ g.generators) (hne : p ≠ addNullables p) : g.generators.card - (addNullables p).card < g.generators.card - p.card

@[irreducible]

noncomputable def ContextFreeGrammar.addNullablesIter {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) (hpg : p ⊆ g.generators) : Finset g.NT

Fixpoint iteration computing the set of nullable symbols of g.

Equations

• ContextFreeGrammar.addNullablesIter p hpg = if p = ContextFreeGrammar.addNullables p then p else ContextFreeGrammar.addNullablesIter (ContextFreeGrammar.addNullables p) ⋯

noncomputable def ContextFreeGrammar.computeNullables {T : Type uT} (g : ContextFreeGrammar T) [DecidableEq g.NT] : Finset g.NT

Compute the least-fixpoint of add_nullable_iter, i.e., all (and only) nullable symbols

Equations

• g.computeNullables = ContextFreeGrammar.addNullablesIter ∅ ⋯

theorem ContextFreeGrammar.ruleIsNullable_NullableNonTerminal {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) (r : ContextFreeRule T g.NT) (hrg : r ∈ g.rules) (hn : ∀ v ∈ p, NullableNonTerminal v) (hr : ruleIsNullable p r = true) : NullableNonTerminal r.input

theorem ContextFreeGrammar.addNullables_mem_nullableNonTerminal {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) (hp : ∀ v ∈ p, NullableNonTerminal v) (v : g.NT) : v ∈ addNullables p → NullableNonTerminal v

@[irreducible]

theorem ContextFreeGrammar.addNullablesIter_only_nullableNonTerminal {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) (hpg : p ⊆ g.generators) (hp : ∀ v ∈ p, NullableNonTerminal v) (v : g.NT) : v ∈ addNullablesIter p hpg → NullableNonTerminal v

theorem ContextFreeGrammar.addIfNullable_monotone {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {p₁ p₂ : Finset g.NT} (hpp : p₁ ⊆ p₂) : addIfNullable r p₁ ⊆ addIfNullable r p₂

theorem ContextFreeGrammar.nullable_input_mem_addNullables {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {p : Finset g.NT} (hpr : ruleIsNullable p r = true) (hrg : r ∈ g.rules) : r.input ∈ addNullables p

@[irreducible]

theorem ContextFreeGrammar.addNullablesIter_fixpoint {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : Finset g.NT} (hpg : p ⊆ g.generators) : addNullablesIter p hpg = addNullables (addNullablesIter p hpg)

@[irreducible]

theorem ContextFreeGrammar.nullable_mem_addNullablesIter {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : Finset g.NT} (hpg : p ⊆ g.generators) (n : g.NT) (m : ℕ) (hvgm : g.DerivesIn [Symbol.nonterminal n] [] m) : n ∈ addNullablesIter p hpg

theorem ContextFreeGrammar.computeNullables_iff {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (n : g.NT) : n ∈ g.computeNullables ↔ NullableNonTerminal n

def ContextFreeGrammar.nullableCombinations {T : Type uT} {N : Type uN} [DecidableEq N] (p : Finset N) (u : List (Symbol T N)) : List (List (Symbol T N))

Compute all possible combinations of leaving out nullable nonterminals from u

Equations

• One or more equations did not get rendered due to their size.
• ContextFreeGrammar.nullableCombinations p [] = [[]]
• ContextFreeGrammar.nullableCombinations p (Symbol.terminal t :: s) = List.map (fun (x : List (Symbol T N)) => Symbol.terminal t :: x) (ContextFreeGrammar.nullableCombinations p s)

def ContextFreeGrammar.removeNullableRule {T : Type uT} {N : Type uN} [DecidableEq N] (p : Finset N) (r : ContextFreeRule T N) : List (ContextFreeRule T N)

Computes all variations of leaving out nullable symbols (except the empty string) of r

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContextFreeGrammar.removeNullables {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (p : Finset g.NT) : Finset (ContextFreeRule T g.NT)

Compute all variations of leaving out nullable symbols (except the empty string) of gs rules

Equations

• ContextFreeGrammar.removeNullables p = (List.map (ContextFreeGrammar.removeNullableRule p) g.rules.toList).flatten.toFinset

noncomputable def ContextFreeGrammar.eliminateEmpty {T : Type uT} [DecidableEq T] (g : ContextFreeGrammar T) [DecidableEq g.NT] : ContextFreeGrammar T

Equations

• g.eliminateEmpty = { NT := g.NT, initial := g.initial, rules := ContextFreeGrammar.removeNullables g.computeNullables }

theorem ContextFreeGrammar.output_mem_removeNullableRule {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r r' : ContextFreeRule T g.NT} {p : Finset g.NT} (hrr : r' ∈ removeNullableRule p r) : r'.output ≠ []

theorem ContextFreeGrammar.output_mem_removeNullables {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {r : ContextFreeRule T g.NT} {p : Finset g.NT} (hr : r ∈ removeNullables p) : r.output ≠ []

theorem ContextFreeGrammar.eliminateEmpty_produces_not_empty {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v : List (Symbol T g.NT)} (huv : g.eliminateEmpty.Produces u v) : v ≠ []

theorem ContextFreeGrammar.eliminateEmpty_derives_not_empty {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v : List (Symbol T g.NT)} (huv : g.eliminateEmpty.Derives u v) (hune : u ≠ []) : v ≠ []

theorem ContextFreeGrammar.mem_nullableCombinations_nullableRelated {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (p : Finset g.NT) (hn : ∀ x ∈ p, NullableNonTerminal x) (huv : u ∈ nullableCombinations p v) : NullableRelated u v

theorem ContextFreeGrammar.mem_removeNullableRule_nullableRelated {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {r' r : ContextFreeRule T g.NT} {hrg : r ∈ removeNullableRule g.computeNullables r'} : r.input = r'.input ∧ NullableRelated r.output r'.output

theorem ContextFreeGrammar.mem_eliminateEmpty {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {r : ContextFreeRule T g.NT} (hrg : r ∈ g.eliminateEmpty.rules) : ∃ r' ∈ g.rules, r.input = r'.input ∧ NullableRelated r.output r'.output

theorem ContextFreeGrammar.eliminateEmpty_produces_to_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v : List (Symbol T g.NT)} (huv : g.eliminateEmpty.Produces u v) : g.Derives u v

theorem ContextFreeGrammar.eliminateEmpty_derives_to_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v : List (Symbol T g.NT)} (huv : g.eliminateEmpty.Derives u v) : g.Derives u v

theorem ContextFreeGrammar.mem_nullableCombinations {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : Finset g.NT) (u : List (Symbol T g.NT)) : u ∈ nullableCombinations p u

theorem ContextFreeGrammar.nullableRelated_mem_removeNullable {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : Finset g.NT} {u v : List (Symbol T g.NT)} (hvu : NullableRelated v u) (hn : ∀ (s : g.NT), s ∈ p ↔ NullableNonTerminal s) : v ∈ nullableCombinations p u

theorem ContextFreeGrammar.nullableRelated_mem_eliminateEmpty_rules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {r : ContextFreeRule T g.NT} {u : List (Symbol T g.NT)} (hur : NullableRelated u r.output) (hrg : r ∈ g.rules) (hu : u ≠ []) : { input := r.input, output := u } ∈ g.eliminateEmpty.rules

theorem ContextFreeGrammar.produces_nullableRelated_to_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hwv : NullableRelated w v) : ∃ (u' : List (Symbol T g.NT)), NullableRelated u' u ∧ g.eliminateEmpty.Derives u' w

@[irreducible]

theorem ContextFreeGrammar.derivesIn_non_empty_to_nullableRelated_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u v : List (Symbol T g.NT)} (hv : v ≠ []) {m : ℕ} (huv : g.DerivesIn u v m) : ∃ (u' : List (Symbol T g.NT)), NullableRelated u' u ∧ g.eliminateEmpty.Derives u' v

theorem ContextFreeGrammar.derivesIn_to_eliminateEmpty_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {w : List (Symbol T g.NT)} {n : g.NT} {hw : w ≠ []} {m : ℕ} (hnwm : g.DerivesIn [Symbol.nonterminal n] w m) : g.eliminateEmpty.Derives [Symbol.nonterminal n] w

theorem ContextFreeGrammar.eliminateEmpty_correct {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] : g.language \ {[]} = g.eliminateEmpty.language