From 9b3a308c7248fd2fa94162e4401726327cc66aa3 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Wed, 23 Jun 2021 16:20:51 +0000 Subject: Add some agda test --- sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html | 115 ++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create 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 new file mode 100644 index 0000000..308e205 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html @@ -0,0 +1,115 @@ + +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