diff a04/lecture.ind @ 69:f124fceba460

subset construction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 06 Nov 2019 17:18:58 +0900 (2019-11-06)
parents a7f09c9a2c7a
children fba1cd54581d
line wrap: on
line diff
--- a/a04/lecture.ind	Thu Oct 31 21:41:54 2019 +0900
+++ b/a04/lecture.ind	Wed Nov 06 17:18:58 2019 +0900
@@ -9,65 +9,14 @@
     record NAutomaton ( Q : Set ) ( Σ : Set  )
            : Set  where
         field
-              nδ : Q → Σ → List Q
-              sid : Q  →  ℕ
-              nstart : Q
-              nend  : Q → Bool
+              Nδ : Q → Σ → Q → Bool
+              Nend  :  Q → Bool
 
 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
 
-次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
-
-少し複雑がだが、insert と merge を定義して、
-
-<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
-
-    insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
-    insert  M  [] q =  q ∷ []
-    insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
-    ... | yes _ = insert  M  T q'
-    ... | no _ = q  ∷ (insert  M  T q' )
-
-    merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
-    merge  M L1 [] = L1
-    merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H
-
-    Nmoves : { Q : Set } { Σ : Set  }
-        → NAutomaton Q  Σ
-        → List Q → List  Σ → List Q
-    Nmoves {Q} { Σ} M q L = Nmoves1 q L []
-       where
-          Nmoves1 : (q : List Q ) ( L : List  Σ ) → List Q → List Q
-          Nmoves1 q  [] _ = q
-          Nmoves1 []  (_  ∷ L) LQ = Nmoves1 LQ L []
-          Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )
+<a href="../agda/nfa.agda"> nfa.agda </a>
 
-    Naccept : { Q : Set } { Σ : Set  }
-        → NAutomaton Q  Σ
-        →  List  Σ → Bool
-    Naccept {Q} { Σ} M L =
-           checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
-       where
-          checkAccept : (q : List Q ) → Bool
-          checkAccept [] = false
-          checkAccept ( H ∷ L ) with (nend M) H
-          ... | true = true
-          ... | false = checkAccept L
-
-とする。 
-
---部分集合を使うと簡単になる
-
-<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
-
-
-    record NAutomaton ( Q : Set ) ( Σ : Set  )
-           : Set  where
-        field
-              Nδ : Q → Σ → Q → Bool
-              Nstart : Q → Bool
-              Nend  :  Q → Bool
-
+状態の受理と遷移は以下のようになる。
 
     Nmoves : { Q : Set } { Σ : Set  }
         → NAutomaton Q  Σ
@@ -76,16 +25,18 @@
     Nmoves {Q} { Σ} M fin  Qs  s q  =
           exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
 
-
-    Naccept : { Q : Set } { Σ : Set  } 
+    Naccept : { Q : Set } { Σ : Set  }
         → NAutomaton Q  Σ
         → {n : ℕ } → FiniteSet Q {n}
-        → List  Σ  → Bool
-    Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
-       where
-          Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
-          Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
-          Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t
+        → (Nstart : Q → Bool) → List  Σ → Bool
+    Naccept M fin sb []  = exists fin ( λ q → sb q ∧ Nend M q )
+    Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M  fin sb i ) t
+
+次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
+しかし、List で定義すると少し複雑になる。
+
+部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。
+
 
 --例題
 
@@ -109,9 +60,21 @@
     start1 _ = false
 
     am2  :  NAutomaton  States1 In2
-    am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
+    am2  =  record { Nδ = transition3 ; Nend = fin1}
+
+    example2-1 = Naccept am2 finState1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+    example2-2 = Naccept am2 finState1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-    example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
-    example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+    fin0 :  States1  → Bool
+    fin0 st = false
+    fin0 ss = false
+    fin0 sr = false
 
+    test0 : Bool
+    test0 = exists finState1 fin0
 
+    test1 : Bool
+    test1 = exists finState1 fin1
+
+    test2 = Nmoves am2 finState1 start1
+