Mercurial > hg > Members > kono > Proof > automaton

changeset 29:2887577a3d63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simpler exists , nfa accept dones not wokred
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 16:41:25 +0900
parents 950d08ec1885
children a9471b42573e
files agda/nfa.agda
diffstat 1 files changed, 15 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/agda/nfa.agda	Mon Nov 05 14:14:40 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 16:41:25 2018 +0900
@@ -35,7 +35,7 @@
     →  ∀ {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 : ℕ )
+record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
      field
         fin : Fin n
@@ -44,27 +44,16 @@
         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 (s≤s (lt0 n)) p where
-         lt0 : (n : ℕ) →  n Data.Nat.≤ n
-         lt0 zero = z≤n
-         lt0 (suc n) = s≤s (lt0 n)
-         lt1 : {m n : ℕ} → suc m  < suc n →  m Data.Nat.≤ n
-         lt1 {zero} _ = z≤n
-         lt1 {suc m} {zero} (s≤s ()) 
-         lt1 {suc m} {suc n} (s≤s lt) = s≤s (lt1 lt) 
-         lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
-         lt2 {zero} lt = z≤n
-         lt2 {suc m} {zero} ()
-         lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
-         exists1 : {m : ℕ} → Fin m → m < suc n  → ( Q → Bool ) → Bool
+     exists p = exists1 fin fin p where
+         exists1 : {m : ℕ} → Fin m → Fin n → ( Q → Bool ) → Bool
          exists1 ( zero ) _ _ = false
-         exists1 ( suc f ) lt p = p (Q←F (inject≤ f (lt1 lt))) ∧ exists1 f (lt2 lt)  p
+         exists1 ( suc f ) fn p = p (Q←F (Data.Fin.pred fn) ) ∧ exists1 f (Data.Fin.pred fn) 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 : FiniteSet States1 
 finState1 = record {
         fin = fromℕ 2
       ; Q←F = Q←F
@@ -96,22 +85,22 @@
 
 Nmoves : { Q : Set } { Σ : Set  }
     → NAutomaton Q  Σ
-    → {n : ℕ } → FiniteSet Q n
+    → {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 )  ))
+      FiniteSet.exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
 
 
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
-    → {n : ℕ } → FiniteSet Q n
+    → {n : ℕ } → FiniteSet Q {n}
     → List  Σ  → Q → Bool
 Naccept M fin [] = Nend M 
-Naccept {Q} {Σ} M fin (s ∷ tail ) = exists1 M ( Nstart M ) s tail 
+Naccept {Q} {Σ} M fin (s ∷ tail ) = Naccept1 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
+      Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  Σ → List  Σ  → Q → Bool
+      Naccept1 M sb s [] q = sb q ∧ Nend M q
+      Naccept1 M sb s (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb s ) i t
 
 
 transition3 : States1  → In2  → States1 → Bool
@@ -131,12 +120,12 @@
 
 start1 : States1 → Bool
 start1 sr = true
-start1 _ = true
+start1 _ = false
 
 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  ∷ [] )
+example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) sr
+example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) sr