Terminal Restriction for CFGs

This file replaces long mixed right-hand sides by rules that isolate terminals in preparation for Chomsky normal form.

Main declarations

• restrictTerminals_correct

def embedSymbol {T : Type} {N : Type uN} (s : Symbol T N) : Symbol T (N ⊕ T)

Intuitive embedding of symbols of the original grammar into symbols of the new grammar's type

Equations

• embedSymbol (Symbol.terminal t) = Symbol.terminal t
• embedSymbol (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl n)

@[reducible, inline]

abbrev embedString {T : Type} {N : Type uN} (u : List (Symbol T N)) : List (Symbol T (N ⊕ T))

Intuitive embedding of strings of the original grammar into strings of the new grammar's type

Equations

• embedString u = List.map embedSymbol u

def rightEmbedSymbol {T : Type} {N : Type uN} (s : Symbol T N) : Symbol T (N ⊕ T)

Embedding of symbols of the original grammar into nonterminals of the new grammar

Equations

• rightEmbedSymbol (Symbol.terminal t) = Symbol.nonterminal (Sum.inr t)
• rightEmbedSymbol (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl n)

@[reducible, inline]

abbrev rightEmbedString {T : Type} {N : Type uN} (w : List (Symbol T N)) : List (Symbol T (N ⊕ T))

Embedding of strings of the original grammar into nonterminal (symbol) strings of the new grammar

Equations

• rightEmbedString w = List.map rightEmbedSymbol w

def projectSymbol {T : Type} {N : Type uN} (s : Symbol T (N ⊕ T)) : Symbol T N

Projection from symbols of the new grammars type into symbols of the original grammar

Equations

• projectSymbol (Symbol.terminal t) = Symbol.terminal t
• projectSymbol (Symbol.nonterminal (Sum.inl nt)) = Symbol.nonterminal nt
• projectSymbol (Symbol.nonterminal (Sum.inr t)) = Symbol.terminal t

def projectString {T : Type} {N : Type uN} (u : List (Symbol T (N ⊕ T))) : List (Symbol T N)

Projection from strings of the new grammars type into strings of the original grammar

Equations

• projectString u = List.map projectSymbol u

theorem projectString_rightEmbedString_id {T : Type} {N : Type uN} {u : List (Symbol T N)} : projectString (rightEmbedString u) = u

theorem projectString_terminals {T : Type} {N : Type uN} {u : List T} : projectString (List.map Symbol.terminal u) = List.map Symbol.terminal u

theorem projectSymbol_nonterminal {T : Type} {N : Type uN} {n : N} : projectSymbol (Symbol.nonterminal (Sum.inl n)) = Symbol.nonterminal n

theorem embedString_terminals {T : Type} {N : Type uN} {u : List T} : embedString (List.map Symbol.terminal u) = List.map Symbol.terminal u

theorem embedString_append {T : Type} {N : Type uN} {u v : List (Symbol T N)} : embedString (u ++ v) = embedString u ++ embedString v

theorem rightEmbed_string_nonUnit {T : Type} {N : Type uN} {u : List (Symbol T N)} (hu : ContextFreeGrammar.NonUnit u) (hut : ∀ (t : T), u ≠ [Symbol.terminal t]) : ContextFreeGrammar.NonUnit (rightEmbedString u)

def ContextFreeGrammar.newTerminalRules {T : Type} {N : Type u_1} (r : ContextFreeRule T N) : List (ContextFreeRule T (N ⊕ T))

Computes rules r' : T -> t, for all terminals t occuring in r.output

Equations

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

def ContextFreeGrammar.restrictTerminalRule {T : Type} {N : Type u_1} (r : ContextFreeRule T N) : List (ContextFreeRule T (N ⊕ T))

If r.output is a single terminal, we lift the rule to the new grammar, otherwise add new rules for each terminal symbol in r.output and right-lift the rule, i.e., replace all terminals with nonterminals

Equations

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

noncomputable def ContextFreeGrammar.restrictTerminalRules {T : Type} {N : Type u_1} [DecidableEq T] [DecidableEq N] (l : List (ContextFreeRule T N)) : Finset (ContextFreeRule T (N ⊕ T))

Compute all lifted rules

Equations

• ContextFreeGrammar.restrictTerminalRules l = (List.map ContextFreeGrammar.restrictTerminalRule l).flatten.toFinset

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

Construct new grammar, using the lifted rules. Each rule's output is either a single terminal or only nonterminals

Equations

• g.restrictTerminals = { NT := g.NT ⊕ T, initial := Sum.inl g.initial, rules := ContextFreeGrammar.restrictTerminalRules g.rules.toList }

theorem ContextFreeGrammar.restrictTerminalRule_right_terminal_output {T : Type} {g : ContextFreeGrammar T} {t : T} {r : ContextFreeRule T g.NT} {r' : ContextFreeRule T (g.NT ⊕ T)} (hrr : r' ∈ restrictTerminalRule r) (hrt : r'.input = Sum.inr t) : r'.output = [Symbol.terminal t]

theorem ContextFreeGrammar.restrictTerminalRules_right_terminal_output {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {t : T} {r : ContextFreeRule T (g.NT ⊕ T)} (hrg : r ∈ restrictTerminalRules g.rules.toList) (hrt : r.input = Sum.inr t) : r.output = [Symbol.terminal t]

theorem ContextFreeGrammar.restrictTerminalRule_left {T : Type} {g : ContextFreeGrammar T} {n : g.NT} {r : ContextFreeRule T g.NT} {r' : ContextFreeRule T (g.NT ⊕ T)} (hrr : r' ∈ restrictTerminalRule r) (hrn : r'.input = Sum.inl n) : r.input = n ∧ r.output = projectString r'.output

theorem ContextFreeGrammar.terminal_mem_newTerminalRules {T : Type} {g : ContextFreeGrammar T} {t : T} {r : ContextFreeRule T g.NT} (htr : Symbol.terminal t ∈ r.output) : { input := Sum.inr t, output := [Symbol.terminal t] } ∈ newTerminalRules r

theorem ContextFreeGrammar.restrictTerminalsRules_left {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {n : g.NT} {r' : ContextFreeRule T (g.NT ⊕ T)} (hrg : r' ∈ restrictTerminalRules g.rules.toList) (hrn : r'.input = Sum.inl n) : ∃ r ∈ g.rules, r.input = n ∧ r.output = projectString r'.output

theorem ContextFreeGrammar.restrictTerminals_produces_derives_projectString {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u v : List (Symbol T (g.NT ⊕ T))} (huv : g.restrictTerminals.Produces u v) : g.Derives (projectString u) (projectString v)

theorem ContextFreeGrammar.restrictTerminals_derives_derives_projectString {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u v : List (Symbol T (g.NT ⊕ T))} (huv : g.restrictTerminals.Derives u v) : g.Derives (projectString u) (projectString v)

theorem ContextFreeGrammar.restrictTerminals_derives_rightEmbedString_embedString {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u : List (Symbol T g.NT)} (hu : ∀ (t : T), Symbol.terminal t ∈ u → ∃ r ∈ g.rules, Symbol.terminal t ∈ r.output) : g.restrictTerminals.Derives (rightEmbedString u) (embedString u)

theorem ContextFreeGrammar.derives_restrictTerminals_derives_embedString {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.Derives u v) : g.restrictTerminals.Derives (embedString u) (embedString v)

theorem ContextFreeGrammar.restrictTerminals_correct {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] : g.language = g.restrictTerminals.language