Mercurial > hg > Members > kono > Proof > automaton

changeset 14:7eb71391088c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 17:22:49 +0900
parents 02b4ecc9972c
children 54382de19264
files agda/sbconst1.agda
diffstat 1 files changed, 25 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/agda/sbconst1.agda	Fri Aug 24 17:03:40 2018 +0900
+++ b/agda/sbconst1.agda	Fri Aug 24 17:22:49 2018 +0900
@@ -31,15 +31,17 @@
 --           nstart : Q
 --           nend  : Q → Bool
 
-record FiniteSet ( Q : Set ) ( max : ℕ  )
+record FiniteSet ( Q : Set ) ( max1 : ℕ  )
         : Set  where
      field
-        not-zero : max > 0
+        not-zero : max1 > 0
         ←ℕ : ℕ → Q
         ←Q : Q → ℕ 
-        finite : (q : Q) → ←Q q < max
+        finite : (q : Q) → ←Q q < max1
         finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
         finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
+     max : ℕ
+     max = max1
 
 open FiniteSet
 
@@ -65,7 +67,7 @@
 _exp_ : ℕ → ℕ → ℕ
 _exp_ = {!!}
 
-sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) {!!} 
+sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) ( 2 exp n )
 sbstFin = {!!}
 
 list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q n → List Q → Q → Bool
@@ -75,3 +77,22 @@
 ... | no _ = list2sbst N t q
 
 
+δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
+δconv = {!!}
+
+subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  
+    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
+subset-construction {Q} { Σ} {n} N NFA = record {
+        δ = λ q x → δconv N ( nδ NFA ) q x
+     ;  astart = astart1
+     ;  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 = {!!}
+     aend1 : (Q → Bool) → Bool
+     aend1 f = aend2 zero f
+