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*):Record reg_grammar: Type:= {
set_non_terminal : (list non_terminal);
set_terminal : (list terminal);
prod_rules: non_terminal -> sf -> Prop;
start_symbol: non_terminal;
}.
Definition a_b_rules: list(list(non_terminal + terminal)):= [[inl S;inr a; inl S];[inl S;inr b; inl S]].
Inductive non_terminal:Type :=
S.
Inductive terminal : Type :=
a | b.
Record dfa (S A : Type) := DFA {
initial_state : S;
is_final : S -> bool;
next : S -> A -> S
}.
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)).
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.