diff a04/lecture.ind @ 326:a3fb231feeb9

omega
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 21 Jan 2022 10:45:42 +0900 (2022-01-21)
parents b3f05cd08d24
children 9324852d3a17
line wrap: on
line diff
--- a/a04/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a04/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -66,6 +66,29 @@
 
 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
 
+--状態と入力の List を使って深さ優先探索する
+
+    {-# TERMINATING #-}
+    NtraceDepth : { Q : Set } { Σ : Set  } 
+        → NAutomaton Q  Σ
+        → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
+    NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
+        ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
+        ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
+        ndepth1 q i [] is t t1 = t1
+        ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
+        ndepth [] sb is t t1 =  t1
+        ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
+        ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
+        ... | false =  ndepth qs sb [] t t1
+        ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
+        ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
+        ... | false = ndepth qs sb (i ∷ is) t t1
+
+確かに動く。しかし、複雑すぎる。
+
+--状態の部分集合を使う
+
 true になるものは複数あるので、やはり部分集合で表される。つまり、
 
      exists : ( P : Q → Bool ) → Q → Bool
@@ -76,6 +99,8 @@
 
 --finiteSet
 
+有限な集合を表すのに、個々の data を使えばよいが、統一的に扱いたい。Agda には Data.Fin が用意されている。
+
 Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。
 
     record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
@@ -116,7 +141,7 @@
 
 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
-遷移可能になる。
+遷移可能になる。(だいぶ簡単になった)
 
     Naccept : { Q : Set } { Σ : Set  } 
         → NAutomaton Q  Σ
@@ -168,10 +193,6 @@
     example136-2 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
 
 
---問題
-
-... 作成中...
-
 
 --非決定性オートマトンと決定性オートマトン
 
@@ -216,7 +237,7 @@
 終了条件は
 
     f q /\ Nend NFA q )
-'
+
 で良い。 これが true になるものを exists を使って探し出す。
 
 Q が FiniteSet Q {n} であれば
@@ -236,6 +257,8 @@
 
 であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。
 
+これで実際に、NFAから DFA を作成することができた。ここで、状態の有限性を使っていることを確認しよう。
+
 <a href=" ../agda/sbconst2.agda"> subset construction  </a>
 
 --subset constructionの状態数
@@ -260,3 +283,19 @@
 
 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。
 
+--NFAの実行
+
+subset construction した automaton はすべての状態を生成する前でも実行することができる。
+ただし、毎回、nest した exists を実行することになる。
+
+
+
+
+
+
+
+
+
+
+
+