Definition of Coq finite state machines
I am studying Coq and I would like to use it to formalize the theory of regular languages, especially for finite state machines. Let's say I have a structure for automata like this:
Record automata : Type := {
dfa_set_states : list state;
init_state : state;
end_state : state;
dfa_func: state -> terminal -> state;
}.
Where the state is inductive type as:
Inductive state:Type :=
S.
And terminal terminal like
Inductive terminal:Type :=
a | b.
I am trying to define it, so that later I can generalize the definition to any common language. For now, I would like to build an automaton that recognizes the language (a * b *), which is all words over the alphabet {a, b}. Does anyone have an idea on how to create some kind of fixpoint function that will trigger a word (which I see as a list of terminals) and tell me if these automata are reconstructing that word or not? Any idea / help would be greatly appreciated.
Thanks in advance, Erick.
source to share
Since you're limiting yourself to regular languages, it's pretty straightforward: you just have to use a fold. Here's an example:
Require Import Coq.Lists.List.
Import ListNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Record dfa (S A : Type) := DFA {
initial_state : S;
is_final : S -> bool;
next : S -> A -> S
}.
Definition run_dfa S A (m : dfa S A) (l : list A) : bool :=
is_final m (fold_left (next m) l (initial_state m)).
This snippet differs slightly from your original definition in that the state and alphabet components are now DFA type parameters, and in this I have replaced the final state with a predicate that says whether we are in an accepting state or not. The function run_dfa
simply iterates over the DFA transition function, starting from the initial state, and then checks to see if the last state is accepting.
You can use this framework to describe almost any common language. For example, here is a recognition machine a*b*
:
Inductive ab := A | B.
Inductive ab_state : Type :=
ReadA | ReadB | Fail.
Definition ab_dfa : dfa ab_state ab := {|
initial_state := ReadA;
is_final s := match s with Fail => false | _ => true end;
next s x :=
match s, x with
| ReadB, A => Fail
| ReadA, B => ReadB
| _, _ => s
end
|}.
We can prove that this automaton does what we expect. Here's a theorem that says it takes strings of the target language:
Lemma ab_dfa_complete n m : run_dfa ab_dfa (repeat A n ++ repeat B m) = true.
Proof.
unfold run_dfa. rewrite fold_left_app.
assert (fold_left (next ab_dfa) (repeat A n) (initial_state ab_dfa) = ReadA) as ->.
{ now simpl; induction n as [| n IH]; simpl; trivial. }
destruct m as [|m]; simpl; trivial.
induction m as [|m IH]; simpl; trivial.
Qed.
We can also indicate the opposite, which says that it only accepts strings of that language and nothing else. I left proof; it shouldn't be hard to understand.
Lemma ab_dfa_sound l :
run_dfa ab_dfa l = true ->
exists n m, l = repeat A n ++ repeat B m.
Unfortunately, there is not much we can do with this view other than starting the machine. In particular, we cannot minimize an automaton, check if two automata are equivalent, etc. These functions also need to take as argument lists that list all elements of the state and alphabet type, S
and A
.
source to share