Documentation

Mathlib.Computability.ContextFreeGrammar

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 #

Main theorems #

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

      Initial nonterminal.

    • rules : List (ContextFreeRule T self.NT)

      Rewrite rules.

    Instances For
      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).

      Instances For
        theorem ContextFreeRule.Rewrites.exists_parts {T : Type uT} {N : Type uN} {r : ContextFreeRule T N} {u : List (Symbol T N)} {v : List (Symbol T N)} (hyp : 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_of_exists_parts {T : Type uT} {N : Type uN} (r : ContextFreeRule T N) (p : List (Symbol T N)) (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 : List (Symbol T N)) (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} {v : List (Symbol T N)} {w : List (Symbol T N)} (hvw : r.Rewrites v w) (p : List (Symbol T N)) :
        r.Rewrites (p ++ v) (p ++ w)

        Add extra prefix to context-free rewriting.

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

        Add extra postfix to context-free rewriting.

        def ContextFreeGrammar.Produces {T : Type uT} (g : ContextFreeGrammar T) (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
        • g.Produces u v = rg.rules, r.Rewrites u v
        Instances For
          @[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
          Instances For

            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

              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)}
              Instances For
                @[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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {v : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 : List (Symbol T g.NT)} {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 prefix to context-free deriving.

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

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

                  Rules for a grammar for a reversed language.

                  Equations
                  • r.reverse = { input := r.input, output := r.output.reverse }
                  Instances For

                    Grammar for a reversed language.

                    Equations
                    • g.reverse = { NT := g.NT, initial := g.initial, rules := List.map ContextFreeRule.reverse g.rules }
                    Instances For
                      theorem ContextFreeRule.reverse_involutive {T : Type uT} {N : Type uN} :
                      Function.Involutive ContextFreeRule.reverse
                      theorem ContextFreeGrammar.reverse_involutive {T : Type uT} :
                      Function.Involutive ContextFreeGrammar.reverse
                      theorem ContextFreeGrammar.reverse_derives {T : Type uT} (g : ContextFreeGrammar T) {s : List (Symbol T g.NT)} (hgs : g.reverse.Derives [Symbol.nonterminal g.reverse.initial] s) :
                      g.Derives [Symbol.nonterminal g.initial] s.reverse
                      theorem ContextFreeGrammar.reverse_mem_language_of_mem_reverse_language {T : Type uT} (g : ContextFreeGrammar T) {w : List T} (hgw : w g.reverse.language) :
                      w.reverse g.language
                      theorem ContextFreeGrammar.mem_reverse_language_iff_reverse_mem_language {T : Type uT} (g : ContextFreeGrammar T) (w : List T) :
                      w g.reverse.language w.reverse g.language
                      theorem Language.IsContextFree.reverse {T : Type uT} (L : Language T) :
                      L.IsContextFreeL.reverse.IsContextFree

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