--- a/a04/lecture.ind	Thu Nov 16 17:40:42 2023 +0900
+++ b/a04/lecture.ind	Wed Nov 22 17:07:01 2023 +0900
@@ -140,50 +140,16 @@
 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
 入力を読み終わった後に、終了状態になれば受理されることになる。
 
-このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
+このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。これを
 
---状態と入力の List を使って深さ優先探索する
+     exists : ( P : Q → Bool ) → Bool
 
-    {-# 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
+として定義する。この気持ちは P 満たす状態Qが一つはあるということ。それは自分で保証するようにかく。
 
-確かに動く。しかし、複雑すぎる。
-
---状態の部分集合を使う
-
-true になるものは複数あるので、やはり部分集合で表される。つまり、
-
-     exists : ( P : Q → Bool ) → Q → Bool
-
-このような関数を実現する必要がある。
-
-もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。
-
-
---NAutomatonの受理と遷移
+状態が有限なら、FiniteSet の exists を使える。
 
 状態の受理と遷移は exists を使って以下のようになる。
 
-    Nmoves : { Q : Set } { Σ : Set  }
-        → NAutomaton Q  Σ
-        → (exists : ( Q → Bool ) → Bool)
-        →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
-    Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
-
 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
 遷移可能になる。(だいぶ簡単になった)
@@ -198,6 +164,26 @@
 
 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
 
+--Ntrace 
+
+Qをすべて含む List Qを用意すれば、状態と入力の List から、状態の集合のListを作ることができる。
+
+    Ntrace : { Q : Set } { Σ : Set  } 
+        → NAutomaton Q  Σ
+        → (all-states : List Q )
+        → (exists : ( Q → Bool ) → Bool)
+        → (Nstart : Q → Bool) → List  Σ → List (List Q)
+    Ntrace M all-states exists sb []  = to-list all-states ( λ q → sb q /\ Nend M q ) ∷ []
+    Ntrace M all-states exists sb (i ∷ t ) =
+        to-list all-states (λ q →  sb q ) ∷
+        Ntrace M all-states exists (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t
+
+たとえば、
+
+    Ntrace am2 LStates1  existsS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+
+のように呼び出す。
+
 --例題
 
 例題1.36 を考えよう。状態遷移関数は以下のようになる。
@@ -237,6 +223,12 @@
 
     example136-2 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
 
+---問題4.1 NFAのtrace
+
+
+<a href="../exercise/007.html"> NFAのtrace </a> <!--- Exercise 4.1 --->
+
+Ntrace を修正すればよい。
 
 
 
@@ -248,4 +240,3 @@
 
 
 
-