Determinization

[stschaef]

Demonstrate the weak equivalence between an NFA and its epsilon-saturated powerset DFA

Defining the term from NFA traces to DFA traces is straightforward

 NFA→DFA : ∀ q →
    N.Trace true q ⊢
      &[ X ∈ ε-closed ]
      &[ q∈X ∈ q ∈-ε-closed X ] ℙN.Trace true X

Defining the map back needs a way to order the many traces that the DFA encodes and then take the smallest. Given a trace in the DFA into subset X, we may choose the smallest NFA trace that X encodes

  DFA→NFA : ∀ X →
    ℙN.Trace true X ⊢
      ⊕[ q ∈ ⟨ N.Q ⟩ ]
      ⊕[ q∈X ∈ q ∈-ε-closed X ] N.Trace true q

and then we compose that with a function that pulls this trace back to the initial state

  fold-walk :
    (q : ⟨ N.Q ⟩) → (X : ⟨ FinSetDecℙ N.Q ⟩) →
    (q' : ⟨ N.Q ⟩) →
    (q∈εX : q ∈-ε-closed ε-closure X) →
    (q'-[ε*]→q : GraphWalk' ε-graph q q') →
    N.Trace true q ⊢ N.Trace true q'

To all result in the function we really want

  DFA→NFA-init :
    ℙN.Trace true (ε-closure (SingletonDecℙ {A = N.Q} N.init))
      ⊢ N.Trace true (N .init)

[maxsnew]

it's not compiling rn

[maxsnew]

Looks like it's because you deleted the old NFA code instead of making a new module so all of the regex stuff is just broken. I'll add it back in a separate module and I might do a big re-org