Library ATBR.DKA_Determinisation

Conversion from NFAs to DFAs.

The algorithm basically constructs a Store, i.e.,

a bijection from reachable set of states to a new set of states,

represented as a Table together with a bound (the next fresh state, or, equivalently, the size of the Table)

a transition relation over these new states, represented by a map (Delta)

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import MxSemiRing.
Require Import MxKleeneAlgebra.

Require Import DKA_Definitions.
Require Import DKA_StateSetSets.
Require Import Numbers.
Require Import Utils_WF.

Import Numbers.Positive.
Open Scope num_scope.

Notation Table := (statesetmap state).
Notation Delta := (statelabelmap state).
Notation Store := (Table * Delta * state)%type.

Section S.

  Open Scope num_scope.
  Variable A : NFA.t.

  Notation delta := (NFA.delta A).
  Notation initiaux := (NFA.initiaux A).
  Notation finaux := (NFA.finaux A).
  Notation max_label := (NFA.max_label A).
  Notation size := (NFA.size A).

extension of the transition function to sets

  Definition delta_set :=
    let delta := delta in
      fun (a: label) (q: stateset) => StateSet.fold (fun x => StateSet.union (delta a x)) q StateSet.empty.

we start with the store mapping the set of initial states to one

Definition initial_store: Store :=
(StateSetMap.add initiaux (state_of_nat 0) (StateSetMap.empty _),StateLabelMap.empty _,(state_of_nat 1)).

the algorithm (function build_store below) consists in iterating the following function step, defined by open recursion through the loop argument. intuitively, step loop p np a s assumes that p points to np in the store s ; it returns the store where all descendants of p along a have been added.

  Definition step (delta_set: label -> stateset -> stateset) loop p np :=
    (fun a s =>
      let q := delta_set a p in
        let '(table,d,next) := s in
          match StateSetMap.find q table with
            | None => loop (StateSetMap.add q next table, StateLabelMap.add (np,a) next d, S next) q next
            | Some nq => (table, StateLabelMap.add (np,a) nq d, next)
          end
    ).

powerfix does (2^size) iterations, which is sufficient since the set of reachable sets of states cannot have a larger size. at each stage, one folds over the set of labels to add all the descendence of p

  Definition build_store :=
    let step := step delta_set in
    let max_label := max_label in
    powerfix size
    (fun loop (s: Store) (p: stateset) (np: state) =>
      fold_labels (step loop p np) max_label s
    ) (fun s _ _ => s) initial_store initiaux 0.

once we obtained the store, it suffices to convert it into a DFA

  Definition table_finals (table: Table) :=
    let finaux := finaux in
    StateSetMap.fold
      (fun p np acc =>
        if StateSet.exists_ (fun s => StateSet.mem s finaux) p
          then StateSet.add np acc else acc
      ) table StateSet.empty.

  Definition delta' (d: Delta) :=
    fun a x => match StateLabelMap.find (x,a) d with Some y => y | None => 0 end.

  Definition NFA_to_DFA :=
    let '(t,d,n) := build_store in
      DFA.mk n (delta' d) 0 (table_finals t) max_label.

Now starts the correctness proof ; we need to know that the NFA A is bounded.

Hypothesis HA: NFA.bounded A.

We start the correctness proof by characterising build_store with the following simpler fixpoint (which is problematic from the computational point of view: one has to compute the worst case exponential bound, even if it is not reached)

  Definition step' := step delta_set.

  Fixpoint steps n s p np :=
    match n with
      | O => s
      | Datatypes.S n => fold_labels (step' (steps n) p np) max_label s
    end.

  Instance step_compat: Proper
    (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (@eq _)))
      ==>
     pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (@eq _))))) step'.

characterisation of build_store with steps, as explained above

  Lemma build_store_spec: build_store = steps (power size) initial_store initiaux (state_of_nat 0).

  Notation "s %t" := (fst (fst s)) (at level 1).
  Notation "s %d" := (snd (fst s)) (at level 1).
  Notation "s %s" := (snd s) (at level 1).

preliminary lemma: delta_set builds bounded sets

Lemma bounded_delta_set: forall a p, setbelow (delta_set a p) size.

Invariant of the construction

Record invariant s: Prop := {

all states in the table are bounded

i_table_wf: forall p i, StateSetMap.MapsTo p i s%t -> setbelow p size /\ below i s%s;

the table is injective

i_table_inj: forall p q i, StateSetMap.MapsTo p i s%t -> StateSetMap.MapsTo q i s%t -> StateSet.Equal p q;

the table is surjective

i_table_surj: forall i, below i s%s -> exists p, StateSetMap.MapsTo p i s%t;

the table contains s%n elements (derivable from the two previous points, but easier to require here)

i_table_size: StateSetMap.cardinal s%t = nat_of_num s%s;

any transition in s%d corresponds to a delta_set transition in the NFA

    i_delta: forall np a nq, StateLabelMap.MapsTo (np,a) nq s%d ->
      exists2 p, StateSetMap.MapsTo p np s%t & StateSetMap.MapsTo (delta_set a p) nq s%t
  }.

Dynamics of the construction : we basically prove that invariant s entails extends s (steps i s) /\ defined (steps i s)

Record extends (s s': Store): Prop := {

the resulting store satisfies the invariant

e_invariant :> invariant s';

the table was extended

    e_table: forall p i, StateSetMap.MapsTo p i s%t -> StateSetMap.MapsTo p i s'%t;
    e_next: s%s <= s'%s
  }.

Last definition: a store is `defined up to P' if there are transitions for all state n and label a, except for those specified in P

  Definition defined (s: Store) P := forall n a, n<s%s -> a < max_label -> StateLabelMap.In (n,a) s%d \/ P n a.

  Instance transitive_extends: Transitive extends.
  Lemma reflexive_extends: forall s, invariant s -> extends s s.

the following lemma corresponds to the termination of the algorithm: iterating 2^n times is enough to reach all possible subsets

Lemma store_size_bound: forall s, invariant s -> (nat_of_state s%s <= power size)%nat.

heart of the proof : specification of steps

  Lemma steps_correct: forall i (s: Store) p np,
    (power size - s%s < i)%nat ->
    invariant s ->
    StateSetMap.MapsTo p np s%t ->
    extends s (steps i s p np) /\
    forall P, defined s (fun n a => P n a \/ n=np) -> defined (steps i s p np) P.

the initial store satisfies the invariant

Lemma invariant_initial_store: invariant initial_store.

therefore, the constructed store extends the initial one, and is completely defined

  Lemma build_store_correct:
    extends initial_store build_store
    /\ forall n a, n<build_store %s -> a < max_label -> StateLabelMap.In (n,a) build_store %d.

in particular, the constructed store satisfies the invariant

Lemma invariant_build_store: invariant build_store.

we define notations for the three projections

  Notation table := (build_store %t).
  Notation size' := (build_store %s).
  Notation d := (build_store %d).

rho is the predicate that associates states of the DFA to the sets of reachable states from the NFA

Notation rho p i := (StateSetMap.MapsTo p i table).

theta is the converse function: it associates a set of states to each state of the DFA

Definition theta i :=
StateSetMap.fold (fun p np acc => if eq_state_bool i np then p else acc) table StateSet.empty.

specification of theta, for valid states

Lemma rho_theta i: i<size' -> rho (theta i) i.

rho is injective (it admits theta as an inverse function)

Lemma theta_rho: forall p i, rho p i -> StateSet.Equal (theta i) p.

sets build via theta are bounded, and theta is empty out of the bounds

Lemma theta_below: forall u i, StateSet.In u (theta i) -> i < size' /\ u < size.

specification of the delta_set function

  Lemma in_delta_set: forall j p b,
    StateSet.In j (delta_set b p) <->
    exists k, StateSet.In k p /\ StateSet.In j (delta b k).

theta and delta' commute

Lemma theta_delta': forall a i, a < max_label -> i < size' ->
StateSet.eq (theta (delta' d a i)) (delta_set a (theta i)).

we need this lemma to use the StateSetProps.exists_iff from the FSet library

Lemma final_compat: SetoidList.compat_bool NumSet.E.eq (fun s => StateSet.mem s finaux).
Local Hint Resolve final_compat.

two auxiliary lemmas about table_finals, to obtain the characterisation mem_table_finals below

  Lemma table_finals_correct:
    forall i, StateSet.In i (table_finals table) ->
      exists2 u, StateSet.In u (theta i) & StateSet.In u finaux.

  Lemma table_finals_complete:
    forall u p i, StateSet.In u finaux -> rho p i -> StateSet.In u p -> StateSet.In i (table_finals table).

specification of table_finals

Lemma mem_table_finals: forall i,
StateSet.mem i (table_finals table) = StateSet.exists_ (fun x => StateSet.mem x finaux) (theta i).

the construted DFA has at least one state

Lemma positive_size: 0 < size'.

its transitions are bounded

Lemma delta'_below: forall a i, delta' d a i < size'.

the constructed DFA is bounded (requirement of DFA_Merge / DFA_Equiv)

Lemma bounded: DFA.bounded NFA_to_DFA.

the state 1 points to the set of initial states

Lemma theta_0: StateSet.eq (theta (state_of_nat 0)) (initiaux).

Final theorem : correctness of the algorithm, the constructed DFA evaluates as the original NFA

Theorem correct: DFA.eval NFA_to_DFA == NFA.eval A.

Opaque dot one zero equal. Transparent dot one zero equal.
Opaque eq_nat_bool. Transparent eq_nat_bool.

End S.

We finally prove that the algorithm preserves the max_label field

Lemma preserve_max_label: forall A, DFA.max_label (NFA_to_DFA A) = NFA.max_label A.