Library Lstar

Rivest-Schapire-style automata learning https://www.tifr.res.in/~shibashis.guha/courses/diwali2021/L-starMalharManagoli.pdf

From lstar Require Import DFA ListLemmas RS.
From Stdlib Require Import Classes.RelationClasses.
From Stdlib Require Import Setoids.Setoid.
From Stdlib Require Import List.
From Stdlib Require Import Lia.
From Stdlib Require Import Recdef.
From Stdlib Require Import PeanoNat.
From Stdlib Require Import Eqdep_dec.
Import ListNotations.
From lstar Require Import Teacher.

Module Lstar (s : Symbol) (L : RegularLanguage s) (T : Teacher s L).
Import s L T D.

T-equivalent

Given any two strings u, v ∈ Σ∗ and a set T ⊆ Σ∗, we say that u, v are T-equivalent, and write u ≡T v, if ∀t ∈ T, u · t ∈ L ⇐⇒ v · t ∈ L. Otherwise, we say that they are T-distinguishable

Definition T_equiv (T : str → bool) (u v : str) : Prop :=
    ∀ (t : str),
        T t = true →
        member (u ++ t) = member (v ++ t).

Notation "T '[' u '==' v ']'" := (T_equiv T u v).

Note that ≡T is an equivalence relation

Definition Teq_refl : ∀ T u,
    T [u == u].

Definition Teq_sym : ∀ T u v,
    T [u == v] → T [v == u].

Definition Teq_trans : ∀ T u v w,
    T [u == v] →
    T [v == w] →
    T [u == w].

Instance Teq_relation : ∀ T, Equivalence (T_equiv T).

Add Parametric Relation T : str (T_equiv T)
  reflexivity proved by (Teq_refl T)
  symmetry proved by (Teq_sym T)
  transitivity proved by (Teq_trans T)
  as Teq_setoid.

Also, for every T1 ⊆ T2 ⊆ Σ∗, ≡T2 is a refinement of ≡T1.

As T2 has more strings in it, it has a better chance of distinguishing any given pair of strings

Theorem refined_distinguish : ∀ T1 T2
    (Subset: ∀ s : str,
        T1 s = true → T2 s = true),
    ∀ u v,
        T2 [u == v] → T1 [u == v].

But Σ∗ is a superset of all the T's, so IL refines every ≡T.

Lemma total_refinement : ∀ T u v,
(fun _ ⇒ true) [u == v] → T [u == v].

The states Q and T that we maintain will be finite

Definition finite (f : str → bool) :=
{l : list str | NoDup l ∧
∀ (s : str), f s = true ↔ In s l}.

T-equivalence is decidable for finite sets

Definition T_equiv_dec : ∀ T (u v : str),
finite T →
{T [u == v]} + {~ T [u == v]}.

A set Q ⊆ Σ∗ is said to be separable with respect to T, if the elements of Q are pairwise T-distinguishable.

Definition separable (Q T : str → bool) : Type :=
    ∀ (u v : str), Q u = true → Q v = true →
        u ≠ v →
        ¬ T [u == v].

A set Q is said to be closed with respect to T, if ∀q ∈ Q ∀a ∈ Σ, ∃q′ ∈ Q such that q · a ≡T q'.

Definition closed (Q T : str → bool) :=
    ∀ q a,
        Q q = true →
        {q' : str | Q q' = true ∧ T [(q ++ [a]) == q']}.

Closedness is decidable for finite sets:

Q is not closed wrt T if one can traverse the list of elements in Q without finding a q' such that q · a ≡T q' for all a
Q is closed wrt T otherwise

Definition closed_dec_witness : ∀ Q T,
  finite Q →
  finite T →
  closed Q T +
  { q : str & { a : s.t &
      Q q = true ∧
      ∀ q', Q q' = true → ¬ T [q ++ [a] == q'] }}.

Definition closed_dec : ∀ Q T,
    finite Q →
    finite T →
    closed Q T + (closed Q T → Empty_set).

Lemma 1. If Q is closed and separable with respect to T, the transition function δ : (q, a) → q′ ∈ Q such that q′ ≡T q · a, is well defined.

Definition delta Q T (c : closed Q T) (q : str) (a : s.t) (Qq : Q q = true) :
{q' : str | Q q' = true ∧ T [q' == (q ++ [a])]}.
Defined.

Lemma 2. Given a hypothesis DFA H = (Q, Σ, δ, ε, F) where Q is closed and separable with respect to T, and a counterexample w = w1, w2 ... wm, we can find strings qn+1 and t such that Q′ = Q ∪ {qn+1} is separable with respect to T′ = T ∪ {t}.

A hypothesis DFA is one whose states are the string representatives in Q, with the transition function given by delta.

Record HypothesisDFA : Type := {
  Q : str → bool;
  T : str → bool;
  sep : separable Q T;
  clos : closed Q T;

ε must be in Q as the initial state

eps_in_Q : Q nil = true;

Q and T must be finite

fin_Q : finite Q;
fin_T : finite T;
}.

The concrete DFA extracted from a HypothesisDFA

Definition make_dfa (H : HypothesisDFA) : D.t {q | H.(Q) q = true}.
Defined.

Updating sets of strings

Definition update (S : str → bool) k b :=
    fun s ⇒ if str_eq s k then b else S s.

Notation "s [ k := v ]" := (update s k v).

Lemma update_neq : ∀ S x y k,
    x ≠ y →
    S[x := k] y = S y.

Lemma update_eq : ∀ S x k,
    S[x := k] x = k.

Given a counter-example, we can always find q_new and t to add to Q, T such that Q' and T' are finite and Q' is separable wrt T' (see RS.v for linear and binary searches)

Module RSS <: RS_Setup s L T.
  Definition obt := HypothesisDFA.
  Definition P (o : obt) (q : str) : Prop := o.(Q) q = true.
  Definition make_dfa (o : obt) : D.t { q | P o q } := make_dfa o.

  Lemma eps_in_H : ∀ (o : obt),
      proj1_sig (make_dfa o).(initial _) = [].

  Lemma acc_correct : ∀ (o : obt) q,
      accept _ (make_dfa o) q = member (proj1_sig q).
End RSS.

Module RSan := RS s L T RSS.
Import RSan.

Theorem find_separable :
  ∀ (H : HypothesisDFA)
         (w : str)

         (Hce : accept_string (make_dfa H) w ≠ member w),
  { q_new : str &
  { t : str &
      (H.(Q) q_new = false) ×
      let Q' := H.(Q) [q_new := true] in
      let T' := H.(T) [t := true] in
      separable Q' T' ×
      finite Q' ×
      finite T' }}.

Lemma 3. If Q is separable with respect to T, it is possible to add finitely many strings to Q resulting in a set Q′ which is closed and separable with respect to T.

For any finite sets Q and T and string u, either we can find a 'representative' string r in Q such that u and r are T-equivalent, or all elements in Q are T-distinguishable from u

Lemma find_representative : ∀ Q T
    (finQ : finite Q)
    (finT : finite T)
    (u : str),
    { r | Q r = true ∧ T [u == r] } +
    { ∀ r, Q r = true → ¬ T [u == r] }.

We can add a representative of q to Q to get a new set Q' that is still separable and finite and is a superset of Q

Lemma close_step : ∀ Q T q (a : s.t)
    (sep : separable Q T)
    (finQ : finite Q)
    (finT : finite T),
    { Q' : str → bool &
        ((Q' = Q [q ++ [a] := true]) + (Q' = Q)) ×
        separable Q' T ×
        finite Q' ×
        (∀ s, Q s = true → Q' s = true) ×
        { r | Q' r = true ∧ T [(q ++ [a]) == r] } }.

If Q is not closed wrt T, we can find a q in Q such that all q' in Q are T-distinguishable from q ++ a for all symbols in the alphabet

Lemma not_closed_impl_distinguishable :
    ∀ Q T,
        (closed Q T → False) →
        finite Q → finite T →
        {q : str & {a : s.t | Q q = true ∧
            ∀ q', Q q' = true → ¬ T [q ++ [a] == q'] }}.

Adds a finite number of strings to Q to make it closed wrt T

Definition union_closed_loop :
    ∀ (n : nat) Q Q' T
        (sep' : separable Q' T)
        (finT : finite T)
        (finQ' : finite Q')
        (sub' : ∀ s, Q s = true → Q' s = true),
        option { Q'' : str → bool &
            closed Q'' T ×
            separable Q'' T ×
            finite Q'' ×
            (∀ s, Q' s = true → Q'' s = true) }.
Defined.

union_closed_loop always returns Some with enough fuel

Lemma loop_terminates : ∀ n Q Q' T
    (sep' : separable Q' T)
    (finQ' : finite Q')
    (Tl : list str)
    (NDT : NoDup Tl)
    (HTl : ∀ s : str, T s = true ↔ In s Tl)
    (sub' : ∀ s, Q s = true → Q' s = true),
    Nat.pow 2 (length Tl) - length (proj1_sig finQ') < n →
    {x | union_closed_loop n Q Q' T sep' (exist _ Tl (conj NDT HTl)) finQ' sub' = Some x}.

Lemma 3

Lemma union_closed :
    ∀ Q T
    (sep : separable Q T)
    (finQ : finite Q)
    (finT : finite T),
    { Q' : str → bool &
        closed Q' T ×
        separable Q' T ×
        finite Q' ×
        (∀ s, Q s = true → Q' s = true) }.

The main L^* implementation that uses Lemmas 2 and 3 to iteratively expand Q and T until the DFA they form encodes L (or fuel runs out).

If fuel runs out, we return the in-progress DFA

Definition num_states_of_fin {f} (H : finite f) : nat :=
    match H with
    | exist _ x _ ⇒ List.length x
    end.

Definition num_states (H : HypothesisDFA) : nat :=
    num_states_of_fin H.(fin_Q).

Lemma finite_subset_is_smaller : ∀
    (f g : str → bool)
    (FinF : finite f)
    (FinG : finite g)
    (FsubG : ∀ (x : str), f x = true → g x = true),
    num_states_of_fin FinF ≤ num_states_of_fin FinG.

Lemma finite_update_impl_finite : ∀
    (f : str → bool) k v
    (FinUpdF : finite f[k := v]),
    finite f.

A hypothesis DFA must be smaller than the number of states in the minimal DFA. This follows from separability of Q

Lemma num_states_le_min : ∀ (H : HypothesisDFA),
num_states H ≤ L.num_states_in_minimal.

If make_dfa has no counterexample then it is minimal. By separability, all q : Q reach distinct states in any encoding DFA, so none can have fewer states

Lemma make_dfa_minimal : ∀ (H : HypothesisDFA),
equiv_query _ (make_dfa H) = None →
minimal (make_dfa H).

Once Q has the full minimal state count there is no counterexample left

Lemma full_states_no_ce : ∀ (H : HypothesisDFA),
L.num_states_in_minimal ≤ num_states H →
equiv_query _ (make_dfa H) = None.

The main L* implementation

Fixpoint lstar_fuel (H : HypothesisDFA) (fuel : nat)
(LE : L.num_states_in_minimal - num_states H ≤ fuel)
: { T : Type & {d : D.t T | minimal d} }.
Defined.

The total L* implementation

Definition lstar (_ : unit) : { T : Type & {d : D.t T | minimal d} }.
Defined.

End Lstar.