~jorge-jbs/theory-of-computation

117d423a923488657bf9be1179665567033a1e47 — Jorge Blázquez Saborido 1 year, 9 months ago 6baae12
Redefine IsFinite and use it as typeclass
9 files changed, 107 insertions(+), 91 deletions(-)

A Common.agda
M DFA.agda
M FA-Regex-Equiv.agda
M Fin.agda
M Lang.agda
M NFA-e.agda
M NFA.agda
M PFA.agda
M Regex.agda
A Common.agda => Common.agda +13 -0
@@ 0,0 1,13 @@
{-# OPTIONS --cubical #-}

module Common where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level
    A : Type ℓ

it : {{_ : A}} → A
it {{x}} = x

M DFA.agda => DFA.agda +22 -23
@@ 17,6 17,7 @@ open import Data.Fin as S
import Data.Fin.Properties
import Data.Empty as Empty

open import Common
open import Lang
open import Fin



@@ 31,26 32,27 @@ f $ x = f x
_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
A ∋ t = t

record DFA {A : Type₀} (A-alph : IsAlphabet A) : Type₁ where
  field
    Q : Type₀
    Q-fin : IsFinite Q
    δ : Q → A → Q
    initial-state : Q
    F : ℙ Q
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  record DFA : Type₁ where
    field
      Q : Type₀
      instance isFinSetQ : isFinSet Q
      δ : Q → A → Q
      initial-state : Q
      F : ℙ Q

  δ̂ : Q → Word A-alph → Q
  δ̂ q [] = q
  δ̂ q (a ∷ w) = δ̂ (δ q a) w
    δ̂ : Q → Word A → Q
    δ̂ q [] = q
    δ̂ q (a ∷ w) = δ̂ (δ q a) w

  lang : Lang A-alph
  lang w = F (δ̂ initial-state w)
    lang : Lang A
    lang w = F (δ̂ initial-state w)

{-
Languages definable by deterministic finite automata
-}
DfaLangs : {A : Type₀} (IsA : IsAlphabet A) → ℙ (Lang IsA)
DfaLangs IsA N = ∃[ M ∶ DFA IsA ] (DFA.lang M ≡ N) , powersets-are-sets _ _
  {-
  Languages definable by deterministic finite automata
  -}
  DfaLangs : ℙ (Lang A)
  DfaLangs N = ∃[ M ∶ DFA ] (DFA.lang M ≡ N) , powersets-are-sets _ _

module example-2-1 where
  δ : Fin 3 → Fin 2 → Fin 3


@@ 63,19 65,16 @@ module example-2-1 where
  A : Type₀
  A = Fin 2

  A-alph : IsAlphabet A
  A-alph = 2 , refl

  M : DFA A-alph
  M : DFA A
  M = record
    { Q = Fin 3
    ; Q-fin = 3 , refl
    ; isFinSetQ = it
    ; δ = δ
    ; initial-state = zero
    ; F = λ q → (q ≡ suc zero) , isSetFin q (suc zero)
    }

  P : Word A-alph → hProp ℓ-zero
  P : Word A → hProp ℓ-zero
  P [] = ⊥
  P (a ∷ []) = ⊥
  P (zero ∷ suc zero ∷ _) = ⊤

M FA-Regex-Equiv.agda => FA-Regex-Equiv.agda +5 -4
@@ 5,18 5,19 @@ module FA-Regex-Equiv where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic

open import Fin
open import Lang
open import DFA
open import NFA
open import NFA-e
open import Regex

module _ {A : Type₀} (IsA : IsAlphabet A) where
  DFA~Regex : DfaLangs IsA ≡ RegexLangs IsA
module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
  DFA~Regex : DfaLangs A ≡ RegexLangs A
  DFA~Regex = {!!}

  DFA~NFA : DfaLangs IsA ≡ NfaLangs IsA
  DFA~NFA : DfaLangs A ≡ NfaLangs A
  DFA~NFA = {!!}

  DFA~NFA-ε : DfaLangs IsA ≡ NFAεLangs IsA
  DFA~NFA-ε : DfaLangs A ≡ NFAεLangs A
  DFA~NFA-ε = {!!}

M Fin.agda => Fin.agda +29 -1
@@ 1,12 1,18 @@
{-# OPTIONS --cubical --safe #-}
{-# OPTIONS --cubical --allow-unsolved-metas #-}

module Fin where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation 
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary using (Discrete; yes; no; mapDec)
open import Cubical.Relation.Nullary.DecidableEq using (Discrete→isSet)
import Cubical.Data.Fin as C


@@ 58,3 64,25 @@ IsFinite A = Σ ℕ (λ n → A ≡ Fin n)

isFinite→isSet : {A : Type₀} → IsFinite A → isSet A
isFinite→isSet (n , r) = transport (cong isSet (sym r)) isSetFin

private
  variable
    ℓ : Level
    A : Type ℓ

isFinSet : Type ℓ → Type ℓ
isFinSet A = ∥ Σ ℕ (λ n → A ≃ Fin n) ∥

isProp-isFinSet : isProp (isFinSet A)
isProp-isFinSet = propTruncIsProp

FinSet : Type (ℓ-suc ℓ)
FinSet = TypeWithStr _ isFinSet

-- Is this even true?
isFinSet→isSet : {{_ : isFinSet A}} → isSet A
isFinSet→isSet = {!!}

instance
  isFinSetFin : ∀ {n} → isFinSet (Fin n)
  isFinSetFin = ∣ _ , pathToEquiv refl ∣

M Lang.agda => Lang.agda +1 -20
@@ 13,22 13,6 @@ module Lang where

open import Fin

Finite : {X : Type ℓ-zero} → ℙ X → Type (ℓ-suc ℓ-zero)
Finite {X} A = Σ X (_∈ A) ≡ Σ ℕ Fin

FiniteSubset : Type₀ → Type₁
FiniteSubset X = Σ (ℙ X) Finite

data FSSet (A : Type₀) : Type₁ where
  [] : FSSet A
  _∷_ : (x : A) → (xs : FSSet A) → FSSet A
  comm : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  dedup : ∀ x xs → x ∷ x ∷ xs ≡ x ∷ xs
  trunc : isSet (FSSet A)

IsAlphabet : Type₀ → Type₁
IsAlphabet A = Σ ℕ (λ n → A ≡ Fin n)

module _ {ℓ}{X : Type ℓ} where
  ∅ : ℙ X
  ∅ _ = Lift Empty , λ ()


@@ 48,10 32,7 @@ module _ {ℓ}{X : Type ℓ} where
  _∩_ : ℙ X → ℙ X → ℙ X
  (A ∩ B) x = A x ⊓ B x

module _ {A : Type₀} (IsA : IsAlphabet A) where
  IsAlphabet→IsSet : isSet A
  IsAlphabet→IsSet = transport (cong isSet (sym (IsA .snd))) isSetFin

module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  Word : Type₀
  Word = List A


M NFA-e.agda => NFA-e.agda +5 -5
@@ 12,11 12,11 @@ open import Cubical.Data.Maybe
open import Lang
open import Fin

module _ {A : Type₀} (A-alph : IsAlphabet A) where
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  record NFA-ε : Type₁ where
    field
      Q : Type₀
      Q-fin : IsFinite Q
      instance isFinSetQ : isFinSet Q
      δ : Q → Maybe A → ℙ Q
      initial-state : Q
      F : ℙ Q


@@ 29,13 29,13 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
    closure : Q → ℙ Q
    closure q p = ∃[ qs ∶ List Q ] is-path-of-εs (q ∷ qs ++ p ∷ [])

    δ̂ : Q → Word A-alph → ℙ Q
    δ̂ : Q → Word A → ℙ Q
    δ̂ q [] = closure q
    δ̂ q (a ∷ w) p = ∃[ r ∶ Q ] ∃[ s ∶ Q ] closure q r ⊓ δ r (just a) s ⊓ δ̂ s w p
      -- p ∈ δ̂ q (a ∷ w) iff (for some states r and s):
      --     there exists a path of the form q …—ε→… r —a→ s …—w→… p

    lang : Lang A-alph
    lang : Lang A
    lang w = ∃[ p ∶ Q ] δ̂ initial-state w p ⊓ F p

  open NFA-ε


@@ 43,5 43,5 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
  {-
  Languages definable by non-deterministic finite automata with empty transitions
  -}
  NFAεLangs : ℙ (Lang A-alph)
  NFAεLangs : ℙ (Lang A)
  NFAεLangs N = ∃[ M ∶ NFA-ε ] (lang M ≡ N) , powersets-are-sets _ _

M NFA.agda => NFA.agda +10 -14
@@ 7,23 7,24 @@ open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
open import Cubical.Data.List hiding ([_])

open import Common
open import Lang
open import Fin

module _ {A : Type₀} (A-alph : IsAlphabet A) where
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  record NFA : Type₁ where
    field
      Q : Type₀
      Q-fin : IsFinite Q
      instance Q-fin : isFinSet Q
      δ : Q → A → ℙ Q
      initial-state : Q
      F : ℙ Q

    δ̂ : Q → Word A-alph → ℙ Q
    δ̂ q [] p = (p ≡ q) , isFinite→isSet Q-fin _ _
    δ̂ : Q → Word A → ℙ Q
    δ̂ q [] p = (p ≡ q) , isFinSet→isSet _ _
    δ̂ q (a ∷ w) p = ∃[ r ∶ Q ] δ q a r ⊓ δ̂ r w p

    lang : Lang A-alph
    lang : Lang A
    --lang w = F ∩ δ̂ initial-state w ≢ ∅
    lang w = ∃[ p ∶ Q ] δ̂ initial-state w p ⊓ F p



@@ 32,19 33,14 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
  {-
  Languages definable by non-deterministic finite automata
  -}
  NfaLangs : ℙ (Lang A-alph)
  NfaLangs : ℙ (Lang A)
  NfaLangs N = ∃[ M ∶ NFA ] (lang M ≡ N) , powersets-are-sets _ _

module example-2-6 where
  A : Type₀
  A = Fin 2

  A-alph : IsAlphabet A
  A-alph = 2 , refl

  Q = Fin 3
  Q-fin : IsFinite Q
  Q-fin = 3 , refl

  δ : Q → A → ℙ Q
  δ zero zero q = ((q ≡ zero) , isSetFin _ _)  ⊓ ((q ≡ suc zero) , isSetFin _ _)


@@ 53,10 49,10 @@ module example-2-6 where
  δ (suc zero) (suc zero) q = (q ≡ suc (suc zero)) , isSetFin _ _
  δ (suc (suc zero)) _ q = ∅ q

  M : NFA A-alph
  M : NFA A
  M = record
    { Q = Q
    ; Q-fin = Q-fin
    ; Q-fin = it
    ; δ = δ
    ; initial-state = zero
    ; F = λ p → (suc (suc zero) ≡ p) , isSetFin _ _


@@ 65,7 61,7 @@ module example-2-6 where
  δ̂ = NFA.δ̂ M
  L = NFA.lang M

  P : Word A-alph → hProp ℓ-zero
  P : Word A → hProp ℓ-zero
  P [] = ⊥
  P (a ∷ []) = ⊥
  P (zero ∷ suc zero ∷ _) = ⊤

M PFA.agda => PFA.agda +11 -10
@@ 21,16 21,17 @@ isEmpty X = X → [ ⊥ ]
Subset : {X : Type ℓ} (P : ℙ X) → Type ℓ
Subset {X = X} P = Σ X (_∈ P)

module _ {A : Type₀} (A-alph : IsAlphabet A) where
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  record PFA : Type₁ where
    field
      Q : Type₀
      Q-fin : IsFinite Q
      instace isFinSetQ : isFinSet Q
      S : Type₀
      S-alph : IsAlphabet S
      instance isFinSetS : isFinSet S
      δ : Q → Maybe A → S → ℙ (Q × List S)
      instance δ-fin : ∀ {q a s} → IsFinite (Subset (δ q a s))
      instance δ-fin : ∀ {q a s} → isFinSet (Subset (δ q a s))
      --δ : Q → Maybe A → S → Σ (ℙ (Q × List S)) (IsFinite ∘ Subset)
      --δ : Q → Maybe A → S → LFSet (Q × List S)
      initial-state : Q
      initial-symbol : S
      F : ℙ Q


@@ 39,7 40,7 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
      constructor config
      field
        state : Q
        word : Word A-alph
        word : Word A
        stack : List S

    data _⊢_ : Config → Config → Type₀ where


@@ 65,13 66,13 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
        → J ⊢* K
        → I ⊢* K

    final-state-lang : Lang A-alph
    final-state-lang : Lang A
    final-state-lang w =
      ∃[ q ∶ Q ] ∃[ α ∶ List S ]
        F q ⊓
        ∥ config initial-state w (initial-symbol ∷ []) ⊢* config q [] α ∥ₚ

    empty-stack-lang : Lang A-alph
    empty-stack-lang : Lang A
    empty-stack-lang w =
      ∃[ q ∶ Q ]
        ∥ config initial-state w (initial-symbol ∷ []) ⊢* config q [] [] ∥ₚ


@@ 84,10 85,10 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where

  open PFA

  FinalStatePfaLangs : ℙ (Lang A-alph)
  FinalStatePfaLangs : ℙ (Lang A)
  FinalStatePfaLangs N = ∃[ M ∶ PFA ] (final-state-lang M ≡ N) , powersets-are-sets _ _

  EmptyStackPfaLangs : ℙ (Lang A-alph)
  EmptyStackPfaLangs : ℙ (Lang A)
  EmptyStackPfaLangs N = ∃[ M ∶ PFA ] (empty-stack-lang M ≡ N) , powersets-are-sets _ _

  _ : FinalStatePfaLangs ≡ EmptyStackPfaLangs


@@ 96,5 97,5 @@ module _ {A : Type₀} (A-alph : IsAlphabet A) where
  {-
  Languages definable by pushdown finite automata
  -}
  PfaLangs : ℙ (Lang A-alph)
  PfaLangs : ℙ (Lang A)
  PfaLangs = FinalStatePfaLangs

M Regex.agda => Regex.agda +11 -14
@@ 17,7 17,7 @@ repeat : {A : Type₀} → ℕ → List A → List A
repeat zero xs = []
repeat (suc n) xs = xs ++ repeat n xs

module _ {A : Type₀} (IsA : IsAlphabet A) where
module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
  infixr 10 _+_ _·_
  infixr 11 _*
  data Regex : Type₀ where


@@ 26,21 26,21 @@ module _ {A : Type₀} (IsA : IsAlphabet A) where
    _+_ _·_ : Regex → Regex → Regex
    _* : Regex → Regex

  lang : Regex → Lang IsA
  lang : Regex → Lang A
  lang ∅ w = ⊥
  lang ε w = ⟦ε⟧ IsA w
  lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
  lang ε w = ⟦ε⟧ A w
  lang (char x) w = (w ≡ x ∷ []) , isOfHLevelList 0 isFinSet→isSet _ _
  lang (x + y) w = (lang x ∪ lang y) w
  lang (x · y) w =
    ∃[ u ] ∃[ v ] lang x u ⊓ lang y v ⊓
      ( (u ++ v ≡ w)
      , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
      , isOfHLevelList 0 isFinSet→isSet _ _
      )
  lang (x *) w =
    ⋃ ℕ
      (λ n u →
        ( (u ≡ repeat n w)
        , isOfHLevelList 0 (IsAlphabet→IsSet IsA) _ _
        , isOfHLevelList 0 isFinSet→isSet _ _
        )
      )
      w


@@ 48,7 48,7 @@ module _ {A : Type₀} (IsA : IsAlphabet A) where
  {-
  Languages definable by regular expressions
  -}
  RegexLangs : ℙ (Lang IsA)
  RegexLangs : ℙ (Lang A)
  RegexLangs M = ∃[ x ∶ Regex ] (lang x ≡ M) , powersets-are-sets _ _

  RegexQuot : Type₁


@@ 64,22 64,19 @@ module example where
  A : Type₀
  A = Fin 2

  A-alph : IsAlphabet A
  A-alph = 2 , refl

  -- (0|1)*01(0|1)*
  x : Regex A-alph
  x : Regex A
  x = (char zero + char (suc zero))* · char zero · char (suc zero) · (char zero + char (suc zero))*

  P : Lang A-alph
  P : Lang A
  P [] = ⊥
  P (a ∷ []) = ⊥
  P (zero ∷ suc zero ∷ _) = ⊤
  P (zero ∷ zero ∷ w) = P (zero ∷ w)
  P (suc zero ∷ b ∷ w) = P (b ∷ w)

  L : Lang A-alph
  L = lang A-alph x
  L : Lang A
  L = lang A x

  _ : L ≡ P
  _ = {!!}