Unit-Rule Elimination for CFGs

This file computes unit pairs and removes unit productions without changing the language.

Main declarations

• computeUnitPairs_iff
• eliminateUnitRules_correct

theorem ContextFreeGrammar.Produces.rule {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} {u : List (Symbol T g.NT)} (hnu : g.Produces [Symbol.nonterminal n] u) : { input := n, output := u } ∈ g.rules

@[reducible, inline]

abbrev ContextFreeGrammar.unitRule {T : Type uT} {g : ContextFreeGrammar T} (nᵢ nₒ : g.NT) : ContextFreeRule T g.NT

Convenient to talk about the rule rewriting a nonterminal nᵢ to another nonterminal nₒ

Equations

• ContextFreeGrammar.unitRule nᵢ nₒ = { input := nᵢ, output := [Symbol.nonterminal nₒ] }

inductive ContextFreeGrammar.UnitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] : g.NT → g.NT → Prop

UnitPair n₁ n₂, (w.r.t. a ContextFreeGrammar g) means that g can derive n₂ from n₁ only using unitRules

• refl {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n : g.NT} (hng : n ∈ g.generators) : UnitPair n n
• trans {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n₁ n₂ n₃ : g.NT} (hng : unitRule n₁ n₂ ∈ g.rules) (hnn : UnitPair n₂ n₃) : UnitPair n₁ n₃

theorem ContextFreeGrammar.UnitPair.rfl {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n : g.NT} (hn : n ∈ g.generators) : UnitPair n n

theorem ContextFreeGrammar.UnitPair.derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n₁ n₂ : g.NT} (hnn : UnitPair n₁ n₂) : g.Derives [Symbol.nonterminal n₁] [Symbol.nonterminal n₂]

@[reducible, inline]

abbrev ContextFreeGrammar.NonUnit {T : Type uT} {N : Type u_1} (u : List (Symbol T N)) : Prop

We use this to concisely state a rule is not a unitRule if its output is NonUnit

Equations

• ContextFreeGrammar.NonUnit [Symbol.nonterminal n] = False
• ContextFreeGrammar.NonUnit u = True

theorem ContextFreeGrammar.DerivesIn.unitPair_prefix {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {u : List T} {v : List (Symbol T g.NT)} {n : g.NT} {m : ℕ} (hvu : g.DerivesIn v (List.map Symbol.terminal u) m) (hng : n ∈ g.generators) (hv : [Symbol.nonterminal n] = v) : ∃ (n' : g.NT) (w : List (Symbol T g.NT)) (k : ℕ), UnitPair n n' ∧ g.Produces [Symbol.nonterminal n'] w ∧ NonUnit w ∧ k ≤ m ∧ g.DerivesIn w (List.map Symbol.terminal u) k

Fixpoint iteration to compute all UnitPairs. A unit pair is a pair (n₁, n₂) of nonterminals s.t. g can transform n₁ to n₂ only using unitRules, i.e., a chain of productions rewriting nonterminals to nonterminals

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

generatorsProdDiag g is the diagonal of g.generators × g.generators

Equations

• ContextFreeGrammar.generatorsProdDiag = (List.map (fun (r : ContextFreeRule T g.NT) => (r.input, r.input)) g.rules.toList).toFinset

theorem ContextFreeGrammar.generatorsProdDiag_subset_generators_prod {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] : generatorsProdDiag ⊆ g.generators ×ˢ g.generators

theorem ContextFreeGrammar.generatorsProdDiag_unitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : g.NT × g.NT} (hp : p ∈ generatorsProdDiag) : UnitPair p.1 p.2

def ContextFreeGrammar.addUnitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (nᵢ nₒ : g.NT) (p : g.NT × g.NT) (l : Finset (g.NT × g.NT)) : Finset (g.NT × g.NT)

Reflects transitivity of unit pairs. If (n₂, n₃) is a unit pair and g rewrites n₁ to n₂ then (n₁, n₃) are also a unit pair

Equations

• ContextFreeGrammar.addUnitPair nᵢ nₒ p l = if nₒ = p.1 then insert (nᵢ, p.2) l else l

def ContextFreeGrammar.collectUnitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (r : ContextFreeRule T g.NT) (l : List (g.NT × g.NT)) : Finset (g.NT × g.NT)

If r is a unit rule, add all unit pairs (r.input, n) to l for all unit pairs (r.output, n) in l

Equations

• ContextFreeGrammar.collectUnitPairs r l = match r.output with | [Symbol.nonterminal v] => List.foldr (ContextFreeGrammar.addUnitPair r.input v) ∅ l | x => ∅

theorem ContextFreeGrammar.collectUnitPairs_unitPair_rec {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {nᵢ nₒ : g.NT} {p : g.NT × g.NT} {l : List (g.NT × g.NT)} {x : Finset (g.NT × g.NT)} (hp : p ∈ List.foldr (addUnitPair nᵢ nₒ) x l) : p ∈ x ∨ ∃ (v : g.NT), (nₒ, v) ∈ l ∧ p = (nᵢ, v)

theorem ContextFreeGrammar.collectUnitPairs_unitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {l : List (g.NT × g.NT)} (hrg : r ∈ g.rules) (hp : ∀ p ∈ l, UnitPair p.1 p.2) (p : g.NT × g.NT) : p ∈ collectUnitPairs r l → UnitPair p.1 p.2

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

Single step of fixpoint iteration, adding unit pairs to l for all rules r in g.rules

Equations

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

theorem ContextFreeGrammar.collectUnitPairs_subset_generatorsProd {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {r : ContextFreeRule T g.NT} (l : Finset (g.NT × g.NT)) (hlg : l ⊆ g.generators ×ˢ g.generators) (hrg : r ∈ g.rules) : collectUnitPairs r l.toList ⊆ g.generators ×ˢ g.generators

theorem ContextFreeGrammar.addUnitPairs_subset_generatorsProd {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) (hlg : l ⊆ g.generators ×ˢ g.generators) : addUnitPairs l ⊆ g.generators ×ˢ g.generators

theorem ContextFreeGrammar.subset_addUnitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) : l ⊆ addUnitPairs l

theorem ContextFreeGrammar.generatorsProd_limits_unitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {l : Finset (g.NT × g.NT)} (hlg : l ⊆ g.generators ×ˢ g.generators) (hne : l ≠ addUnitPairs l) : (g.generators ×ˢ g.generators).card - (addUnitPairs l).card < (g.generators ×ˢ g.generators).card - l.card

@[irreducible]

noncomputable def ContextFreeGrammar.addUnitPairsIter {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) (hlg : l ⊆ g.generators ×ˢ g.generators) : Finset (g.NT × g.NT)

Fixpoint iteration computing the unit pairs of g.

Equations

• ContextFreeGrammar.addUnitPairsIter l hlg = if l = ContextFreeGrammar.addUnitPairs l then l else ContextFreeGrammar.addUnitPairsIter (ContextFreeGrammar.addUnitPairs l) ⋯

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

Compute the least-fixpoint of add_unitPairs_iter, i.e., all (and only) unit pairs

Equations

• ContextFreeGrammar.computeUnitPairs = ContextFreeGrammar.addUnitPairsIter ContextFreeGrammar.generatorsProdDiag ⋯

theorem ContextFreeGrammar.mem_addUnitPairs_unitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) (hl : ∀ p ∈ l, UnitPair p.1 p.2) (p : g.NT × g.NT) : p ∈ addUnitPairs l → UnitPair p.1 p.2

@[irreducible]

theorem ContextFreeGrammar.mem_addUnitPairIter_unitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) (hlg : l ⊆ g.generators ×ˢ g.generators) (hl : ∀ p ∈ l, UnitPair p.1 p.2) (p : g.NT × g.NT) : p ∈ addUnitPairsIter l hlg → UnitPair p.1 p.2

@[irreducible]

theorem ContextFreeGrammar.addUnitPairsIter_fixpoint {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (l : Finset (g.NT × g.NT)) (hlg : l ⊆ g.generators ×ˢ g.generators) : addUnitPairsIter l hlg = addUnitPairs (addUnitPairsIter l hlg)

@[irreducible]

theorem ContextFreeGrammar.subset_addUnitPairsIter {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {l : Finset (g.NT × g.NT)} {hlg : l ⊆ g.generators ×ˢ g.generators} : l ⊆ addUnitPairsIter l hlg

theorem ContextFreeGrammar.mem_collectUnitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {l : List (g.NT × g.NT)} {n₁ n₂ n₃ : g.NT} (hl : (n₂, n₃) ∈ l) : (n₁, n₃) ∈ collectUnitPairs (unitRule n₁ n₂) l

theorem ContextFreeGrammar.mem_addUnitPairs {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {l : Finset (g.NT × g.NT)} {n₁ n₂ n₃ : g.NT} (hl : (n₂, n₃) ∈ l) (hg : { input := n₁, output := [Symbol.nonterminal n₂] } ∈ g.rules) : (n₁, n₃) ∈ addUnitPairs l

theorem ContextFreeGrammar.unitPair_mem_addUnitPairsIter {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {l : Finset (g.NT × g.NT)} {n₁ n₂ : g.NT} (hlg : l ⊆ g.generators ×ˢ g.generators) (hgl : generatorsProdDiag ⊆ l) (hp : UnitPair n₁ n₂) : (n₁, n₂) ∈ addUnitPairsIter l hlg

theorem ContextFreeGrammar.computeUnitPairs_iff {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n₁ n₂ : g.NT} : (n₁, n₂) ∈ computeUnitPairs ↔ UnitPair n₁ n₂

noncomputable def ContextFreeGrammar.computeUnitPairRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] (p : g.NT × g.NT) : List (ContextFreeRule T g.NT)

For a given unit pair (n₁, n₂), computes rules r : n₁ → o, s.t. there is a rule r' : n₂ → o in g (and o is non-unit)

Equations

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

noncomputable def ContextFreeGrammar.removeUnitRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] (l : Finset (g.NT × g.NT)) : Finset (ContextFreeRule T g.NT)

Equations

• ContextFreeGrammar.removeUnitRules l = (List.map ContextFreeGrammar.computeUnitPairRules l.toList).flatten.toFinset

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

Given g, computes a new grammar g' in which all unit rules are removed and, for each unit pair (n₁, n₂), we add rules r : n₁ → o if the rule r' : n₂ → o is in the grammar (and non-unit)

Equations

• g.eliminateUnitRules = { NT := g.NT, initial := g.initial, rules := ContextFreeGrammar.removeUnitRules ContextFreeGrammar.computeUnitPairs }

theorem ContextFreeGrammar.nonUnit_rules_mem {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {p : g.NT × g.NT} {r : ContextFreeRule T g.NT} (hrp : r ∈ computeUnitPairRules p) : r.input = p.1 ∧ ∃ r' ∈ g.rules, r.output = r'.output ∧ r'.input = p.2

theorem ContextFreeGrammar.mem_removeUnitRules_exists_UnitPair {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {l : Finset (g.NT × g.NT)} {r : ContextFreeRule T g.NT} (hrl : r ∈ removeUnitRules l) : ∃ (p : g.NT × g.NT) (r' : ContextFreeRule T g.NT), p ∈ l ∧ r' ∈ g.rules ∧ r.input = p.1 ∧ r.output = r'.output ∧ r'.input = p.2

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

theorem ContextFreeGrammar.nonUnit_mem_computeUnitPairRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] {n₁ n₂ : g.NT} {w : List (Symbol T g.NT)} (hg : { input := n₁, output := w } ∈ g.rules) (hw : NonUnit w) : { input := n₂, output := w } ∈ computeUnitPairRules (n₂, n₁)

theorem ContextFreeGrammar.nonUnit_mem_removeUnitRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {n₁ n₂ : g.NT} {u : List (Symbol T g.NT)} {l : Finset (g.NT × g.NT)} (hug : { input := n₂, output := u } ∈ g.rules) (hu : NonUnit u) (hnn : (n₁, n₂) ∈ l) : { input := n₁, output := u } ∈ removeUnitRules l

theorem ContextFreeGrammar.produces_nonUnit_eliminateUnitRules_produces {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {n₁ n₂ : g.NT} {u : List (Symbol T g.NT)} (hu : NonUnit u) (hnn : UnitPair n₁ n₂) (hgu : g.Produces [Symbol.nonterminal n₂] u) : g.eliminateUnitRules.Produces [Symbol.nonterminal n₁] u

theorem ContextFreeGrammar.nonUnit_output_mem_eliminateUnitRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {r : ContextFreeRule T g.NT} (hrg : r ∈ g.rules) (hro : NonUnit r.output) : r ∈ g.eliminateUnitRules.rules

@[irreducible]

theorem ContextFreeGrammar.derives_to_eliminateUnitRules_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] {u : List (Symbol T g.NT)} {v : List T} {m : ℕ} (huv : g.DerivesIn u (List.map Symbol.terminal v) m) : g.eliminateUnitRules.Derives u (List.map Symbol.terminal v)

theorem ContextFreeGrammar.eliminateUnitRules_correct {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq g.NT] [DecidableEq T] : g.language = g.eliminateUnitRules.language