DFA

From 9cb56dabb676391a9382731347e8d2b07b9437a5 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Sun, 7 Apr 2024 13:25:49 +0200 Subject: big cleanup --- sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html | 115 ---------------------------- 1 file changed, 115 deletions(-) delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html (limited to 'sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html') diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html deleted file mode 100644 index 308e205..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html +++ /dev/null @@ -1,115 +0,0 @@ - -DFA

module DFA where
-
--- A pair type 
-record _×_ (A B : Set) : Set where
-  constructor _,_
-  field
-    fst : A
-    snd : B
-
--- A list type
-infixr 5 _∷_
-data List (a : Set) : Set where
-  [] : List a
-  _∷_ : a → List a → List a
-
--- Elements of type x ∈ xs is a proof that x is somewhere in xs
-data _∈_ {A : Set}(x : A) : (xs : List A) → Set where
-  here : ∀ {xs} → x ∈ (x ∷ xs)
-  there : ∀ {y xs} → x ∈ xs → x ∈ (y ∷ xs)
-
--- Elements of type a ≡ b is a proof that a and b are the same
-data _≡_ {A : Set}(x : A) : A → Set where
-  refl : x ≡ x
-
--- The empty type. There are no members of this type, so it is the same as false
-data ⊥ : Set where
-
--- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.
-¬_ : Set → Set
-¬ A = A → ⊥
-
--- A DFA is a five tuple of Q Σ q₀ δ F
-record DFA (Q : Set) (Σ : Set) (q₀ : Q) (δ : Q × Σ → Q) (F : List Q) : Set where
-
--- The DFArun data type keeps track of a running dfa.
-data DFArun {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
-  empty : {q : Q} → q ∈ F → DFArun dfa q []
-  acceptOne : {ws : List Σ} →
-              (w : Σ) →
-              (q : Q) →
-              DFArun dfa (δ (q , w)) ws →
-              DFArun dfa q (w ∷ ws)
-
--- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀
-data Accepts {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (w : List Σ) → Set where
-  accepts : ∀{w} → DFArun dfa q₀ w → Accepts dfa w
-
--- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.
-data CantAccept {Q Σ q₀ δ F}(dfa : DFA Q Σ q₀ δ F) : (q : Q) → (w : List Σ) → Set where
-  cantAccept : ∀ {w q} → DFArun dfa q w → ¬(q ≡ q₀) → CantAccept dfa q w
-
-
--- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn't.
-data _∈Lang_ {Q Σ q₀ δ F}(w : List Σ)(dfa : DFA Q Σ q₀ δ F) : Set where
-  inLang : Accepts dfa w → w ∈Lang dfa
-  notInLang : ∀{q} → CantAccept dfa q w → w ∈Lang dfa
-
-
-
-
--- Test stuff. Create a DFA which only accepts an input with an even number of a's
-
-data TestQ : Set where
-  evenNumberOfAs : TestQ
-  oddNumberOfAs : TestQ
-
-data TestΣ : Set where
-  a : TestΣ
-  b : TestΣ
-
-Testδ : TestQ × TestΣ → TestQ
-Testδ (evenNumberOfAs , a) = oddNumberOfAs
-Testδ (evenNumberOfAs , b) = evenNumberOfAs
-Testδ (oddNumberOfAs , a) = evenNumberOfAs
-Testδ (oddNumberOfAs , b) = oddNumberOfAs
-
-TestF : List TestQ
-TestF = evenNumberOfAs ∷ []
-
-TestDFA : DFA TestQ TestΣ evenNumberOfAs Testδ TestF
-TestDFA = _ -- Since a DFA is a record with no fields, agda can infer it
-
--- Try to construct proofs for different input strings
-
-input₁ input₂ input₃ : List TestΣ
-input₁ = [] -- Empty string
-input₂ = a ∷ b ∷ a ∷ a ∷ b ∷ [] -- Three a's
-input₃ = b ∷ b ∷ a ∷ b ∷ a ∷ [] -- Two a's
-
-
--- The proofs are found automatically by agda, and no other proofs would type check
-proof₁ : input₁ ∈Lang TestDFA -- Proof that input₁ is in the language
-proof₁ = inLang (accepts (empty here))
-
-proof₂ : input₂ ∈Lang TestDFA -- Proof that input₂ is not in the language
-proof₂ = notInLang
-           (cantAccept
-            (acceptOne a oddNumberOfAs
-             (acceptOne b evenNumberOfAs
-              (acceptOne a evenNumberOfAs
-               (acceptOne a oddNumberOfAs
-                (acceptOne b evenNumberOfAs (empty here))))))
-            (λ ()))
-
-proof₃ : input₃ ∈Lang TestDFA -- Proof that input₃ is in the language
-proof₃ = inLang
-           (accepts
-            (acceptOne b evenNumberOfAs
-             (acceptOne b evenNumberOfAs
-              (acceptOne a evenNumberOfAs
-               (acceptOne b oddNumberOfAs
-                (acceptOne a oddNumberOfAs (empty here)))))))
-
-

\ No newline at end of file -- cgit v1.2.3