~jorge-jbs/theory-of-computation

499cf042c085086947714dac013705f5dc74f2ec — Jorge Blázquez Saborido 1 year, 9 months ago 02da137
Add product constructions for DFA
4 files changed, 170 insertions(+), 8 deletions(-)

M Axioms.agda
M DFA.agda
M Fin.agda
M Lang.agda
M Axioms.agda => Axioms.agda +4 -4
@@ 6,17 6,17 @@ open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import Cubical.Data.Sum

record LEM {ℓ : Level} : Type (ℓ-suc ℓ) where
record LEM : Typeω where
  field
    decide : ∀ (P : Type ℓ) → isProp P → P ⊎ (¬ P)
    decide : ∀ {ℓ} (P : Type ℓ) → isProp P → P ⊎ (¬ P)

classical-decide : ∀ {ℓ} {{lem : LEM {ℓ}}}  (P : Type ℓ) → isProp P → P ⊎ (¬ P)
classical-decide : ∀ {{_ : LEM}} {ℓ} (P : Type ℓ) → isProp P → P ⊎ (¬ P)
classical-decide {{lem}} = lem .LEM.decide

private
  open import Cubical.Data.Nat
  open import Common
  example : {{lem : LEM}} → ℕ → ℕ
  example : {{_ : LEM}} → ℕ → ℕ
  example x with classical-decide (x ≡ 0) (isSetℕ x 0)
  ... | inl _ = x + 1
  ... | inr _ = x ∸ 1

M DFA.agda => DFA.agda +141 -4
@@ 7,6 7,9 @@ open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
open import Cubical.HITs.PropositionalTruncation as PT
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


@@ 17,6 20,7 @@ open import Data.Fin as S
import Data.Fin.Properties
import Data.Empty as Empty

open import Axioms
open import Common
open import Lang
open import Fin


@@ 34,18 38,152 @@ module _ (Symbol : Type₀) {{isFinSetA : isFinSet Symbol}} where
      --final-states : LFSet State

    run : State → Word Symbol → State
    run  q [] = q
    run q [] = q
    run q (a ∷ w) = run (next q a) w

    lang : Lang Symbol
    --lang w = run start-state w ∈ final-states
    lang w = FinalState (run start-state w)

  {-
  open DFA

  {-|
  Languages definable by deterministic finite automata
  -}
  DfaLangs : ℙ (Lang Symbol)
  DfaLangs N = ∃[ M ∶ DFA ] (DFA.lang M ≡ N) , powersets-are-sets _ _
  DfaLangs N = ∃[ M ∶ DFA ] (lang M ≡ N) , powersets-are-sets _ _

  _×ₐ_ : DFA → DFA → DFA
  M ×ₐ N = record
    { State = (M .State) × (N .State)
    ; next = λ (p , q) a → next M p a , next N q a
    ; start-state = start-state M , start-state N
    ; FinalState = λ (p , q) → FinalState M p ⊓ FinalState N q
    }

  lang-× : (M N : DFA) → lang (M ×ₐ N) ≡ lang M ∩ lang N
  lang-× M N = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      run-ext
        : ∀ w p q
        → run (M ×ₐ N) (p , q) w
        ≡ (run M p w , run N q w)
      run-ext [] _ _ = refl
      run-ext (x ∷ w) p q = run-ext w (next M p x) (next N q x)

      ⇒ : ∀ w → w ∈ lang (M ×ₐ N) → w ∈ (lang M ∩ lang N)
      ⇒ w = subst
        (_∈ FinalState (M ×ₐ N))
        (run-ext w (start-state M) (start-state N))
      ⇐ : ∀ w → w ∈ (lang M ∩ lang N) → w ∈ lang (M ×ₐ N)
      ⇐ w = subst
        (_∈ FinalState (M ×ₐ N))
        (sym (run-ext w (start-state M) (start-state N)))

  _⊕ₐ_ : DFA → DFA → DFA
  M ⊕ₐ N = record
    { State = (M .State) × (N .State)
    ; next = λ (p , q) a → next M p a , next N q a
    ; start-state = start-state M , start-state N
    ; FinalState = λ (p , q) → FinalState M p ⊔ FinalState N q
    }

  lang-⊕ : ∀ M N → lang (M ⊕ₐ N) ≡ lang M ∪ lang N
  lang-⊕ M N = ⊆-extensionality _ _  (⇒ , ⇐)
    where
      run-ext
        : ∀ w p q
        → run (M ⊕ₐ N) (p , q) w
        ≡ (run M p w , run N q w)
      run-ext [] _ _ = refl
      run-ext (x ∷ w) p q = run-ext w (next M p x) (next N q x)

      ⇒ : ∀ w → w ∈ lang (M ⊕ₐ N) → w ∈ (lang M ∪ lang N)
      ⇒ w = PT.rec (∈-isProp (lang M ∪ lang N) w)
        λ { (⊎.inl x) → PT.∣ ⊎.inl (subst
              (_∈ FinalState M ∘ fst)
              (run-ext w (start-state M) (start-state N))
              x
            ) ∣
          ; (⊎.inr x) → PT.∣ ⊎.inr (subst
              (_∈ FinalState N ∘ snd)
              (run-ext w (start-state M) (start-state N))
              x
            ) ∣
          }
      ⇐ : ∀ w → w ∈ (lang M ∪ lang N) → w ∈ lang (M ⊕ₐ N)
      ⇐ w = rec (∈-isProp (lang (M ⊕ₐ N)) w)
        λ { (⊎.inl x) → PT.∣ ⊎.inl (subst
              (_∈ FinalState M ∘ fst)
              (sym (run-ext w (start-state M) (start-state N)))
              x
            ) ∣
          ; (⊎.inr x) → PT.∣ ⊎.inr (subst
              (_∈ FinalState N ∘ snd)
              (sym (run-ext w (start-state M) (start-state N)))
              x
            ) ∣
          }

  _ᶜᵃ : DFA → DFA
  M ᶜᵃ = record
    { State = M .State
    ; next = M .next
    ; start-state = M .start-state
    ; FinalState = λ q → ¬ FinalState M q
    }

  lang-ᶜ : ∀ M → lang (M ᶜᵃ) ≡ (lang M) ᶜ
  lang-ᶜ M = ⊆-extensionality _ _  (⇒ , ⇐)
    where
      run-ext
        : ∀ w p
        → run (M ᶜᵃ) p w
        ≡ run M p w
      run-ext [] _ = refl
      run-ext (x ∷ w) p = run-ext w (next M p x)

      ⇒ : ∀ w → w ∈ lang (M ᶜᵃ) → w ∈ ((lang M)ᶜ)
      ⇒ w = subst
        (λ h → fst (FinalState M h) → ⊥.⊥)
        (run-ext w (start-state M))

      ⇐ : ∀ w → w ∈ ((lang M)ᶜ) → w ∈ lang (M ᶜᵃ)
      ⇐ w = subst
        (λ h → fst (FinalState M h) → ⊥.⊥)
        (sym (run-ext w (start-state M)))

  de-morgan-⊔
    : {{_ : LEM}}
    → ∀ {ℓ ℓ′} (P : hProp ℓ) (Q : hProp ℓ′)
    → P ⊔ Q
    ≡ ¬ (¬ P ⊓ ¬ Q)
  de-morgan-⊔ P Q = (⇔toPath ⇒) ⇐
    where
      ⇒ : [ P ⊔ Q ] → [ ¬ (¬ P ⊓ ¬ Q) ]
      ⇒ P∨Q (¬P , ¬Q) = PT.rec
        ⊥.isProp⊥
          { (⊎.inl [P]) → ¬P [P]
          ; (⊎.inr [Q]) → ¬Q [Q]
          })
        P∨Q
      ⇐ : [ ¬ (¬ P ⊓ ¬ Q) ] → [ P ⊔ Q ]
      ⇐ ¬[¬P∧¬Q]
        with classical-decide [ P ] (snd P)
           | classical-decide [ Q ] (snd Q)
      ... | ⊎.inl [P] | _ = PT.∣ ⊎.inl [P] ∣
      ... | ⊎.inr ¬P  | ⊎.inl [Q] = PT.∣ ⊎.inr [Q] ∣
      ... | ⊎.inr ¬P  | ⊎.inr ¬Q  = ⊥.elim (¬[¬P∧¬Q] (¬P , ¬Q))

  de-morgan-⊕ : {{_ : LEM}} → ∀ M N → M ⊕ₐ N ≡ ((M ᶜᵃ) ×ₐ (N ᶜᵃ)) ᶜᵃ
  de-morgan-⊕ M N i = record
    { State = refl i
    ; isFinSetState = it
    ; next = λ (p , q) a → next M p a , next N q a
    ; start-state = start-state M , start-state N
    ; FinalState = λ (p , q) → de-morgan-⊔ (FinalState M p) (FinalState N q) i
    }

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


@@ 61,7 199,6 @@ module example-2-1 where
  M : DFA Symbol
  M = record
    { State = Fin 3
    ; isFinSetState = it
    ; next = next
    ; start-state = zero
    -- ; final-states = suc zero LFS.∷ LFS.[]

M Fin.agda => Fin.agda +2 -0
@@ 235,3 235,5 @@ equiv-⊎ {n = n} {m = m} {A = A} {B = B} p q =
instance
  isFinSet-⊎ : {{_ : isFinSet A}} {{_ : isFinSet B}} → isFinSet (A ⊎ B)
  isFinSet-⊎ = {!!}
  isFinSet-× : {{_ : isFinSet A}} {{_ : isFinSet B}} → isFinSet (A × B)
  isFinSet-× = {!!}

M Lang.agda => Lang.agda +23 -0
@@ 82,6 82,29 @@ module _ {ℓ}{X : Type ℓ} where
      ... | ⊎.inl [A] | ⊎.inr ¬B  = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inr ¬B ∣)
      ... | ⊎.inr ¬A  | _         = ⊥.elim (¬[¬A∨¬B] PT.∣ ⊎.inl ¬A ∣)

  de-morgan-∪
    : {{_ : LEM}}
    → {A B : ℙ X}
    → A ∪ B ≡ ((A ᶜ) ∩ (B ᶜ))ᶜ
  de-morgan-∪ {A = A} {B = B} = ⊆-extensionality _ _ (⇒ , ⇐)
    where
      ⇒ : ∀ x → x ∈ (A ∪ B) → x ∈ (((A ᶜ) ∩ (B ᶜ))ᶜ)
      ⇒ x A∨B (¬A , ¬B) =
        PT.rec
          isProp⊥
          (λ { (⊎.inl Ax) → ¬A Ax
             ; (⊎.inr Bx) → ¬B Bx
             }
          )
          A∨B
      ⇐ : ∀ x → x ∈ (((A ᶜ) ∩ (B ᶜ))ᶜ) → x ∈ (A ∪ B)
      ⇐ x ¬[¬A∧¬B]
        with classical-decide (x ∈ A) (∈-isProp A x)
           | classical-decide (x ∈ B) (∈-isProp B x)
      ... | ⊎.inl Ax | _ = PT.∣ ⊎.inl Ax ∣
      ... | ⊎.inr ¬A | ⊎.inl Bx = PT.∣ ⊎.inr Bx ∣
      ... | ⊎.inr ¬A | ⊎.inr ¬B = ⊥.elim (¬[¬A∧¬B] (¬A , ¬B))

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