Every unrestricted grammar is equivalent to one with finitely many nonterminals

Since an unrestricted grammar stores its rules in a List, only finitely many nonterminals can ever appear in a derivation from the initial symbol. We restrict the nonterminal type to those that actually occur in the grammar, producing an equivalent grammar whose nonterminal type carries a Fintype instance.

Main results

• restrictGrammar — restrict any grammar to one with Fintype nonterminals.
• grammar_language_eq_restrictGrammar — the restricted grammar generates the same language.
• grammar_equivalent_finiteNT — every unrestricted grammar has an equivalent one with Finite nonterminals.

Extracting nonterminals from symbol lists

def symbolsNTs {T N : Type} : List (symbol T N) → List N

Extract all nonterminals from a list of symbols.

Equations

• symbolsNTs [] = []
• symbolsNTs (symbol.terminal a :: rest) = symbolsNTs rest
• symbolsNTs (symbol.nonterminal n :: rest) = n :: symbolsNTs rest

@[simp]

theorem symbolsNTs_nil {T N : Type} : symbolsNTs [] = []

@[simp]

theorem symbolsNTs_cons_terminal {T N : Type} (t : T) (l : List (symbol T N)) : symbolsNTs (symbol.terminal t :: l) = symbolsNTs l

@[simp]

theorem symbolsNTs_cons_nonterminal {T N : Type} (n : N) (l : List (symbol T N)) : symbolsNTs (symbol.nonterminal n :: l) = n :: symbolsNTs l

theorem mem_symbolsNTs_iff {T N : Type} {n : N} {l : List (symbol T N)} : n ∈ symbolsNTs l ↔ symbol.nonterminal n ∈ l

theorem symbolsNTs_append {T N : Type} (l₁ l₂ : List (symbol T N)) : symbolsNTs (l₁ ++ l₂) = symbolsNTs l₁ ++ symbolsNTs l₂

theorem symbolsNTs_map_terminal {T N : Type} (w : List T) : symbolsNTs (List.map symbol.terminal w) = []

Used nonterminals of a grammar

def ruleNTs {T N : Type} (r : grule T N) : List N

All nonterminals mentioned in a grammar rule.

Equations

• ruleNTs r = symbolsNTs r.input_L ++ [r.input_N] ++ symbolsNTs r.input_R ++ symbolsNTs r.output_string

def usedNTsList {T : Type} (g : grammar T) : List g.nt

The list of all nonterminals used in a grammar.

Equations

• usedNTsList g = [g.initial] ++ List.flatMap ruleNTs g.rules

def usedNTs {T : Type} (g : grammar T) : Finset g.nt

The finite set of all nonterminals used in a grammar.

Equations

• usedNTs g = (usedNTsList g).toFinset

theorem initial_mem_usedNTs {T : Type} (g : grammar T) : g.initial ∈ usedNTs g

theorem ruleNT_mem_usedNTs {T : Type} {g : grammar T} {r : grule T g.nt} {n : g.nt} (hr : r ∈ g.rules) (hn : n ∈ ruleNTs r) : n ∈ usedNTs g

theorem inputN_mem_ruleNTs {T N : Type} (r : grule T N) : r.input_N ∈ ruleNTs r

The restricted grammar

@[reducible, inline]

abbrev UsedNT {T : Type} (g : grammar T) : Type

The subtype of used nonterminals.

Equations

• UsedNT g = { n : g.nt // n ∈ usedNTs g }

instance usedNT_fintype {T : Type} (g : grammar T) : Fintype (UsedNT g)

Equations

• usedNT_fintype g = Fintype.subtype (usedNTs g) ⋯

def restrictNT {T : Type} (g : grammar T) (n : g.nt) : UsedNT g

Restrict a nonterminal to UsedNT g. Maps unused nonterminals to the initial symbol.

Equations

• restrictNT g n = if h : n ∈ usedNTs g then ⟨n, h⟩ else ⟨g.initial, ⋯⟩

def restrictSym {T : Type} (g : grammar T) : symbol T g.nt → symbol T (UsedNT g)

Restrict a symbol to UsedNT g.

Equations

• restrictSym g (symbol.terminal t) = symbol.terminal t
• restrictSym g (symbol.nonterminal n) = symbol.nonterminal (restrictNT g n)

def embedSym {T : Type} (g : grammar T) : symbol T (UsedNT g) → symbol T g.nt

Embed a symbol over UsedNT g back into a symbol over g.nt.

Equations

• embedSym g (symbol.terminal t) = symbol.terminal t
• embedSym g (symbol.nonterminal ⟨n, property⟩) = symbol.nonterminal n

def restrictGrammar {T : Type} (g : grammar T) : grammar T

The grammar restricted to its used nonterminals.

Equations

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

instance restrictGrammar_fintype {T : Type} (g : grammar T) : Fintype (restrictGrammar g).nt

Equations

• restrictGrammar_fintype g = usedNT_fintype g

Properties of restrictSym and embedSym

theorem restrictNT_of_mem {T : Type} {g : grammar T} {n : g.nt} (h : n ∈ usedNTs g) : restrictNT g n = ⟨n, h⟩

@[simp]

theorem restrictSym_terminal {T : Type} (g : grammar T) (t : T) : restrictSym g (symbol.terminal t) = symbol.terminal t

@[simp]

theorem embedSym_terminal {T : Type} (g : grammar T) (t : T) : embedSym g (symbol.terminal t) = symbol.terminal t

theorem restrictSym_embedSym {T : Type} (g : grammar T) (s : symbol T (UsedNT g)) : restrictSym g (embedSym g s) = s

theorem embedSym_restrictSym {T : Type} {g : grammar T} {s : symbol T g.nt} (h : ∀ (n : g.nt), s = symbol.nonterminal n → n ∈ usedNTs g) : embedSym g (restrictSym g s) = s

The allNTsUsed predicate

def allNTsUsed {T : Type} (g : grammar T) (l : List (symbol T g.nt)) : Prop

All nonterminals in a symbol list belong to usedNTs g.

Equations

• allNTsUsed g l = ∀ (n : g.nt), symbol.nonterminal n ∈ l → n ∈ usedNTs g

theorem allNTsUsed_nil {T : Type} (g : grammar T) : allNTsUsed g []

theorem allNTsUsed_append {T : Type} {g : grammar T} {l₁ l₂ : List (symbol T g.nt)} : allNTsUsed g (l₁ ++ l₂) ↔ allNTsUsed g l₁ ∧ allNTsUsed g l₂

theorem allNTsUsed_singleton_nonterminal {T : Type} {g : grammar T} {n : g.nt} : allNTsUsed g [symbol.nonterminal n] ↔ n ∈ usedNTs g

theorem allNTsUsed_initial {T : Type} (g : grammar T) : allNTsUsed g [symbol.nonterminal g.initial]

theorem allNTsUsed_of_rule_input_L {T : Type} {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : allNTsUsed g r.input_L

theorem allNTsUsed_of_rule_input_R {T : Type} {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : allNTsUsed g r.input_R

theorem allNTsUsed_of_rule_output {T : Type} {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : allNTsUsed g r.output_string

Roundtrip properties for lists

theorem map_embedSym_map_restrictSym {T : Type} {g : grammar T} {l : List (symbol T g.nt)} (h : allNTsUsed g l) : List.map (embedSym g) (List.map (restrictSym g) l) = l

theorem map_restrictSym_map_embedSym {T : Type} (g : grammar T) (l : List (symbol T (UsedNT g))) : List.map (restrictSym g) (List.map (embedSym g) l) = l

theorem map_restrictSym_terminal {T : Type} (g : grammar T) (w : List T) : List.map (restrictSym g) (List.map (fun (t : T) => symbol.terminal t) w) = List.map (fun (t : T) => symbol.terminal t) w

theorem map_embedSym_terminal {T : Type} (g : grammar T) (w : List T) : List.map (embedSym g) (List.map (fun (t : T) => symbol.terminal t) w) = List.map (fun (t : T) => symbol.terminal t) w

Preservation of allNTsUsed through derivations

theorem allNTsUsed_preserved_by_transform {T : Type} {g : grammar T} {u v : List (symbol T g.nt)} (ht : grammar_transforms g u v) (hu : allNTsUsed g u) : allNTsUsed g v

theorem allNTsUsed_preserved_by_derives {T : Type} {g : grammar T} {u v : List (symbol T g.nt)} (hd : grammar_derives g u v) (hu : allNTsUsed g u) : allNTsUsed g v

Rule membership in the restricted grammar

theorem restrictGrammar_rule_of_mem {T : Type} {g : grammar T} {r : grule T g.nt} (hr : r ∈ g.rules) : { input_L := List.map (restrictSym g) r.input_L, input_N := restrictNT g r.input_N, input_R := List.map (restrictSym g) r.input_R, output_string := List.map (restrictSym g) r.output_string } ∈ (restrictGrammar g).rules

theorem restrictGrammar_rule_mem {T : Type} {g : grammar T} {r' : grule T (UsedNT g)} (hr' : r' ∈ (restrictGrammar g).rules) : ∃ r ∈ g.rules, r'.input_L = List.map (restrictSym g) r.input_L ∧ r'.input_N = restrictNT g r.input_N ∧ r'.input_R = List.map (restrictSym g) r.input_R ∧ r'.output_string = List.map (restrictSym g) r.output_string

Derivation correspondence

theorem transforms_restrict {T : Type} {g : grammar T} {u v : List (symbol T g.nt)} (ht : grammar_transforms g u v) (_hu : allNTsUsed g u) : grammar_transforms (restrictGrammar g) (List.map (restrictSym g) u) (List.map (restrictSym g) v)

theorem derives_restrict {T : Type} {g : grammar T} {u v : List (symbol T g.nt)} (hd : grammar_derives g u v) (hu : allNTsUsed g u) : grammar_derives (restrictGrammar g) (List.map (restrictSym g) u) (List.map (restrictSym g) v)

theorem transforms_embed {T : Type} {g : grammar T} {u v : List (symbol T (UsedNT g))} (ht : grammar_transforms (restrictGrammar g) u v) : grammar_transforms g (List.map (embedSym g) u) (List.map (embedSym g) v)

theorem derives_embed {T : Type} {g : grammar T} {u v : List (symbol T (UsedNT g))} (hd : grammar_derives (restrictGrammar g) u v) : grammar_derives g (List.map (embedSym g) u) (List.map (embedSym g) v)

Main theorem

theorem grammar_language_eq_restrictGrammar {T : Type} (g : grammar T) : grammar_language g = grammar_language (restrictGrammar g)

theorem grammar_equivalent_finiteNT {T : Type} (g : grammar T) : ∃ (g' : grammar T), Finite g'.nt ∧ grammar_language g = grammar_language g'

Every unrestricted grammar is equivalent to one with finitely many nonterminals.