Mercurial > hg > Members > kono > Proof > automaton
view agda/nfa.agda @ 27:caf9b6aebd24
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 05 Nov 2018 11:16:29 +0900 |
parents | 7ce76b3acc62 |
children | 950d08ec1885 |
line wrap: on
line source
module nfa where -- open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Data.List open import Data.Fin hiding ( _<_ ) open import Data.Maybe open import Relation.Nullary open import Data.Empty open import Data.Bool using ( Bool ; true ; false ; _∧_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) data States1 : Set where sr : States1 ss : States1 st : States1 data In2 : Set where i0 : In2 i1 : In2 record NAutomaton ( Q : Set ) ( Σ : Set ) : Set where field Nδ : Q → Σ → Q → Bool Nstart : Q → Bool Nend : Q → Bool open NAutomaton Nmoves1 : { Q : Set } { Σ : Set } → NAutomaton Q Σ → ∀ {q : Q} → ( (q : Q ) → Bool ) → Σ → Q → Bool Nmoves1 {Q} { Σ} M {q'} Qs s q = (Qs q') ∧ ( Nδ M q' s q ) record FiniteSet ( Q : Set ) ( n : ℕ ) : Set where field fin : Fin n Q←F : Fin n → Q F←Q : Q → Fin n finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f exists : ( Q → Bool ) → Bool exists p = exists1 fin p where exists1 : {n : ℕ} → Fin n → ( Q → Bool ) → Bool exists1 ( zero ) _ = false exists1 ( suc f ) p = p (Q←F {!!}) ∧ exists1 f p fless : {n : ℕ} → (f : Fin n ) → toℕ f < n fless zero = s≤s z≤n fless (suc f) = s≤s ( fless f ) finState1 : FiniteSet States1 3 finState1 = record { fin = fromℕ 2 ; Q←F = Q←F ; F←Q = F←Q ; finiso→ = finiso→ ; finiso← = finiso← } where Q←F : Fin 3 → States1 Q←F zero = sr Q←F (suc zero) = ss Q←F (suc (suc zero)) = st Q←F (suc (suc (suc ()))) F←Q : States1 → Fin 3 F←Q sr = zero F←Q ss = suc (zero) F←Q st = suc ( suc zero ) finiso→ : (q : States1) → Q←F (F←Q q) ≡ q finiso→ sr = refl finiso→ ss = refl finiso→ st = refl finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f finiso← zero = refl finiso← (suc zero) = refl finiso← (suc (suc zero)) = refl finiso← (suc (suc (suc ()))) open FiniteSet Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ → {n : ℕ } → FiniteSet Q n → ( Q → Bool ) → Σ → Q → Bool Nmoves {Q} { Σ} M fin Qs s q = FiniteSet.exists fin ( λ qn → (Qs q ∧ ( Nδ M q s qn ) )) Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ → {n : ℕ } → FiniteSet Q n → List Σ → Q → Bool Naccept M fin [] = Nend M Naccept {Q} {Σ} M fin (s ∷ tail ) = exists1 M ( Nstart M ) s tail where exists1 : NAutomaton Q Σ → ( Q → Bool ) → Σ → List Σ → Q → Bool exists1 M sb s [] = Nend M exists1 M sb s (i ∷ t ) = exists1 M ( Nmoves M fin sb s ) i t transition3 : States1 → In2 → States1 → Bool transition3 sr i0 sr = true transition3 sr i1 ss = true transition3 sr i1 sr = true transition3 ss i0 sr = true transition3 ss i1 sr = true transition3 st i0 sr = true transition3 st i1 sr = true transition3 _ _ _ = false fin1 : States1 → Bool fin1 st = true fin1 ss = false fin1 sr = false start1 : States1 → Bool start1 sr = true start1 _ = true am2 : NAutomaton States1 In2 am2 = record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1} example2-1 = Naccept am2 finState1 ( i0 ∷ i1 ∷ i0 ∷ [] ) example2-2 = Naccept am2 finState1 ( i1 ∷ i1 ∷ i1 ∷ [] )