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 #

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 : ContextFreeRule.Rewrites r 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)) :
        ContextFreeRule.Rewrites r (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)) :
        ContextFreeRule.Rewrites r 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 : ContextFreeRule.Rewrites r v w) (p : List (Symbol T N)) :

        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 : ContextFreeRule.Rewrites r v w) (p : List (Symbol T N)) :

        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
        Instances For
          @[inline, reducible]
          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
              Instances For
                @[simp]

                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.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 : ContextFreeGrammar.Derives g u v) (hvw : ContextFreeGrammar.Derives g 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 : ContextFreeGrammar.Produces g v w) (p : List (Symbol T g.NT)) :

                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 : ContextFreeGrammar.Produces g v w) (p : List (Symbol T g.NT)) :

                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 : ContextFreeGrammar.Derives g v w) (p : List (Symbol T g.NT)) :

                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 : ContextFreeGrammar.Derives g v w) (p : List (Symbol T g.NT)) :

                Add extra prefix to context-free deriving.