File CoMoLang.RG

Require Import List.

From CoMoLang Require Import Languages Grammars CFG.

A regular grammar (RG) is a CFG, where the right side of rules is very stricted (see below).

Class RG (V Sigma : Set) :=
  {
    RG_CFG :> CFG V Sigma;
    rule_right_side :
      ∀ t1 t2,
        @rule V Sigma (@CFG_Grammar V Sigma RG_CFG) t1 t2 →
        (∃ c v ,
        t2 = (inr c ) :: (inl v ) :: nil

One char followed by a variable at the right side

        ) ∨
        (∃ c ,
        t2 = (inr c ) :: nil

One char at the right side

) ∨
t2 = nil

The empty term

Just a helper, which gives us directly the base grammar to a RG.

Definition RG_Grammar {V Sigma} `(G : RG V Sigma) : Grammar V Sigma.
Proof.
destruct RG_CFG; assumption.
Defined.

A language L is called regular, if a RG exists, which produces L.

Definition is_regular {Sigma} `(L : Language Sigma) : Prop :=
∃ (V : Set) `(G : RG V Sigma ),
grammar_produces (RG_Grammar G) L.