# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1700640421 -32400
# Node ID db02b6938e0431ec0acb4559368518247ff7518e
# Parent  4e4acdc43dee2730731662fa6489d7642eaa0ec8
StarProp and Ntrace

diff -r 4e4acdc43dee -r db02b6938e04 a04/lecture.ind
--- 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 @@
 
 
 
-
diff -r 4e4acdc43dee -r db02b6938e04 automaton-in-agda/src/nfa136.agda
--- a/automaton-in-agda/src/nfa136.agda	Thu Nov 16 17:40:42 2023 +0900
+++ b/automaton-in-agda/src/nfa136.agda	Wed Nov 22 17:07:01 2023 +0900
@@ -97,7 +97,9 @@
 
 aδ : Q2 → Σ2 → Q2 
 aδ a0 ca = a1 
-aδ a0 _ = af 
+aδ a0 cb = af
+aδ a0 cc = af
+aδ a0 cf = af
 aδ a1 cf = ae 
 aδ a1 _ = a1 
 aδ ae cf = ae 
@@ -109,13 +111,15 @@
 test111 : Bool
 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
 
+-- b.*f
+
 b-end : Q2 → Bool
 b-end be = true
 b-end _ = false
 
 bδ : Q2 → Σ2 → Q2 
-bδ b0 cb = b1 
-bδ b0 _ = bf 
+bδ ae cb = b1 
+bδ ae _ = bf 
 bδ b1 cf = be 
 bδ b1 _ = b1 
 bδ be cf = be 
@@ -129,13 +133,20 @@
 
 open import regular-language
 
+-- (a.*f)(b.*f)    -- a.*(fb).*f
 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
+--                                                  a0   ae   b0   b1   be 
+test117 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ ca ∷ cb ∷ ca ∷ cf ∷ cf ∷ [] )
+--                                                  a0   ae   a0   b0   b1   be
+--                                                  a0   ae   ae   b0   b1   be
 
 naδ : Q2 → Σ2 → Q2 → Bool
 naδ a0 ca a1 = true
 naδ a0 _ _ = false
 naδ a1 cf ae = true
 naδ a1 _ a1 = true
+naδ ae cf ae = true
+naδ ae _ a1 = true
 naδ _ _ _ = false
 
 a-start : Q2 → Bool
@@ -160,6 +171,8 @@
 nbδ ae _ _ = false
 nbδ b1 cf be = true
 nbδ b1 _ b1 = true
+nbδ be cf be = true
+nbδ be _ b1 = true
 nbδ _ _ _ = false
 
 b-start : Q2 → Bool
@@ -170,7 +183,7 @@
 nfa-b = record { Nδ = nbδ ; Nend = b-end }
 
 nfa-b-exists : (Q2 → Bool) → Bool
-nfa-b-exists p = p b0 \/ p b1 \/ p ae
+nfa-b-exists p = p b0 \/ p b1 \/ p be
 
 -- (a.*f)(b.*f)
 
@@ -183,11 +196,23 @@
 nfa-ab-exists : (Q2 → Bool) → Bool
 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p
 
+test-ab1-data : List Σ2
+test-ab1-data = ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
+
 test-ab1 : Bool
-test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
+test-ab1 = Naccept nfa-ab nfa-ab-exists a-start test-ab1-data  -- should be false
+
+test-ab2-data : List Σ2
+test-ab2-data = ( ca ∷ cf ∷ ca ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
 
 test-ab2 : Bool
-test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
+test-ab2 = Naccept nfa-ab nfa-ab-exists a-start test-ab2-data   -- should be true
+
+q2-list : List Q2
+q2-list = a0 ∷ a1 ∷ ae ∷ af ∷ b0 ∷ b1 ∷ be ∷ bf ∷ []
+
+test-tr : List (List Q2)
+test-tr = Ntrace nfa-ab q2-list nfa-ab-exists a-start ( ca ∷ cf ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
 
 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
 
@@ -200,9 +225,36 @@
 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
 -- 
+open import regex
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+Σ2-cmp : (x y : Σ2 ) → Dec (x ≡ y)
+Σ2-cmp ca ca = yes refl
+Σ2-cmp ca cb = no (λ ())
+Σ2-cmp ca cc = no (λ ())    
+Σ2-cmp ca cf = no (λ ())    
+Σ2-cmp cb ca =  no (λ ())
+Σ2-cmp cb cb = yes refl
+Σ2-cmp cb cc =  no (λ ())
+Σ2-cmp cb cf =  no (λ ())
+Σ2-cmp cc ca =  no (λ ())
+Σ2-cmp cc cb =  no (λ ())
+Σ2-cmp cc cc = yes refl
+Σ2-cmp cc cf =  no (λ ())
+Σ2-cmp cf ca =  no (λ ())
+Σ2-cmp cf cb =  no (λ ())
+Σ2-cmp cf cc =  no (λ ())
+Σ2-cmp cf cf = yes refl
+
+Σ2-any :  Regex Σ2
+Σ2-any = < ca > || < cb > || < cc > || < cf >
+
+test-ab1-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > )  )  Σ2-cmp test-ab1-data ≡ false
+test-ab1-regex = refl
+
+test-ab2-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > )  )  Σ2-cmp test-ab2-data ≡ true
+test-ab2-regex = refl
 
 
 
 
-
-
diff -r 4e4acdc43dee -r db02b6938e04 automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Thu Nov 16 17:40:42 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 22 17:07:01 2023 +0900
@@ -42,7 +42,7 @@
 --
 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
-repeat2 x pre [] = false
+repeat2 x pre [] = true
 repeat2 x pre (h ∷ y) = 
    (x (pre ++ (h ∷ [])) /\ repeat x y )
    \/ repeat2 x (pre ++ (h ∷ [])) y 
@@ -211,3 +211,37 @@
 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S)  )
   
 
+-- low of exclude middle of Split A B x
+lemma-concat : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Split A B x ∨ ( ¬ Split A B x )
+lemma-concat {Σ} A B x with split A B x in eq
+... | true = case1 (split→AB A B x eq )
+... | false = case2 (λ p →  ¬-bool eq (split→AB1 A B x p )) 
+
+-- Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+-- Concat {Σ} A B = split A B
+
+Concat' : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Set
+Concat' {Σ} A B = λ x → Split A B x
+
+record StarProp {Σ : Set} (A : List Σ → Bool ) (x :  List Σ ) : Set where
+    field
+        spn : List ( List Σ )
+        spn-concat : foldr (λ k → k ++_ ) [] spn ≡ x
+        propn : foldr (λ k → λ j → A k /\ j ) true spn ≡ true
+
+open StarProp
+
+Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
+Star→StarProp = ?
+
+StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
+StarProp→Star {Σ} A x sp = subst (λ k →  Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where
+     spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x
+     spsx y refl = spn-concat sp 
+     sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true
+     sps1 = ?
+
+
+lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x )
+lemma-starprop = ?
+