Context-Free Grammars

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.

Main theorems

• Language.IsContextFree.reverse: The class of context-free languages is closed under reversal.

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.

theorem ContextFreeRule.ext {T : Type uT} {N : Type uN} {x y : ContextFreeRule T N} (input : x.input = y.input) (output : x.output = y.output) : x = y

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 : self.NT

  Initial nonterminal.

• rules : Finset (ContextFreeRule T self.NT)

  Rewrite rules.

inductive ContextFreeRule.Rewrites {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) : 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).

• head: ∀ {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} (s : List (Symbol T N)), r.Rewrites (Symbol.nonterminal r.input :: s) (r.output ++ s)

  The replacement is at the start of the remaining string.

• cons: ∀ {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} (x : Symbol T N) {s₁ s₂ : List (Symbol T N)}, r.Rewrites s₁ s₂ → r.Rewrites (x :: s₁) (x :: s₂)

  There is a replacement later in the string.

theorem ContextFreeRule.Rewrites.exists_parts {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hr : r.Rewrites u v) : ∃ (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.input_output {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} : r.Rewrites [Symbol.nonterminal r.input] r.output

theorem ContextFreeRule.rewrites_of_exists_parts {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) (p q : List (Symbol T N)) : r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

theorem ContextFreeRule.rewrites_iff {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.Rewrites u v ↔ ∃ (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.

theorem ContextFreeRule.Rewrites.append_left {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hvw : r.Rewrites u v) (p : List (Symbol T N)) : r.Rewrites (p ++ u) (p ++ v)

Add extra prefix to context-free rewriting.

theorem ContextFreeRule.Rewrites.append_right {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hvw : r.Rewrites u v) (p : List (Symbol T N)) : r.Rewrites (u ++ p) (v ++ p)

Add extra postfix to context-free rewriting.

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

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

• g.Produces u v = ∃ r ∈ g.rules, r.Rewrites u v

@[reducible, inline]

abbrev ContextFreeGrammar.Derives {T : Type uT} (g : ContextFreeGrammar T) : 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

• g.Derives = Relation.ReflTransGen g.Produces

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

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

• g.Generates s = g.Derives [Symbol.nonterminal g.initial] s

def ContextFreeGrammar.language {T : Type uT} (g : ContextFreeGrammar T) : Language T

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

Equations

• g.language = {w : List T | g.Generates (List.map Symbol.terminal w)}

@[simp]

theorem ContextFreeGrammar.mem_language_iff {T : Type uT} (g : ContextFreeGrammar T) (w : List T) : w ∈ g.language ↔ g.Derives [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 : ContextFreeGrammar T} (w : List (Symbol T g.NT)) : g.Derives w w

theorem ContextFreeGrammar.Produces.single {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) : g.Derives v w

theorem ContextFreeGrammar.Derives.trans {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Derives v w) : g.Derives u w

theorem ContextFreeGrammar.Derives.trans_produces {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Produces v w) : g.Derives u w

theorem ContextFreeGrammar.Produces.trans_derives {T : Type uT} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hvw : g.Derives v w) : g.Derives u w

theorem ContextFreeGrammar.Derives.eq_or_head {T : Type uT} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} (huw : g.Derives u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.Derives v w

theorem ContextFreeGrammar.Derives.eq_or_tail {T : Type uT} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} (huw : g.Derives u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Derives u v ∧ g.Produces v w

theorem ContextFreeGrammar.Produces.append_left {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) (p : List (Symbol T g.NT)) : g.Produces (p ++ v) (p ++ w)

Add extra prefix to context-free producing.

theorem ContextFreeGrammar.Produces.append_right {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) (p : List (Symbol T g.NT)) : g.Produces (v ++ p) (w ++ p)

Add extra postfix to context-free producing.

theorem ContextFreeGrammar.Derives.append_left {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Derives v w) (p : List (Symbol T g.NT)) : g.Derives (p ++ v) (p ++ w)

Add extra prefix to context-free deriving.

theorem ContextFreeGrammar.Derives.append_right {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Derives v w) (p : List (Symbol T g.NT)) : g.Derives (v ++ p) (w ++ p)

Add extra postfix to context-free deriving.

def Language.IsContextFree {T : Type uT} (L : Language T) : Prop

Context-free languages are defined by context-free grammars.

Equations

• L.IsContextFree = ∃ (g : ContextFreeGrammar T), g.language = L

def ContextFreeRule.reverse {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) : ContextFreeRule T N

Rules for a grammar for a reversed language.

Equations

• r.reverse = { input := r.input, output := r.output.reverse }

@[simp]

theorem ContextFreeRule.reverse_reverse {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) : r.reverse.reverse = r

@[simp]

theorem ContextFreeRule.reverse_comp_reverse {T : Type uT} {N : Type uN} : ContextFreeRule.reverse ∘ ContextFreeRule.reverse = id

theorem ContextFreeRule.reverse_involutive {T : Type uT} {N : Type uN} : Function.Involutive ContextFreeRule.reverse

theorem ContextFreeRule.reverse_bijective {T : Type uT} {N : Type uN} : Function.Bijective ContextFreeRule.reverse

theorem ContextFreeRule.reverse_injective {T : Type uT} {N : Type uN} : Function.Injective ContextFreeRule.reverse

theorem ContextFreeRule.reverse_surjective {T : Type uT} {N : Type uN} : Function.Surjective ContextFreeRule.reverse

theorem ContextFreeRule.Rewrites.reverse {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.Rewrites u v → r.reverse.Rewrites u.reverse v.reverse

theorem ContextFreeRule.rewrites_reverse {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u v

@[simp]

theorem ContextFreeRule.rewrites_reverse_comm {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse

def ContextFreeGrammar.reverse {T : Type uT} (g : ContextFreeGrammar T) : ContextFreeGrammar T

Grammar for a reversed language.

Equations

• g.reverse = { NT := g.NT, initial := g.initial, rules := Finset.map { toFun := ContextFreeRule.reverse, inj' := ⋯ } g.rules }

@[simp]

theorem ContextFreeGrammar.reverse_NT {T : Type uT} (g : ContextFreeGrammar T) : g.reverse.NT = g.NT

@[simp]

theorem ContextFreeGrammar.reverse_initial {T : Type uT} (g : ContextFreeGrammar T) : g.reverse.initial = g.initial

@[simp]

theorem ContextFreeGrammar.reverse_rules {T : Type uT} (g : ContextFreeGrammar T) : g.reverse.rules = Finset.map { toFun := ContextFreeRule.reverse, inj' := ⋯ } g.rules

@[simp]

theorem ContextFreeGrammar.reverse_reverse {T : Type uT} (g : ContextFreeGrammar T) : g.reverse.reverse = g

theorem ContextFreeGrammar.reverse_involutive {T : Type uT} : Function.Involutive ContextFreeGrammar.reverse

theorem ContextFreeGrammar.reverse_bijective {T : Type uT} : Function.Bijective ContextFreeGrammar.reverse

theorem ContextFreeGrammar.reverse_injective {T : Type uT} : Function.Injective ContextFreeGrammar.reverse

theorem ContextFreeGrammar.reverse_surjective {T : Type uT} : Function.Surjective ContextFreeGrammar.reverse

theorem ContextFreeGrammar.produces_reverse {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} : g.reverse.Produces u.reverse v.reverse ↔ g.Produces u v

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

Alias of the reverse direction of ContextFreeGrammar.produces_reverse.

@[simp]

theorem ContextFreeGrammar.produces_reverse_comm {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} : g.reverse.Produces u v ↔ g.Produces u.reverse v.reverse

theorem ContextFreeGrammar.Derives.reverse {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (hg : g.Derives u v) : g.reverse.Derives u.reverse v.reverse

theorem ContextFreeGrammar.derives_reverse {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} : g.reverse.Derives u.reverse v.reverse ↔ g.Derives u v

@[simp]

theorem ContextFreeGrammar.derives_reverse_comm {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} : g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse

theorem ContextFreeGrammar.generates_reverse {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : g.reverse.Generates u.reverse ↔ g.Generates u

theorem ContextFreeGrammar.Generates.reverse {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : g.Generates u → g.reverse.Generates u.reverse

Alias of the reverse direction of ContextFreeGrammar.generates_reverse.

@[simp]

theorem ContextFreeGrammar.generates_reverse_comm {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : g.reverse.Generates u ↔ g.Generates u.reverse

@[simp]

theorem ContextFreeGrammar.language_reverse {T : Type uT} {g : ContextFreeGrammar T} : g.reverse.language = g.language.reverse

theorem Language.IsContextFree.reverse {T : Type uT} (L : Language T) : L.IsContextFree → L.reverse.IsContextFree

The class of context-free languages is closed under reversal.