Determinization (#24)

--------- Co-authored-by: nvarner <[email protected]>
maxsnew · Oct 8, 2024 · 7e76a4a · 7e76a4a
1 parent 402b72b
commit 7e76a4a
Show file tree

Hide file tree

Showing 16 changed files with 1,757 additions and 885 deletions.
diff --git a/code/cubical/DFA/Base.agda b/code/cubical/DFA/Base.agda
@@ -8,172 +8,35 @@ open import Cubical.Foundations.Structure
 open import Cubical.Relation.Nullary.DecidablePropositions
 
 open import Cubical.Data.FinSet
-open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Bool
 
 open import Grammar Alphabet
+open import Grammar.Lift Alphabet
+open import Grammar.Inductive.Indexed Alphabet
 open import Grammar.Equivalence Alphabet
+import Cubical.Data.Equality as Eq
 open import Term Alphabet
 open import Helper
 
 private
-  variable ℓΣ₀ ℓD ℓP ℓ : Level
+  variable ℓD ℓP ℓ : Level
 
-record DFA : Type (ℓ-suc ℓD) where
+record DFA ℓD : Type (ℓ-suc ℓD) where
   field
     Q : FinSet ℓD
     init : ⟨ Q ⟩
-    isAcc : ⟨ Q ⟩ → DecProp ℓD
+    isAcc : ⟨ Q ⟩ → Bool
     δ : ⟨ Q ⟩ → ⟨ Alphabet ⟩ → ⟨ Q ⟩
 
-  negate : DFA
-  Q negate = Q
-  init negate = init
-  isAcc negate q = negateDecProp (isAcc q)
-  δ negate = δ
+  data TraceTag : Type ℓD where
+    stop step : TraceTag
 
-  module _ (q-end : ⟨ Q ⟩) where
-    -- The grammar "Trace q" denotes the type of traces in the DFA
-    -- from state q to q-end
-    data Trace : (q : ⟨ Q ⟩) → Grammar ℓD where
-      nil : ε ⊢ Trace q-end
-      cons : ∀ q c →
-        literal c ⊗' Trace (δ q c) ⊢ Trace q
+  TraceTy : Bool → (q : ⟨ Q ⟩) → Functor ⟨ Q ⟩
+  TraceTy b q = ⊕e TraceTag λ {
+      stop → ⊕e (Lift (b Eq.≡ isAcc q))
+        (λ (lift acc) → k (LiftG ℓD ε) )
+    ; step → ⊕e (Lift ⟨ Alphabet ⟩)
+      λ { (lift c) → ⊗e (k (LiftG ℓD (literal c))) (Var (δ q c)) }}
 
-    record Algebra : Typeω where
-      field
-        the-ℓs : ⟨ Q ⟩ → Level
-        G : (q : ⟨ Q ⟩) → Grammar (the-ℓs q)
-        nil-case : ε ⊢ G q-end
-        cons-case : ∀ q c →
-          literal c ⊗ G (δ q c) ⊢ G q
-
-    open Algebra
-
-    opaque
-      unfolding _⊗_
-      initial : Algebra
-      the-ℓs initial _ = ℓD
-      G initial = Trace
-      nil-case initial = nil
-      cons-case initial = cons
-
-    record AlgebraHom (alg alg' : Algebra) : Typeω where
-      field
-        f : (q : ⟨ Q ⟩) → alg .G q ⊢ alg' .G q
-        on-nil :
-          f q-end ∘g alg .nil-case ≡ alg' .nil-case
-        on-cons : ∀ q c →
-          f q ∘g alg .cons-case q c ≡
-            alg' .cons-case q c ∘g (⊗-intro id (f (δ q c)))
-      fInit = f init
-
-    open AlgebraHom
-
-    opaque
-      unfolding ⊗-intro
-      idAlgebraHom : (alg : Algebra) →
-        AlgebraHom alg alg
-      f (idAlgebraHom alg) q = id
-      on-nil (idAlgebraHom alg) = refl
-      on-cons (idAlgebraHom alg) _ _ = refl
-
-      AlgebraHom-seq : {alg alg' alg'' : Algebra} →
-        AlgebraHom alg alg' → AlgebraHom alg' alg'' →
-        AlgebraHom alg alg''
-      AlgebraHom-seq ϕ ψ .f q = ψ .f q ∘g ϕ .f q
-      AlgebraHom-seq ϕ ψ .on-nil =
-        cong (ψ .f _ ∘g_) (ϕ .on-nil)  ∙
-        ψ .on-nil
-      AlgebraHom-seq ϕ ψ .on-cons q c =
-        cong (ψ .f q ∘g_) (ϕ .on-cons q c) ∙
-        cong (_∘g ⊗-intro id (ϕ .f (δ q c))) (ψ .on-cons q c)
-
-    module _ (the-alg : Algebra) where
-      opaque
-        unfolding _⊗_
-        recTrace : ∀ {q} → Trace q ⊢ the-alg .G q
-        recTrace {q} w (nil .w pε) = the-alg .nil-case w pε
-        recTrace {q} w (cons .q c .w p⊗) =
-          the-alg .cons-case q c _
-            (p⊗ .fst , (p⊗ .snd .fst) , (recTrace _ (p⊗ .snd .snd)))
-
-      recInit : Trace init ⊢ the-alg .G init
-      recInit = recTrace
-
-      opaque
-        unfolding recTrace ⊗-intro initial _⊗_
-        ∃AlgebraHom : AlgebraHom initial the-alg
-        f ∃AlgebraHom q = recTrace {q}
-        on-nil ∃AlgebraHom = refl
-        on-cons ∃AlgebraHom _ _ = refl
-
-        !AlgebraHom-help :
-          (e e' : AlgebraHom initial the-alg) →
-          (q : ⟨ Q ⟩) →
-          (∀ w p → e .f q w p ≡ e' .f q w p)
-        !AlgebraHom-help e e' q w (nil .w pε) =
-          cong (λ a → a w pε) (e .on-nil) ∙
-          sym (cong (λ a → a w pε) (e' .on-nil))
-        !AlgebraHom-help e e' q w (cons .q c .w p⊗) =
-          cong (λ a → a w p⊗) (e .on-cons q c) ∙
-          cong (λ a → the-alg .cons-case q c _
-            ((p⊗ .fst) , ((p⊗ .snd .fst) , a)))
-            (!AlgebraHom-help e e' (δ q c) _
-              (p⊗ .snd .snd)) ∙
-          sym (cong (λ a → a w p⊗) (e' .on-cons q c))
-
-      !AlgebraHom :
-        (e e' : AlgebraHom initial the-alg) →
-        (q : ⟨ Q ⟩) →
-        e .f q ≡ e' .f q
-      !AlgebraHom e e' q =
-        funExt (λ w → funExt (λ p → !AlgebraHom-help e e' q w p))
-
-    opaque
-      unfolding idAlgebraHom
-      initial→initial≡id :
-        (e : AlgebraHom initial initial) →
-        (q : ⟨ Q ⟩) →
-        (e .f q)
-          ≡
-        id
-      initial→initial≡id e q =
-        !AlgebraHom initial e (idAlgebraHom initial) q
-
-    algebra-η :
-      (e : AlgebraHom initial initial) →
-      fInit e ≡ id
-    algebra-η e = initial→initial≡id e _
-
-  module _ (q-start : ⟨ Q ⟩) where
-    module _ (q-end : ⟨ Q ⟩) where
-      AcceptingTrace : Grammar ℓD
-      AcceptingTrace =
-        LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
-
-      Parse = AcceptingTrace
-
-      RejectingTrace : Grammar ℓD
-      RejectingTrace =
-        LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
-
-    TraceFrom : Grammar ℓD
-    TraceFrom = LinΣ[ q-end ∈ ⟨ Q ⟩ ] Trace q-end q-start
-
-    AcceptingTraceFrom : Grammar ℓD
-    AcceptingTraceFrom =
-      LinΣ[ q-end ∈ ⟨ Q ⟩ ]
-        LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
-
-    ParseFrom = AcceptingTraceFrom
-
-    RejectingTraceFrom : Grammar ℓD
-    RejectingTraceFrom =
-      LinΣ[ q-end ∈ ⟨ Q ⟩ ]
-        LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
-
-  InitTrace : Grammar ℓD
-  InitTrace = TraceFrom init
-
-  InitParse : Grammar ℓD
-  InitParse = ParseFrom init
+  Trace : Bool → (q : ⟨ Q ⟩) → Grammar ℓD
+  Trace b = μ (TraceTy b)
diff --git a/code/cubical/DFA/Decider.agda b/code/cubical/DFA/Decider.agda
@@ -16,75 +16,111 @@ open import Cubical.Data.SumFin
 open import Cubical.Data.Unit
 open import Cubical.Data.Empty as Empty
 open import Cubical.Data.List hiding (init)
+import Cubical.Data.Equality as Eq
+
 
 open import Grammar Alphabet
+open import Grammar.Inductive.Indexed Alphabet as Idx
 open import Grammar.Equivalence Alphabet
+open import Grammar.String.Properties Alphabet
+open import Grammar.Lift Alphabet
 open import Term Alphabet
 open import DFA.Base Alphabet
 open import Helper
 
 private
   variable ℓΣ₀ ℓD ℓP ℓ : Level
 
-module _ (D : DFA {ℓD}) where
+module _ (D : DFA ℓD) where
   open DFA D
 
   open *r-Algebra
-  open Algebra
-  open AlgebraHom
-
-  opaque
-    unfolding _⊗_
-    run-from-state : string ⊢ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
-    run-from-state = foldKL*r char the-alg
-      where
-        the-cons :
-          char ⊗ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q ⊢
-            LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
-        the-cons =
-          LinΠ-intro (λ q →
-          ⟜-intro⁻ (LinΣ-elim (λ c →
-            ⟜-intro {k = TraceFrom q}
-              (⊸-intro⁻
-                (LinΣ-elim
-                  (λ q' → ⊸-intro {k = TraceFrom q}
-                    (LinΣ-intro {h = λ q'' → Trace q'' q} q' ∘g
-                      Trace.cons q c))
-                ∘g LinΠ-app (δ q c))))))
-
-        the-alg : *r-Algebra char
-        the-alg .the-ℓ = ℓD
-        the-alg .G = LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
-        the-alg .nil-case = LinΠ-intro (λ q → LinΣ-intro q ∘g nil)
-        the-alg .cons-case = the-cons
-
-  check-accept : {q-start : ⟨ Q ⟩} (q-end : ⟨ Q ⟩) →
-    Trace q-end q-start ⊢
-      AcceptingTrace q-start q-end ⊕ RejectingTrace q-start q-end
-  check-accept q =
-    decRec
-      (λ acc → ⊕-inl ∘g LinΣ-intro acc)
-      (λ rej → ⊕-inr ∘g LinΣ-intro rej)
-      (isAcc q .snd)
-
-  check-accept-from : (q-start : ⟨ Q ⟩) →
-    TraceFrom q-start ⊢
-      AcceptingTraceFrom q-start ⊕ RejectingTraceFrom q-start
-  check-accept-from q-start =
-    LinΣ-elim (λ q-end →
-      ⊕-elim (⊕-inl ∘g LinΣ-intro q-end) (⊕-inr ∘g LinΣ-intro q-end) ∘g
-      check-accept q-end)
-
-  decide :
-    string ⊢
-      LinΠ[ q ∈ ⟨ Q ⟩ ] (AcceptingTraceFrom q ⊕ RejectingTraceFrom q)
-  decide =
-    LinΠ-intro (λ q →
-      check-accept-from q ∘g
-      LinΠ-app q) ∘g
-    run-from-state
-
-  decideInit :
-    string ⊢
-      (AcceptingTraceFrom init ⊕ RejectingTraceFrom init)
-  decideInit = LinΠ-app init ∘g decide
+
+  open StrongEquivalence
+
+  parse : string ⊢ &[ q ∈ ⟨ Q ⟩ ] ⊕[ b ∈ Bool ] Trace b q
+  parse = foldKL*r char the-alg
+    where
+    the-alg : *r-Algebra char
+    the-alg .the-ℓ = ℓD
+    the-alg .G = &[ q ∈ ⟨ Q ⟩ ] ⊕[ b ∈ Bool ] Trace b q
+    the-alg .nil-case =
+      &ᴰ-in (λ q →
+        ⊕ᴰ-in (isAcc q) ∘g
+        roll ∘g
+        ⊕ᴰ-in stop ∘g
+        ⊕ᴰ-in (lift Eq.refl) ∘g
+        liftG ∘g
+        liftG
+        )
+    the-alg .cons-case =
+      &ᴰ-in λ q →
+        ⊕ᴰ-elim (λ c →
+          ⊕ᴰ-elim
+            (λ b →
+              ⊕ᴰ-in b ∘g
+              roll ∘g ⊕ᴰ-in step ∘g ⊕ᴰ-in (lift c) ∘g
+              liftG ,⊗ liftG ∘g liftG ,⊗ id) ∘g
+          ⊕ᴰ-distR .fun ∘g
+          id ,⊗ &ᴰ-π (δ q c)) ∘g
+        ⊕ᴰ-distL .fun
+
+  printAlg : ∀ b → Algebra (TraceTy b) λ _ → string
+  printAlg b q = ⊕ᴰ-elim ((λ {
+      stop → ⊕ᴰ-elim λ { (lift Eq.refl) → NIL ∘g lowerG ∘g lowerG }
+    ; step →
+        CONS ∘g
+        ⊕ᴰ-elim λ { (lift c) →
+          ⊕ᴰ-in c ,⊗ id ∘g
+          lowerG ,⊗ lowerG ∘g
+          lowerG ,⊗ id}
+    }))
+
+  print : ∀ b → (q : ⟨ Q ⟩) → Trace b q ⊢ string
+  print b q = Idx.rec (TraceTy b) (printAlg b) q
+
+  ⊕ᴰalg : ∀ b → Algebra (TraceTy b) λ q → ⊕[ b ∈ Bool ] Trace b q
+  ⊕ᴰalg b q = ⊕ᴰ-elim (λ {
+      stop → ⊕ᴰ-elim λ {
+        (lift Eq.refl) →
+          ⊕ᴰ-in (isAcc q) ∘g roll ∘g
+          ⊕ᴰ-in stop ∘g ⊕ᴰ-in (lift Eq.refl)}
+    ; step →
+        ⊕ᴰ-elim (λ c → ⊕ᴰ-elim (λ b →
+          ⊕ᴰ-in b ∘g
+          roll ∘g ⊕ᴰ-in step ∘g ⊕ᴰ-in c ∘g liftG ,⊗ liftG)
+          ∘g ⊕ᴰ-distR .fun ∘g lowerG ,⊗ lowerG)
+    })
+
+  Trace≅string :
+    (q : ⟨ Q ⟩) → StrongEquivalence (⊕[ b ∈ Bool ] Trace b q) string
+  Trace≅string q .fun = ⊕ᴰ-elim (λ b → print b q)
+  Trace≅string q .inv = &ᴰ-π q ∘g parse
+  Trace≅string q .sec =  unambiguous-string _ _
+  Trace≅string q .ret = isRetract
+    where
+    opaque
+      unfolding NIL CONS KL*r-elim ⊕ᴰ-distR
+      isRetract : &ᴰ-π q ∘g parse ∘g ⊕ᴰ-elim (λ b → print b q) ≡ id
+      isRetract = ⊕ᴰ≡ _ _ λ b →
+        ind'
+          (TraceTy b)
+          (⊕ᴰalg b)
+          ((λ q'  → &ᴰ-π q' ∘g parse ∘g print b q') ,
+          λ q' → ⊕ᴰ≡ _ _ (λ {
+            stop → funExt λ w → funExt λ {
+              ((lift Eq.refl) , p) → refl}
+          ; step → ⊕ᴰ≡ _ _ λ c → refl }))
+          ((λ q' → ⊕ᴰ-in b) ,
+          λ q' → ⊕ᴰ≡ _ _ λ {
+            stop → funExt (λ w → funExt λ {
+              ((lift Eq.refl) , p) → refl})
+          ; step → refl })
+          q
+
+  unambiguous-⊕Trace : ∀ q → unambiguous (⊕[ b ∈ Bool ] Trace b q)
+  unambiguous-⊕Trace q =
+   unambiguous≅ (sym-strong-equivalence (Trace≅string q)) unambiguous-string
+
+  unambiguous-Trace : ∀ b q → unambiguous (Trace b q)
+  unambiguous-Trace b q = unambiguous⊕ᴰ isSetBool (unambiguous-⊕Trace q) b