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.

We restrict nonterminals of a context-free grammar to Type because universe polymorphism would be cumbersome and unnecessary; we can always restrict a context-free grammar to the finitely many nonterminal symbols that are referred to by its finitely many rules.

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 u_1) (N : Type u_2) : Type (max u_1 u_2)

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 u_1} {N : Type u_2} {x y : ContextFreeRule T N} (input : x.input = y.input) (output : x.output = y.output) : x = y

theorem ContextFreeRule.ext_iff {T : Type u_1} {N : Type u_2} {x y : ContextFreeRule T N} : x = y ↔ x.input = y.input ∧ x.output = y.output

instance instDecidableEqContextFreeRule {T✝ : Type u_1} {N✝ : Type u_2} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (ContextFreeRule T✝ N✝)

Equations

• instDecidableEqContextFreeRule = decEqContextFreeRule✝

instance instReprContextFreeRule {T✝ : Type u_1} {N✝ : Type u_2} [Repr T✝] [Repr N✝] : Repr (ContextFreeRule T✝ N✝)

Equations

• instReprContextFreeRule = { reprPrec := reprContextFreeRule✝ }

structure ContextFreeGrammar (T : Type u_1) : Type (max 1 u_1)

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

• NT : Type

  Type of nonterminals.

• initial : self.NT

  Initial nonterminal.

• rules : Finset (ContextFreeRule T self.NT)

  Rewrite rules.

inductive ContextFreeRule.Rewrites {T : Type u_1} {N : Type u_2} (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 u_1} {N : Type u_2} {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 u_1} {N : Type u_2} {r : ContextFreeRule T N} (x : Symbol T N) {s₁ s₂ : List (Symbol T N)} (hrs : 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 u_1} {N : Type u_2} {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 u_1} {N : Type u_2} {r : ContextFreeRule T N} : r.Rewrites [Symbol.nonterminal r.input] r.output

theorem ContextFreeRule.rewrites_of_exists_parts {T : Type u_1} {N : Type u_2} (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 u_1} {N : Type u_2} {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.nonterminal_input_mem {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)} : r.Rewrites u v → Symbol.nonterminal r.input ∈ u

theorem ContextFreeRule.Rewrites.append_left {T : Type u_1} {N : Type u_2} {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 u_1} {N : Type u_2} {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 u_1} (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 u_1} (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 u_1} (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 u_1} (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 u_1} (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 u_1} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)) : g.Derives w w

theorem ContextFreeGrammar.Produces.single {T : Type u_1} {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 u_1} {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 u_1} {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 u_1} {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 u_1} {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_iff_eq_or_head {T : Type u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} : 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 u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)} (huw : g.Derives u w) : w = u ∨ ∃ (v : List (Symbol T g.NT)), g.Derives u v ∧ g.Produces v w

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

theorem ContextFreeGrammar.Produces.append_left {T : Type u_1} {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 u_1} {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 u_1} {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 u_1} {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.

theorem ContextFreeGrammar.Produces.exists_nonterminal_input_mem {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} (hguv : g.Produces u v) : ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

theorem ContextFreeGrammar.derives_nonterminal {T : Type u_1} {g : ContextFreeGrammar T} {t : g.NT} (hgt : ∀ r ∈ g.rules, r.input ≠ t) (s : List (Symbol T g.NT)) (hs : s ≠ [Symbol.nonterminal t]) : ¬g.Derives [Symbol.nonterminal t] s

theorem ContextFreeGrammar.language_eq_zero_of_forall_input_ne_initial {T : Type u_1} {g : ContextFreeGrammar T} (hg : ∀ r ∈ g.rules, r.input ≠ g.initial) : g.language = 0

def Language.IsContextFree {T : Type u_1} (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 u_1} {N : Type u_2} (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 u_1} {N : Type u_2} (r : ContextFreeRule T N) : r.reverse.reverse = r

@[simp]

theorem ContextFreeRule.reverse_comp_reverse {T : Type u_1} {N : Type u_2} : reverse ∘ reverse = id

theorem ContextFreeRule.reverse_involutive {T : Type u_1} {N : Type u_2} : Function.Involutive reverse

theorem ContextFreeRule.reverse_bijective {T : Type u_1} {N : Type u_2} : Function.Bijective reverse

theorem ContextFreeRule.reverse_injective {T : Type u_1} {N : Type u_2} : Function.Injective reverse

theorem ContextFreeRule.reverse_surjective {T : Type u_1} {N : Type u_2} : Function.Surjective reverse

theorem ContextFreeRule.Rewrites.reverse {T : Type u_1} {N : Type u_2} {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 u_1} {N : Type u_2} {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 u_1} {N : Type u_2} {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 u_1} (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_rules {T : Type u_1} (g : ContextFreeGrammar T) : g.reverse.rules = Finset.map { toFun := ContextFreeRule.reverse, inj' := ⋯ } g.rules

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem ContextFreeGrammar.produces_reverse {T : Type u_1} {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 u_1} {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 u_1} {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 u_1} {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 u_1} {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 u_1} {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 u_1} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : g.reverse.Generates u.reverse ↔ g.Generates u

theorem ContextFreeGrammar.Generates.reverse {T : Type u_1} {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 u_1} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : g.reverse.Generates u ↔ g.Generates u.reverse

@[simp]

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

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

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