# Documentation

Mathlib.Computability.ContextFreeGrammar

# Context-Free Grammar #

This file contains the definition of a context-free grammar, which is a grammar that has a single nonterminal symbol on the left-hand side of each rule.

## Main definitions #

• ContextFreeGrammar: A context-free grammar.
• ContextFreeGrammar.language: A language generated by a given context-free grammar.
structure ContextFreeRule (T : Type uT) (N : Type uN) :
Type (max uN uT)

Rule that rewrites a single nonterminal to any string (a list of symbols).

• input : N

Input nonterminal a.k.a. left-hand side.

• output : List (Symbol T N)

Output string a.k.a. right-hand side.

Instances For
structure ContextFreeGrammar (T : Type uT) :
Type (max (uN + 1) uT)

Context-free grammar that generates words over the alphabet T (a type of terminals).

• NT : Type uN

Type of nonterminals.

• initial : s.NT

Initial nonterminal.

• rules : List (ContextFreeRule T s.NT)

Rewrite rules.

Instances For
inductive ContextFreeRule.Rewrites {T : Type uT} {N : Type uN} (r : ) :
List (Symbol T N)List (Symbol T N)Prop

Inductive definition of a single application of a given context-free rule r to a string u; r.Rewrites u v means that the r sends u to v (there may be multiple such strings v).

Instances For
theorem ContextFreeRule.Rewrites.exists_parts {T : Type uT} {N : Type uN} {r : } {u : List (Symbol T N)} {v : List (Symbol T N)} (hyp : ) :
∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q v = p ++ r.output ++ q
theorem ContextFreeRule.rewrites_of_exists_parts {T : Type uT} {N : Type uN} (r : ) (p : List (Symbol T N)) (q : List (Symbol T N)) :
ContextFreeRule.Rewrites r (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
theorem ContextFreeRule.rewrites_iff {T : Type uT} {N : Type uN} {r : } (u : List (Symbol T N)) (v : List (Symbol T N)) :
∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q v = p ++ r.output ++ q

Rule r rewrites string u is to string v iff they share both a prefix p and postfix q such that the remaining middle part of u is the input of r and the remaining middle part of u is the output of r.

def ContextFreeGrammar.Produces {T : Type uT} (g : ) (u : List (Symbol T g.NT)) (v : List (Symbol T g.NT)) :

Given a context-free grammar g and strings u and v g.Produces u v means that one step of a context-free transformation by a rule from g sends u to v.

Equations
• = ∃ r ∈ g.rules,
Instances For
@[inline, reducible]
abbrev ContextFreeGrammar.Derives {T : Type uT} (g : ) :
List (Symbol T g.NT)List (Symbol T g.NT)Prop

Given a context-free grammar g and strings u and v g.Derives u v means that g can transform u to v in some number of rewriting steps.

Equations
Instances For
def ContextFreeGrammar.Generates {T : Type uT} (g : ) (s : List (Symbol T g.NT)) :

Given a context-free grammar g and a string s g.Generates s means that g can transform its initial nonterminal to s in some number of rewriting steps.

Equations
Instances For
def ContextFreeGrammar.language {T : Type uT} (g : ) :

The language (set of words) that can be generated by a given context-free grammar g.

Equations
Instances For
@[simp]
theorem ContextFreeGrammar.mem_language_iff {T : Type uT} (g : ) (w : List T) :
ContextFreeGrammar.Derives g [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)

A given word w belongs to the language generated by a given context-free grammar g iff g can derive the word w (wrapped as a string) from the initial nonterminal of g in some number of steps.

theorem ContextFreeGrammar.Derives.refl {T : Type uT} {g : } (w : List (Symbol T g.NT)) :
theorem ContextFreeGrammar.Produces.single {T : Type uT} {g : } {v : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (hvw : ) :
theorem ContextFreeGrammar.Derives.trans {T : Type uT} {g : } {u : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (huv : ) (hvw : ) :
theorem ContextFreeGrammar.Derives.trans_produces {T : Type uT} {g : } {u : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (huv : ) (hvw : ) :
theorem ContextFreeGrammar.Produces.trans_derives {T : Type uT} {g : } {u : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (huv : ) (hvw : ) :
theorem ContextFreeGrammar.Derives.eq_or_head {T : Type uT} {g : } {u : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (huw : ) :
u = w ∃ (v : List (Symbol T g.NT)),
theorem ContextFreeGrammar.Derives.eq_or_tail {T : Type uT} {g : } {u : List (Symbol T g.NT)} {w : List (Symbol T g.NT)} (huw : ) :
u = w ∃ (v : List (Symbol T g.NT)),