Symbols, rules and derivations of a context-free grammar

Lemmas on mathlib's Symbol, ContextFreeRule and ContextFreeGrammar that the derivation trees, the closure properties and the weighted grammars share. [UPSTREAM] candidate for Mathlib/Computability/ContextFreeGrammar.lean.

Main definitions

• Symbol.terminal?, Symbol.IsNonterminal, Symbol.mapNonterminal: the terminal at a symbol, the nonterminal predicate, and relabelling of nonterminals.
• ContextFreeRule.NonterminalPos: the positions of a right-hand side holding a nonterminal.
• ContextFreeGrammar.RulesWithLHS: the rules of a grammar with a given left-hand side.
• DFA.toContextFreeGrammar M: the right-linear grammar of a finite automaton over a finite alphabet.

Main results

• ContextFreeGrammar.Derives.append_split: a derivation from a concatenation splits into derivations from the two halves.
• ContextFreeGrammar.produces_map_terminal_append_singleton_append_iff: the one-step productions of a word with a single nonterminal, the step of linear grammars.
• ContextFreeGrammar.Derives.terminal_mem: a derivation introduces only terminals that occur in the output of a rule.
• DFA.language_toContextFreeGrammar: the right-linear grammar of M generates the language of M, so over a finite alphabet regular languages are context-free (Language.IsRegular.isContextFree).
• Language.isContextFree_top_iff: the language of all words is context-free exactly when the alphabet is finite.

Implementation notes

The right-linear grammar of a finite automaton M has a nonterminal for each state, a rule q → a q' for each transition from q to q' on the letter a, and a rule q → ε for each accepting state q; its sentential forms are a word w followed by the state M.eval w, or an accepted word. The alphabet must be finite, because a grammar has finitely many rules and so uses finitely many letters: over an infinite alphabet the language of all words is regular, by a one-state automaton, but not context-free.

References

• J. E. Hopcroft, R. Motwani and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (2000)

def Symbol.terminal? {T : Type u_1} {N : Type u_2} : Symbol T N → Option T

The terminal at a symbol, if it is one.

Equations

• (Symbol.terminal a).terminal? = some a
• (Symbol.nonterminal n).terminal? = none

@[simp]

theorem Symbol.terminal?_terminal {T : Type u_1} {N : Type u_2} (a : T) : (terminal a).terminal? = some a

@[simp]

theorem Symbol.terminal?_nonterminal {T : Type u_1} {N : Type u_2} (A : N) : (nonterminal A).terminal? = none

def Symbol.IsNonterminal {T : Type u_1} {N : Type u_2} : Symbol T N → Prop

The nonterminal symbols.

Equations

• (Symbol.terminal a).IsNonterminal = False
• (Symbol.nonterminal n).IsNonterminal = True

@[instance_reducible]

instance Symbol.instDecidablePredIsNonterminal {T : Type u_1} {N : Type u_2} : DecidablePred IsNonterminal

Equations

• (Symbol.terminal a).instDecidablePredIsNonterminal = isFalse ⋯
• (Symbol.nonterminal n).instDecidablePredIsNonterminal = isTrue trivial

@[simp]

theorem Symbol.isNonterminal_nonterminal {T : Type u_1} {N : Type u_2} (A : N) : (nonterminal A).IsNonterminal

@[simp]

theorem Symbol.not_isNonterminal_terminal {T : Type u_1} {N : Type u_2} (a : T) : ¬(terminal a).IsNonterminal

theorem Symbol.isNonterminal_iff_terminal?_eq_none {T : Type u_1} {N : Type u_2} (s : Symbol T N) : s.IsNonterminal ↔ s.terminal? = none

def Symbol.mapNonterminal {T : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') : Symbol T N → Symbol T N'

Relabel the nonterminals of a symbol.

Equations

• Symbol.mapNonterminal f (Symbol.terminal a) = Symbol.terminal a
• Symbol.mapNonterminal f (Symbol.nonterminal n) = Symbol.nonterminal (f n)

@[simp]

theorem Symbol.mapNonterminal_terminal {T : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') (a : T) : mapNonterminal f (terminal a) = terminal a

@[simp]

theorem Symbol.mapNonterminal_nonterminal {T : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') (A : N) : mapNonterminal f (nonterminal A) = nonterminal (f A)

@[simp]

theorem Symbol.terminal?_mapNonterminal {T : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') (s : Symbol T N) : (mapNonterminal f s).terminal? = s.terminal?

instance Symbol.instCountable_linglib {T : Type u_1} {N : Type u_2} [Countable T] [Countable N] : Countable (Symbol T N)

@[reducible, inline]

abbrev ContextFreeRule.NonterminalPos {T : Type u_1} {N : Type u_2} (r : ContextFreeRule T N) : Type

The positions on the right-hand side of r that hold a nonterminal: the slots at which a derivation from r branches.

Equations

• r.NonterminalPos = { i : Fin r.output.length // r.output[i].IsNonterminal }

theorem ContextFreeRule.Rewrites.append_split {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u₁ u₂ v : List (Symbol T N)} : r.Rewrites (u₁ ++ u₂) v → (∃ (v₁ : List (Symbol T N)), v = v₁ ++ u₂ ∧ r.Rewrites u₁ v₁) ∨ ∃ (v₂ : List (Symbol T N)), v = u₁ ++ v₂ ∧ r.Rewrites u₂ v₂

A rewrite of a concatenation u₁ ++ u₂ happens entirely in u₁ or entirely in u₂.

theorem ContextFreeRule.Rewrites.not_map_terminal {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {w : List T} {v : List (Symbol T N)} : ¬r.Rewrites (List.map Symbol.terminal w) v

No rule rewrites a word of terminals.

theorem ContextFreeRule.rewrites_map_terminal_append_singleton_append_iff {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {A : N} {w u : List T} {v : List (Symbol T N)} : r.Rewrites (List.map Symbol.terminal w ++ [Symbol.nonterminal A] ++ List.map Symbol.terminal u) v ↔ r.input = A ∧ v = List.map Symbol.terminal w ++ r.output ++ List.map Symbol.terminal u

A rewrite of a word with a single nonterminal replaces that nonterminal by the output of a rule with that input.

@[reducible, inline]

abbrev ContextFreeGrammar.RulesWithLHS {T : Type u_1} (g : ContextFreeGrammar T) [DecidableEq g.NT] (a : g.NT) : Type u_1

The rules of g with left-hand side a.

Equations

• g.RulesWithLHS a = ↥({x ∈ g.rules | x.input = a})

theorem ContextFreeGrammar.Produces.append_split {T : Type u_1} {g : ContextFreeGrammar T} {u₁ u₂ v : List (Symbol T g.NT)} (h : g.Produces (u₁ ++ u₂) v) : (∃ (v₁ : List (Symbol T g.NT)), v = v₁ ++ u₂ ∧ g.Produces u₁ v₁) ∨ ∃ (v₂ : List (Symbol T g.NT)), v = u₁ ++ v₂ ∧ g.Produces u₂ v₂

A production from a concatenation u₁ ++ u₂ happens entirely in u₁ or entirely in u₂.

theorem ContextFreeGrammar.Derives.append_split {T : Type u_1} {g : ContextFreeGrammar T} {u₁ u₂ v : List (Symbol T g.NT)} (h : g.Derives (u₁ ++ u₂) v) : ∃ (v₁ : List (Symbol T g.NT)) (v₂ : List (Symbol T g.NT)), v = v₁ ++ v₂ ∧ g.Derives u₁ v₁ ∧ g.Derives u₂ v₂

A derivation from a concatenation u₁ ++ u₂ splits into derivations from u₁ and from u₂.

theorem ContextFreeGrammar.not_produces_map_terminal {T : Type u_1} {g : ContextFreeGrammar T} {w : List T} {v : List (Symbol T g.NT)} : ¬g.Produces (List.map Symbol.terminal w) v

A word of terminals produces nothing.

theorem ContextFreeGrammar.produces_map_terminal_append_singleton_append_iff {T : Type u_1} {g : ContextFreeGrammar T} {A : g.NT} {w u : List T} {v : List (Symbol T g.NT)} : g.Produces (List.map Symbol.terminal w ++ [Symbol.nonterminal A] ++ List.map Symbol.terminal u) v ↔ ∃ r ∈ g.rules, r.input = A ∧ v = List.map Symbol.terminal w ++ r.output ++ List.map Symbol.terminal u

A word with a single nonterminal produces exactly the words obtained by replacing that nonterminal with the output of one of its rules.

theorem ContextFreeGrammar.produces_map_terminal_append_singleton_iff {T : Type u_1} {g : ContextFreeGrammar T} {A : g.NT} {w : List T} {v : List (Symbol T g.NT)} : g.Produces (List.map Symbol.terminal w ++ [Symbol.nonterminal A]) v ↔ ∃ r ∈ g.rules, r.input = A ∧ v = List.map Symbol.terminal w ++ r.output

A word ending in its only nonterminal produces exactly the words obtained by replacing that nonterminal with the output of one of its rules, the step of right-linear grammars.

theorem ContextFreeGrammar.Derives.terminal_mem {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (h : g.Derives u v) {a : T} (ha : Symbol.terminal a ∈ v) : Symbol.terminal a ∈ u ∨ ∃ r ∈ g.rules, Symbol.terminal a ∈ r.output

A terminal of a derived word is a terminal of the source word or of the output of a rule.

Regular languages

def DFA.toContextFreeGrammar {α : Type u_1} {σ : Type} [Fintype α] [Fintype σ] (M : DFA α σ) [DecidablePred fun (x : σ) => x ∈ M.accept] : ContextFreeGrammar α

The right-linear grammar of M: a nonterminal for each state, a rule q → a (M.step q a) for each state q and letter a, and a rule q → ε for each accepting state q.

Equations

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

theorem DFA.mem_rules_toContextFreeGrammar {α : Type u_1} {σ : Type} [Fintype α] [Fintype σ] {M : DFA α σ} [DecidablePred fun (x : σ) => x ∈ M.accept] {r : ContextFreeRule α σ} : r ∈ M.toContextFreeGrammar.rules ↔ (∃ (a : α), r.output = [Symbol.terminal a, Symbol.nonterminal (M.step r.input a)]) ∨ r.input ∈ M.accept ∧ r.output = []

theorem DFA.derives_toContextFreeGrammar {α : Type u_1} {σ : Type} [Fintype α] [Fintype σ] {M : DFA α σ} [DecidablePred fun (x : σ) => x ∈ M.accept] (w : List α) : M.toContextFreeGrammar.Derives [Symbol.nonterminal M.start] (List.map Symbol.terminal w ++ [Symbol.nonterminal (M.eval w)])

The grammar of M derives every word followed by the state M reaches on it.

theorem DFA.derives_toContextFreeGrammar_iff {α : Type u_1} {σ : Type} [Fintype α] [Fintype σ] {M : DFA α σ} [DecidablePred fun (x : σ) => x ∈ M.accept] {v : List (Symbol α σ)} : M.toContextFreeGrammar.Derives [Symbol.nonterminal M.start] v ↔ ∃ (w : List α), v = List.map Symbol.terminal w ++ [Symbol.nonterminal (M.eval w)] ∨ v = List.map Symbol.terminal w ∧ M.eval w ∈ M.accept

The sentential forms of the grammar of M are a word followed by the state M reaches on it, and the words M accepts.

theorem DFA.language_toContextFreeGrammar {α : Type u_1} {σ : Type} [Fintype α] [Fintype σ] {M : DFA α σ} [DecidablePred fun (x : σ) => x ∈ M.accept] : M.toContextFreeGrammar.language = M.accepts

The grammar of M generates the language of M.

theorem Language.IsRegular.isContextFree {α : Type u_1} [Finite α] {L : Language α} (h : L.IsRegular) : L.IsContextFree

Over a finite alphabet, every regular language is context-free.

theorem Language.isContextFree_top_iff {α : Type u_1} : ⊤.IsContextFree ↔ Finite α

The language of all words is context-free exactly when the alphabet is finite: it is regular over any alphabet, but a grammar has finitely many rules and so uses finitely many letters.