regexp.abstract.automata: Automata in the abstract layer



Overview

  • NFA B St : For finite types B St : finType the type of nondeterministic finite automata. NFAs do not have ε transitions.
  • accept M: The language accepted by M
  • M1 =A= M2: Automata equivalence.

A nondeterministic automata

Record NFA (B St : finType) := {
    trans : transition.t B St;
    start : {set St};
    final : {set St}
  }.

Arguments trans {B St}.
Arguments start {B St}.
Arguments final {B St}.

Section DecEq.
  Context [B St : finType].
  Definition eqnfa (m0 m1 : NFA B St) :=
    (trans m0 == trans m1) && (start m0 == start m1) && (final m0 == final m1).

  Lemma eqnfaP (m0 m1 : NFA B St) : reflect (m0 = m1) (eqnfa m0 m1).
    apply/(iffP idP).
    - case: m0 ⇒ tr0 S0 F0 ; case: m1 ⇒ tr1 S1 F1; rewrite /eqnfa //=.
      move /andP ⇒ [/andP [/eqP htr] /eqP hS] /eqP hF; by rewrite htr hS hF.
    - move ⇒ h; rewrite h {h}; case: m1 ⇒ tr S F; rewrite /eqnfa.
      by do 2 (apply /andP; intuition).
  Qed.

End DecEq.

HB.instance Definition nfaeqdec B St := hasDecEq.Build (NFA B St) (@eqnfaP B St).

Given an nfa mac : NFA B St, string xs : seq B is acceptable if
Definition accept {B St : finType}(mac : NFA B St) : seq B → Prop
  := path.reachable (trans mac) (start mac)(final mac).


Section Equiv.
  Context {B St : finType}.
  Definition equiv (m0 m1 : NFA B St) : Prop
    := (start m0 == start m1) ∧ (final m0 == final m1) ∧ (trans m0 == trans m1).

  Lemma eq_equiv (m0 m1 : NFA B St) : equiv m0 m1 → m0 = m1.
    case m0 ⇒ tr0 start0 end0; case m1 ⇒ tr1 start1 end1.
    rewrite /equiv //=; case ⇒ [h1 [h2 h3]]; apply /eqP; rewrite /eq_op //=.
    lazy [eqnfa]; by rewrite //= h1 h2 h3 //=.
  Qed.

End Equiv.

Infix "=A=" := equiv (at level 70).