Indexed grammars as a LFP of an endofunctor (#18)

* a generic definition of (non-indexed) inductive grammars (uses TERMINATING) * syntax for LinPi/Sigma that matches the paper syntax better * wip on indexed inductives * Kleene star via mu * wip on porting the Dyck example to indexed mu * port the Dyck example to indexed inductives * id/comp for indexed inductive algebra homomorphisms * induction principle and case analysis for indexed inductives * Compatibility with opaque tensor --------- Co-authored-by: Steven Schaefer <[email protected]>
maxsnew · Sep 27, 2024 · d127d1f · d127d1f
1 parent d970635
commit d127d1f
Show file tree

Hide file tree

Showing 5 changed files with 399 additions and 2 deletions.
diff --git a/code/cubical/Examples/Indexed/Dyck.agda b/code/cubical/Examples/Indexed/Dyck.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS -WnoUnsupportedIndexedMatch #-}
+module Examples.Indexed.Dyck where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Bool as Bool hiding (_⊕_ ;_or_)
+import Cubical.Data.Equality as Eq
+open import Cubical.Data.Nat as Nat
+open import Cubical.Data.List hiding (init; rec)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as Sum hiding (rec)
+open import Cubical.Data.FinSet
+
+private
+  variable
+    ℓg : Level
+
+open import Examples.Dyck
+open import Grammar Alphabet
+open import Grammar.Maybe Alphabet hiding (μ)
+open import Grammar.Equivalence Alphabet
+open import Grammar.Inductive.Indexed Alphabet
+open import Term Alphabet
+
+data DyckTag : Type ℓ-zero where
+  nil' balanced' : DyckTag
+DyckTy : Unit → Functor Unit
+DyckTy _ = ⊕e DyckTag (λ
+  { nil' → k ε
+  ; balanced' → ⊗e (k (literal [)) (⊗e (Var _) (⊗e (k (literal ])) (Var _))) })
+IndDyck : Grammar ℓ-zero
+IndDyck = μ DyckTy _
+
+data TraceTag : Type where
+  eof' open' close' leftovers' unexpected' : TraceTag
+TraceTys : ℕ × Bool → Functor (ℕ × Bool)
+TraceTys (n , b) = ⊕e TraceTag (λ
+  { eof' → ⊕e (n Eq.≡ zero) (λ _ → ⊕e (b Eq.≡ true) λ _ → k ε)
+  ; open' → ⊗e (k (literal [)) (Var (suc n , b))
+  ; close' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊗e (k (literal ])) (Var (n-1 , b))
+  ; leftovers' → ⊕e (Eq.fiber suc n) λ (n-1 , _) → ⊕e (b Eq.≡ false) λ _ → k ε
+  ; unexpected' → ⊕e ((n , b) Eq.≡ (0 , false)) λ _ → ⊗e (k (literal ])) (k ⊤)
+  })
+
+Trace : ℕ → Bool → Grammar ℓ-zero
+Trace n b = μ TraceTys (n , b)
+
+opaque
+  unfolding _⊗_ ⊗-intro
+  parse : string ⊢ &[ n ∈ ℕ ] ⊕[ b ∈ _ ] Trace n b
+  parse = foldKL*r _ (record { the-ℓ = ℓ-zero ; G = _
+    ; nil-case = LinΠ-intro (Nat.elim
+      (LinΣ-intro true ∘g roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl ∘g id)
+      (λ n-1 _ → LinΣ-intro false ∘g roll ∘g LinΣ-intro leftovers' ∘g LinΣ-intro (_ , Eq.refl) ∘g LinΣ-intro Eq.refl ∘g id))
+    ; cons-case = LinΠ-intro λ n → ⟜-intro⁻ (LinΣ-elim (λ
+      { [ → ⟜-intro {k = Goal n} (⊸-intro⁻ (
+        (LinΣ-elim λ b → ⊸-intro {k = Goal n}
+          (LinΣ-intro b ∘g roll ∘g LinΣ-intro open'))
+        ∘g LinΠ-app (suc n)))
+      ; ] → ⟜-intro {k = Goal n} (Nat.elim {A = λ n → _ ⊢ Goal n}
+          (LinΣ-intro false ∘g roll ∘g LinΣ-intro unexpected' ∘g LinΣ-intro Eq.refl ∘g id ,⊗ ⊤-intro)
+          (λ n-1 _ →
+          ⊸-intro⁻ ((LinΣ-elim λ b → ⊸-intro {k = Goal (suc n-1)} (LinΣ-intro b ∘g roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl)))
+            ∘g LinΠ-app n-1))
+          n) })) })
+    where
+      Goal : ℕ → Grammar ℓ-zero
+      Goal n = ⊕[ b ∈ Bool ] Trace n b
+
+  mkTree : Trace zero true ⊢ IndDyck
+  mkTree = ⊗-unit-r ∘g rec TraceTys alg (0 , true) where
+    Stk : ℕ → Grammar ℓ-zero
+    Stk = Nat.elim ε λ _ Stk⟨n⟩ → literal ] ⊗ IndDyck ⊗ Stk⟨n⟩
+    GenIndDyck : ℕ × Bool → Grammar ℓ-zero
+    GenIndDyck (n , false) = ⊤
+    GenIndDyck (n , true) = IndDyck ⊗ Stk n
+    alg : Algebra TraceTys GenIndDyck
+    alg (n , b) = LinΣ-elim (λ
+      { eof' → LinΣ-elim (λ { Eq.refl → LinΣ-elim λ { Eq.refl → (roll ∘g LinΣ-intro nil') ,⊗ id ∘g ⊗-unit-r⁻ } })
+      ; open' → Bool.elim {A = λ b → literal [ ⊗ GenIndDyck (suc n , b)  ⊢ GenIndDyck (n , b)}
+          (⟜4⊗ (⟜4-intro-ε (roll ∘g LinΣ-intro balanced')))
+          ⊤-intro b
+      ; close' → LinΣ-elim (λ { (n-1 , Eq.refl) → Bool.elim
+                                                   {A =
+                                                    λ b →
+                                                      Term (literal ] ⊗ GenIndDyck (n-1 , b)) (GenIndDyck (suc n-1 , b))}
+        (⟜0⊗ (roll ∘g LinΣ-intro nil'))
+        ⊤-intro
+        b } )
+      ; leftovers' → LinΣ-elim λ { (n-1 , Eq.refl) → LinΣ-elim λ { Eq.refl → ⊤-intro } }
+      ; unexpected' → LinΣ-elim λ { Eq.refl → ⊤-intro }
+      })
+
+  exhibitTrace' : IndDyck ⊢ Trace zero true
+  exhibitTrace' = ((⟜-app ∘g ⊸0⊗ (roll ∘g LinΣ-intro eof' ∘g LinΣ-intro Eq.refl ∘g LinΣ-intro Eq.refl)) ∘g LinΠ-app 0) ∘g rec DyckTy alg _ where
+    Goal : Unit → Grammar ℓ-zero
+    Goal _ = &[ n ∈ ℕ ] (Trace n true ⟜ Trace n true)
+    alg : Algebra DyckTy Goal
+    alg _ = LinΣ-elim (λ
+      { nil' → LinΠ-intro (λ n → ⟜-intro-ε id)
+      ; balanced' → LinΠ-intro λ n → ⟜-intro {k = Trace n true}
+        (roll ∘g LinΣ-intro open'
+        ∘g id ,⊗ ((⟜-app ∘g LinΠ-app (suc n) ,⊗ ((roll ∘g LinΣ-intro close' ∘g LinΣ-intro (_ , Eq.refl) ∘g id ,⊗ (⟜-app ∘g LinΠ-app n ,⊗ id)) ∘g ⊗-assoc⁻)) ∘g ⊗-assoc⁻)
+        ∘g ⊗-assoc⁻)
+      })
diff --git a/code/cubical/Grammar/Dependent/Base.agda b/code/cubical/Grammar/Dependent/Base.agda
@@ -24,15 +24,23 @@ LinearΠ {A = A} f w = ∀ (a : A) → f a w
 LinearΣ : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΣ {A = A} f w = Σ[ a ∈ A ] f a w
 
+Dep⊕-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
+Dep⊕-syntax = LinearΣ
+
 LinearΣ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΣ-syntax = LinearΣ
 
+Dep&-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
+Dep&-syntax = LinearΠ
+
 LinearΠ-syntax : {A : Type ℓS} → (A → Grammar ℓG) → Grammar (ℓ-max ℓS ℓG)
 LinearΠ-syntax = LinearΠ
 
 -- TODO: this precedence isn't really right
 syntax LinearΣ-syntax {A = A} (λ x → B) = LinΣ[ x ∈ A ] B
+syntax Dep⊕-syntax {A = A} (λ x → B) = ⊕[ x ∈ A ] B
 syntax LinearΠ-syntax {A = A} (λ x → B) = LinΠ[ x ∈ A ] B
+syntax Dep&-syntax {A = A} (λ x → B) = &[ x ∈ A ] B
 
 module _ {A : Type ℓS} {g : Grammar ℓG}{h : A → Grammar ℓH} where
   LinΠ-intro : (∀ a → g ⊢ h a) → g ⊢ LinΠ[ a ∈ A ] h a

diff --git a/code/cubical/Grammar/Inductive.agda b/code/cubical/Grammar/Inductive.agda
@@ -0,0 +1,151 @@
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+module Grammar.Inductive (Alphabet : hSet ℓ-zero)where
+
+open import Cubical.Foundations.Structure
+
+open import Helper
+open import Grammar Alphabet
+open import Term Alphabet
+
+private
+  variable ℓG ℓG' ℓ ℓ' : Level
+
+module _ where
+  data Endofunctor ℓ : Type (ℓ-suc ℓ) where
+    k : Grammar ℓ → Endofunctor ℓ
+    Var : Endofunctor ℓ -- identity
+    &e ⊕e : ∀ (X : Type ℓ) → (X → Endofunctor ℓ) → Endofunctor ℓ
+    ⊗e : Endofunctor ℓ → Endofunctor ℓ → Endofunctor ℓ
+
+  ⟦_⟧ : Endofunctor ℓ → Grammar ℓ → Grammar ℓ
+  ⟦ k x ⟧ g = x
+  ⟦ Var ⟧ g = g
+  ⟦ &e X F_x ⟧ g = LinΠ[ x ∈ X ] (⟦ F_x x ⟧ g)
+  ⟦ ⊕e X F_x ⟧ g = LinΣ[ x ∈ X ] (⟦ F_x x ⟧ g)
+  ⟦ ⊗e F F' ⟧ g = ⟦ F ⟧ g ⊗' ⟦ F' ⟧ g
+
+  opaque
+    unfolding _⊗_ ⊗-intro
+    map : ∀ (F : Endofunctor ℓ) {g h} → g ⊢ h → ⟦ F ⟧ g ⊢ ⟦ F ⟧ h
+    map (k x) f    = id
+    map Var f      = f
+    map (&e X Fx) f = LinΠ-intro λ x → map (Fx x) f ∘g LinΠ-app x
+    map (⊕e X Fx) f = LinΣ-elim (λ x → LinΣ-intro x ∘g map (Fx x) f)
+    map (⊗e F G) f = map F f ,⊗ map G f
+
+    map-id : ∀ (F : Endofunctor ℓ) {g} → map F (id {g = g}) ≡ id
+    map-id (k h) i w x = x
+    map-id Var i w x = x
+    map-id (&e A F) i w x a = map-id (F a) i w (x a)
+    map-id (⊕e A F) i w (a , x) = a , (map-id (F a) i w x)
+    map-id (⊗e F F') i w (sp , x , x') = sp , map-id F i _ x , map-id F' i _ x'
+
+    map-∘ :  ∀ (F : Endofunctor ℓ) {g h k} (f : h ⊢ k)(f' : g ⊢ h)
+      → map F (f ∘g f') ≡ map F f ∘g map F f'
+    map-∘ (k g') f f' i w x = x
+    map-∘ Var f f' i w x = f w (f' w x)
+    map-∘ (&e A F) f f' i w  x   a  = map-∘ (F a) f f' i w (x a)
+    map-∘ (⊕e A F) f f' i w (a , x) = a , map-∘ (F a) f f' i w x
+    map-∘ (⊗e F F') f f' i w (sp , x , x') = sp , map-∘ F f f' i _ x , map-∘ F' f f' i _ x'
+
+  data μ (F : Endofunctor ℓ) : Grammar ℓ where
+    roll : ⟦ F ⟧ (μ F) ⊢ μ F
+
+  module _ (F : Endofunctor ℓ) where
+    Algebra : Grammar ℓ → Type _
+    Algebra X = ⟦ F ⟧ X ⊢ X
+
+    initialAlgebra : Algebra (μ F)
+    initialAlgebra = roll
+
+    Homomorphism : ∀ {g h} → Algebra g → Algebra h → Type _
+    Homomorphism {g = g}{h = h} ϕ ψ = Σ[ f ∈ g ⊢ h ]
+      f ∘g ϕ ≡ ψ ∘g map F f
+
+    idHomo : ∀ {g} → (ϕ : Algebra g) → Homomorphism ϕ ϕ
+    idHomo ϕ = id , λ i → ϕ ∘g map-id F (~ i)
+
+    compHomo : ∀ {g h k} (ϕ : Algebra g)(ψ : Algebra h)(χ : Algebra k)
+      → Homomorphism ψ χ → Homomorphism ϕ ψ
+      → Homomorphism ϕ χ
+    compHomo ϕ ψ χ α β = (α .fst ∘g β .fst) ,
+      ( (λ i → α .fst ∘g β .snd i)
+      ∙ (λ i → α .snd i ∘g map F (β .fst))
+      ∙ (λ i → χ ∘g map-∘ F (α .fst) (β .fst) (~ i)))
+
+  {-# TERMINATING #-}
+  rec : ∀ {F : Endofunctor ℓ}{X} → Algebra F X → μ F ⊢ X
+  rec {F = F} alg w (roll _ x) = alg w (map F (rec alg) w x)
+
+  μ-β : ∀ {F : Endofunctor ℓ}{X} → (alg : Algebra F X) → rec {F = F} alg ∘g roll ≡ alg ∘g map F (rec {F = F} alg)
+  μ-β alg = refl
+
+
+  module _ {F : Endofunctor ℓ}{X} (alg : Algebra F X) (ϕ : Homomorphism F (initialAlgebra F) alg) where
+    private
+      {-# TERMINATING #-}
+      μ-η' : ∀ w x → ϕ .fst w x ≡ rec alg w x
+      μ-η' w (roll _ x) = funExt⁻ (funExt⁻ (ϕ .snd) _) x
+        ∙ cong (alg _) (funExt⁻ (funExt⁻ (cong (map F) (funExt λ _ → funExt (μ-η' _))) w) x)
+
+    μ-η : ϕ .fst ≡ rec alg
+    μ-η = funExt λ w → funExt (μ-η' w)
+
+  μ-ind : ∀ {F : Endofunctor ℓ}{X} (alg : Algebra F X) (ϕ ϕ' : Homomorphism F (initialAlgebra F) alg)
+    → ϕ .fst ≡ ϕ' .fst
+  μ-ind α ϕ ϕ' = μ-η α ϕ ∙ sym (μ-η α ϕ')
+
+  μ-ind-id : ∀ {F : Endofunctor ℓ} (ϕ : Homomorphism F (initialAlgebra F) (initialAlgebra F))
+    → ϕ .fst ≡ id
+  μ-ind-id {F = F} ϕ = μ-ind (initialAlgebra F) ϕ (idHomo F (initialAlgebra F))
+
+open import Cubical.Data.Bool
+module _ (g : Grammar ℓ-zero) where
+  -- TODO define sugar for binary sum via Σ[ bool ]
+  *endo : Endofunctor ℓ-zero
+  *endo = ⊕e Bool (λ { false → k ε ; true → ⊗e (k g) Var})
+
+  * : Grammar ℓ-zero
+  * = μ *endo
+
+  opaque
+    unfolding _⊗_
+    open *r-Algebra
+    KLalg : *r-Algebra g
+    KLalg .the-ℓ = ℓ-zero
+    KLalg .G = *
+    KLalg .nil-case = roll ∘g LinΣ-intro false
+    KLalg .cons-case = roll ∘g LinΣ-intro true
+
+    KL*→* : KL* g ⊢ *
+    KL*→* = foldKL*r g KLalg
+
+  *alg : Algebra *endo (KL* g)
+  *alg w (false , x) = nil w x
+  *alg w (true , x) = cons w x
+
+  *→KL* : * ⊢ KL* g
+  *→KL* = rec *alg
+
+  opaque
+    unfolding *r-initial KL*→* KL*r-elim map
+    open import Grammar.Equivalence Alphabet
+    open StrongEquivalence
+    *≅KL* : StrongEquivalence * (KL* g)
+    *≅KL* .fun = *→KL*
+    *≅KL* .inv = KL*→*
+    *≅KL* .sec =
+      !*r-AlgebraHom g (*r-initial g)
+        (record {
+          f = *→KL* ∘g KL*→*
+        ; on-nil = refl
+        ; on-cons = refl })
+        (id*r-AlgebraHom g (*r-initial g))
+    *≅KL* .ret =
+      μ-ind-id
+        (KL*→* ∘g *→KL* ,
+        funExt (λ w → funExt λ {
+          (false , x) → refl
+        ; (true , x) → refl }))