Every context-free grammar has an equivalent one with finite nonterminals

Since a ContextFreeGrammar stores its rules in a Finset, only finitely many nonterminals can ever appear in a derivation. We restrict the nonterminal type to those that actually occur in the grammar, producing an equivalent grammar whose nonterminal type is Fintype.

Main results

• ContextFreeGrammar.toFiniteNT — restrict any CFG to one with Fintype NT.
• ContextFreeGrammar.toFiniteNT_language — the restricted grammar generates the same language.
• ContextFreeGrammar.exists_fintype_nt — every context-free language has a grammar with Fintype NT.

Used nonterminals

noncomputable def ContextFreeGrammar.usedNT {T : Type} (g : ContextFreeGrammar T) : Finset g.NT

The finite set of nonterminals occurring in the grammar (rules + start symbol).

Equations

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

theorem ContextFreeGrammar.initial_mem_usedNT {T : Type} (g : ContextFreeGrammar T) : g.initial ∈ g.usedNT

theorem ContextFreeGrammar.input_mem_usedNT {T : Type} (g : ContextFreeGrammar T) {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules) : r.input ∈ g.usedNT

theorem ContextFreeGrammar.output_nonterminal_mem_usedNT {T : Type} (g : ContextFreeGrammar T) {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules) {n : g.NT} (hn : Symbol.nonterminal n ∈ r.output) : n ∈ g.usedNT

def ContextFreeGrammar.UsedNT {T : Type} (g : ContextFreeGrammar T) : Type

The restricted nonterminal type: nonterminals actually appearing in the grammar.

Equations

• g.UsedNT = { n : g.NT // n ∈ g.usedNT }

noncomputable instance ContextFreeGrammar.instFintypeUsedNT {T : Type} (g : ContextFreeGrammar T) : Fintype g.UsedNT

Equations

• g.instFintypeUsedNT = Fintype.subtype g.usedNT ⋯

Symbol embedding and restriction

def ContextFreeGrammar.liftSymbol {T : Type} (g : ContextFreeGrammar T) : Symbol T g.UsedNT → Symbol T g.NT

Embed a symbol over the restricted nonterminals back to the original type.

Equations

• g.liftSymbol (Symbol.terminal t) = Symbol.terminal t
• g.liftSymbol (Symbol.nonterminal ⟨n, property⟩) = Symbol.nonterminal n

def ContextFreeGrammar.liftWord {T : Type} (g : ContextFreeGrammar T) : List (Symbol T g.UsedNT) → List (Symbol T g.NT)

Embed a word over restricted nonterminals back to the original type.

Equations

• g.liftWord = List.map g.liftSymbol

theorem ContextFreeGrammar.liftSymbol_injective {T : Type} (g : ContextFreeGrammar T) : Function.Injective g.liftSymbol

theorem ContextFreeGrammar.liftWord_append {T : Type} (g : ContextFreeGrammar T) (u v : List (Symbol T g.UsedNT)) : g.liftWord (u ++ v) = g.liftWord u ++ g.liftWord v

theorem ContextFreeGrammar.liftWord_map_terminal {T : Type} (g : ContextFreeGrammar T) (w : List T) : g.liftWord (List.map Symbol.terminal w) = List.map Symbol.terminal w

def ContextFreeGrammar.restrictOneSymbol {T : Type} (g : ContextFreeGrammar T) (s : Symbol T g.NT) (h : ∀ (n : g.NT), s = Symbol.nonterminal n → n ∈ g.usedNT) : Symbol T g.UsedNT

Restrict a single symbol, given that any nonterminal in it is used.

Equations

• g.restrictOneSymbol (Symbol.terminal t) x = Symbol.terminal t
• g.restrictOneSymbol (Symbol.nonterminal n) h_2 = Symbol.nonterminal ⟨n, ⋯⟩

theorem ContextFreeGrammar.liftSymbol_restrictOneSymbol {T : Type} (g : ContextFreeGrammar T) (s : Symbol T g.NT) (h : ∀ (n : g.NT), s = Symbol.nonterminal n → n ∈ g.usedNT) : g.liftSymbol (g.restrictOneSymbol s h) = s

All-used predicate

def ContextFreeGrammar.AllUsed {T : Type} (g : ContextFreeGrammar T) (w : List (Symbol T g.NT)) : Prop

All nonterminals in a word are used.

Equations

• g.AllUsed w = ∀ s ∈ w, ∀ (n : g.NT), s = Symbol.nonterminal n → n ∈ g.usedNT

theorem ContextFreeGrammar.allUsed_initial {T : Type} (g : ContextFreeGrammar T) : g.AllUsed [Symbol.nonterminal g.initial]

theorem ContextFreeGrammar.allUsed_append {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.NT)} : g.AllUsed (u ++ v) ↔ g.AllUsed u ∧ g.AllUsed v

theorem ContextFreeGrammar.allUsed_cons {T : Type} (g : ContextFreeGrammar T) {s : Symbol T g.NT} {w : List (Symbol T g.NT)} : g.AllUsed (s :: w) ↔ (∀ (n : g.NT), s = Symbol.nonterminal n → n ∈ g.usedNT) ∧ g.AllUsed w

theorem ContextFreeGrammar.allUsed_output {T : Type} (g : ContextFreeGrammar T) {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules) : g.AllUsed r.output

theorem ContextFreeGrammar.allUsed_produces {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.NT)} (h : g.Produces u v) (hu : g.AllUsed u) : g.AllUsed v

theorem ContextFreeGrammar.allUsed_derives {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.NT)} (h : g.Derives u v) (hu : g.AllUsed u) : g.AllUsed v

theorem ContextFreeGrammar.allUsed_map_terminal {T : Type} (g : ContextFreeGrammar T) (w : List T) : g.AllUsed (List.map Symbol.terminal w)

Word restriction

def ContextFreeGrammar.restrictWord {T : Type} (g : ContextFreeGrammar T) (w : List (Symbol T g.NT)) (hw : g.AllUsed w) : List (Symbol T g.UsedNT)

Restrict a word with all-used nonterminals to the restricted type.

Equations

• g.restrictWord w hw = List.pmap (fun (s : Symbol T g.NT) (hs : s ∈ w) => g.restrictOneSymbol s ⋯) w ⋯

theorem ContextFreeGrammar.liftWord_restrictWord {T : Type} (g : ContextFreeGrammar T) (w : List (Symbol T g.NT)) (hw : g.AllUsed w) : g.liftWord (g.restrictWord w hw) = w

theorem ContextFreeGrammar.restrictWord_append {T : Type} (g : ContextFreeGrammar T) (u v : List (Symbol T g.NT)) (hu : g.AllUsed u) (hv : g.AllUsed v) (huv : g.AllUsed (u ++ v)) : g.restrictWord (u ++ v) huv = g.restrictWord u hu ++ g.restrictWord v hv

theorem ContextFreeGrammar.restrictWord_initial {T : Type} (g : ContextFreeGrammar T) : g.restrictWord [Symbol.nonterminal g.initial] ⋯ = [Symbol.nonterminal ⟨g.initial, ⋯⟩]

theorem ContextFreeGrammar.restrictWord_map_terminal {T : Type} (g : ContextFreeGrammar T) (w : List T) (hw : g.AllUsed (List.map Symbol.terminal w)) : g.restrictWord (List.map Symbol.terminal w) hw = List.map Symbol.terminal w

The restricted grammar

def ContextFreeGrammar.restrictRule {T : Type} (g : ContextFreeGrammar T) (r : ContextFreeRule T g.NT) (hr : r ∈ g.rules) : ContextFreeRule T g.UsedNT

Restrict a rule to used nonterminals.

Equations

• g.restrictRule r hr = { input := ⟨r.input, ⋯⟩, output := g.restrictWord r.output ⋯ }

theorem ContextFreeGrammar.liftWord_restrictRule_output {T : Type} (g : ContextFreeGrammar T) (r : ContextFreeRule T g.NT) (hr : r ∈ g.rules) : g.liftWord (g.restrictRule r hr).output = r.output

noncomputable def ContextFreeGrammar.toFiniteNT {T : Type} (g : ContextFreeGrammar T) : ContextFreeGrammar T

The context-free grammar with nonterminals restricted to the finite used set.

Equations

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

noncomputable instance ContextFreeGrammar.toFiniteNT_fintype {T : Type} (g : ContextFreeGrammar T) : Fintype g.toFiniteNT.NT

Equations

• g.toFiniteNT_fintype = id g.instFintypeUsedNT

theorem ContextFreeGrammar.restrictRule_mem_toFiniteNT {T : Type} (g : ContextFreeGrammar T) (r : ContextFreeRule T g.NT) (hr : r ∈ g.rules) : g.restrictRule r hr ∈ g.toFiniteNT.rules

theorem ContextFreeGrammar.mem_toFiniteNT_rules {T : Type} (g : ContextFreeGrammar T) (r' : ContextFreeRule T g.UsedNT) (hr' : r' ∈ g.toFiniteNT.rules) : ∃ (r : ContextFreeRule T g.NT) (hr : r ∈ g.rules), r' = g.restrictRule r hr

Direction 1: toFiniteNT derives → original derives

theorem ContextFreeGrammar.liftWord_produces {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.UsedNT)} (h : g.toFiniteNT.Produces u v) : g.Produces (g.liftWord u) (g.liftWord v)

theorem ContextFreeGrammar.liftWord_derives {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.UsedNT)} (h : g.toFiniteNT.Derives u v) : g.Derives (g.liftWord u) (g.liftWord v)

Direction 2: original derives from initial → toFiniteNT derives

theorem ContextFreeGrammar.restrictWord_produces {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.NT)} (h : g.Produces u v) (hu : g.AllUsed u) (hv : g.AllUsed v) : g.toFiniteNT.Produces (g.restrictWord u hu) (g.restrictWord v hv)

theorem ContextFreeGrammar.restrictWord_derives {T : Type} (g : ContextFreeGrammar T) {u v : List (Symbol T g.NT)} (h : g.Derives u v) (hu : g.AllUsed u) (hv : g.AllUsed v) : g.toFiniteNT.Derives (g.restrictWord u hu) (g.restrictWord v hv)

Main theorem

theorem ContextFreeGrammar.toFiniteNT_language {T : Type} (g : ContextFreeGrammar T) : g.toFiniteNT.language = g.language

theorem ContextFreeGrammar.exists_fintype_nt {T : Type} (L : Language T) (hL : L.IsContextFree) : ∃ (g : ContextFreeGrammar T) (x : Fintype g.NT), g.language = L