Mercurial > hg > Members > kono > Proof > automaton

changeset 15:54382de19264 subset-construction

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sbconst1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 17:55:07 +0900
parents 7eb71391088c
children 911899e36b96
files agda/sbconst1.agda
diffstat 1 files changed, 36 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/agda/sbconst1.agda	Fri Aug 24 17:22:49 2018 +0900
+++ b/agda/sbconst1.agda	Fri Aug 24 17:55:07 2018 +0900
@@ -16,21 +16,6 @@
 open Automaton
 open NAutomaton
 
--- record Automaton ( Q : Set ) ( Σ : Set  )
---        : Set  where
---     field
---         δ : Q → Σ → Q
---         astart : Q
---         aend : Q → Bool
---
--- record NAutomaton ( Q : Set ) ( Σ : Set  )
---        : Set  where
---     field
---           nδ : Q → Σ → List Q
---           sid : Q  →  ℕ
---           nstart : Q
---           nend  : Q → Bool
-
 record FiniteSet ( Q : Set ) ( max1 : ℕ  )
         : Set  where
      field
@@ -45,30 +30,14 @@
 
 open FiniteSet
 
-_div_ : ℕ → ℕ → Maybe ℕ
-_div_ x zero = {!!}
-_div_ x (suc y) = {!!}
-
-_mod_ : ℕ → ℕ → Maybe ℕ
-_mod_ = {!!}
-
-lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
-lemma1 {Q} {R} {zero} {_} N M  = {!!}
-lemma1 {Q} {R} {n} {zero} N M  = {!!}
-lemma1 {Q} {R} {n} {m} N M = record {
-        not-zero = {!!}
-     ;  ←ℕ = λ i → ( ←ℕ N {!!} ,  ←ℕ M {!!})
-     ;  ←Q =  λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
-     ;  finite = {!!}
-     ;  finiso→ = {!!}
-     ;  finiso← = {!!}
-   }
-
-_exp_ : ℕ → ℕ → ℕ
-_exp_ = {!!}
-
-sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) ( 2 exp n )
-sbstFin = {!!}
+exists : { Q : Set} {n  : ℕ } → FiniteSet Q n → ( Q → Bool ) → Bool
+exists {Q} {n} N f = exists1 (max N)
+  where
+     exists1 :  ℕ → Bool
+     exists1 zero = false
+     exists1 (suc i) with f (←ℕ N (suc i) ) 
+     ... | true = true
+     ... | false = exists1 i
 
 list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q n → List Q → Q → Bool
 list2sbst N [] _ = false
@@ -78,7 +47,7 @@
 
 
 δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
-δconv = {!!}
+δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → list2sbst N (nδ r i) q )
 
 subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  
     (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
@@ -88,11 +57,32 @@
      ;  aend = aend1
    } where
      astart1 : Q → Bool
-     astart1 q with sid NFA q  ≟  sid NFA ( nstart NFA )
-     ... | yes _ = true
-     ... | no _ = false
-     aend2 :  ℕ → (Q → Bool)  → Bool
-     aend2 n f = {!!}
+     astart1 = list2sbst N [ nstart NFA ]
      aend1 : (Q → Bool) → Bool
-     aend1 f = aend2 zero f
+     aend1 f = exists N f
 
+-- _div_ : ℕ → ℕ → Maybe ℕ
+-- _div_ x zero = {!!}
+-- _div_ x (suc y) = {!!}
+-- 
+-- _mod_ : ℕ → ℕ → Maybe ℕ
+-- _mod_ = {!!}
+-- 
+-- lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
+-- lemma1 {Q} {R} {zero} {_} N M  = {!!}
+-- lemma1 {Q} {R} {n} {zero} N M  = {!!}
+-- lemma1 {Q} {R} {n} {m} N M = record {
+--         not-zero = {!!}
+--      ;  ←ℕ = λ i → ( ←ℕ N {!!} ,  ←ℕ M {!!})
+--      ;  ←Q =  λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
+--      ;  finite = {!!}
+--      ;  finiso→ = {!!}
+--      ;  finiso← = {!!}
+--    }
+-- 
+-- _exp_ : ℕ → ℕ → ℕ
+-- _exp_ = {!!}
+-- 
+-- sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) ( 2 exp n )
+-- sbstFin = {!!}
+--