Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Trying to make an conversion from a regular grammar to a finite automata

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Trying to make an conversion from a regular grammar to a finite automata


Chronological Thread 
  • From: Erick Simas Grilo <simas_grilo AT id.uff.br>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Trying to make an conversion from a regular grammar to a finite automata
  • Date: Fri, 19 May 2017 12:25:01 -0300
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=simas_grilo AT id.uff.br; spf=None smtp.mailfrom=simas_grilo AT id.uff.br; spf=None smtp.helo=postmaster AT mail-it0-f44.google.com
  • Ironport-phdr: 9a23:tjVIPBGX077km11NrLGF+p1GYnF86YWxBRYc798ds5kLTJ78oc2wAkXT6L1XgUPTWs2DsrQf2rSQ7v+oGTRZp83Q7zZaKN0EfiRGoPtVtjRjOvLNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMj4ZvLqc8xgHJr3ZKZu9awX9kKU+Jkxvy4sq9/oRv/zhMt/4k6sVNTbj0c6MkQLNXCzgrL3o76Mr3uxfdUACB/GEcUmIYkhpJBwjK8hT3VYrvvyX5q+RwxjCUMdX5Qr4oVzui6bxrSALzhyccKzE56mDXhddug69dvRmsugZww4/QYIGSKfp+YqbQds4USGZdQspcUTFKD4WhZIUNEuUBJ/5VoYnzqVUNsBWwGxWjCfj1xTNUnHL7x7E23/gjHAzAwQcuH8gOsHPRrNjtO6kSS+G1w7XLzT7ecv1W2DL955LTchs8oP+MR7Nwcc7WyUIyEA7FlVSQqYn/MDOOzusNvHKb7+tkVeKokGMnqhx+riKyxscihInFnJkaykrd+Ch/3Y07JsW4RVZlbdK4FJZcrSKXOotsTs88Xm1ltzw2x7IJtJO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpggXJqYrO/hxKr/Uih1u3wStC40FhFoydKiNXMuXcN1xvc6siDVPRx5Fuu2TGK1wzL6+FEJ147lbbDJpI/3rI9koAfvEfDEyPshkn6kaCbel8r9+Wn8+jnZ6/ppp6YN496kAH+NaEul9SkAeQ5NwgBRXOb9vyz1L35/E35RLJKg+Y3kqbEqpzaOMobpqCjDwBOyIYv8wy/ACu+0NQEgXkHK0pIdw6Aj4jwIl3BPPT4DeqkjFm3izdqx/XGPqX7DZnXL3jDlq3hfbdn5EJGxgoz14MX25UBAbYYZfn3R0XZtdrCDxZ/PRbn7fzgDYBQzIIVWiq0A6qQK+v9q16M4ap7OOiJbZQityz8L/8N5vKokHE331UHK/r6laALYWy1S6w1a36SZmDh148M

Hi there, I am a little bit new used to Coq and I am trying to formalize some of the regular aspects of regular languages. I already have a grammar that looks like this:

Record reg_grammar: Type:= {
    set_non_terminal : (list non_terminal);
    set_terminal : (list terminal);
    prod_rules: non_terminal -> sf -> Prop;
    start_symbol: non_terminal;
}.
which (ignoring the prod_rules type, which ends in prop,it is for other purposes) I have a list that has all the rules of the grammar that would look like this(e.g, for the regular grammar generated by (a*b*):

Definition a_b_rules: list(list(non_terminal + terminal)):= [[inl S;inr a; inl S];[inl S;inr b; inl S]].

Which one can see as S -> aS | S -> bS. where S is a non termnal and a and b are terminals (in this case, inductive types given by).

Inductive non_terminal:Type :=
S.
Inductive terminal : Type :=
a | b.

Now let's say I have an automata definition that would look like this one: 
Record dfa (S A : Type) := DFA {
  initial_state : S;
  is_final : S -> bool;
  next : S -> A -> S
}.
And a function that takes a list of elements of the type A (which will be the terminal symbols) and returns whether the list is recgonized by the automata or not.
Definition run_dfa S A (m : dfa S A) (l : list A) : bool :=
  is_final m (fold_left (next m) l (initial_state m)).

I would like to have a function that would iterate over the list of those rules and I could see one of those sublists as a possible function for the automata and store each one of them in a datatype, or just check over the list while running the word in the automata if there is any of those functions that could be used. Does anyone knows how this could be done? Any help/idea will be apreciated.

Thanks in Advance,
Erick.


  • [Coq-Club] Trying to make an conversion from a regular grammar to a finite automata, Erick Simas Grilo, 05/19/2017

Archive powered by MHonArc 2.6.18.

Top of Page