# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573676029 -32400
# Node ID fba1cd54581d9b70f174ee3658d7645eb1d296b8
# Parent  a46e0a2a35436aec70b632a38ec54c1e7572b8bc
use exists in cond, nfa example

diff -r a46e0a2a3543 -r fba1cd54581d a02/lecture.ind
--- a/a02/lecture.ind	Wed Nov 13 09:04:48 2019 +0900
+++ b/a02/lecture.ind	Thu Nov 14 05:13:49 2019 +0900
@@ -266,6 +266,8 @@
 
 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
 
+最低限5題をまとめてレポートで提出せよ
+
 <a href="agda/practice-logic.agda"> practice-logic</a> <!---  Exercise 2.2 --->
 
 
diff -r a46e0a2a3543 -r fba1cd54581d a04/lecture.ind
--- a/a04/lecture.ind	Wed Nov 13 09:04:48 2019 +0900
+++ b/a04/lecture.ind	Thu Nov 14 05:13:49 2019 +0900
@@ -4,7 +4,16 @@
 
 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
 
-この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。
+この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。
+
+Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
+にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
+しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。
+
+--Agda での非決定性オートマトン
+
+ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
+部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。
 
     record NAutomaton ( Q : Set ) ( Σ : Set  )
            : Set  where
@@ -12,69 +21,208 @@
               Nδ : Q → Σ → Q → Bool
               Nend  :  Q → Bool
 
-これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
+これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
 
 <a href="../agda/nfa.agda"> nfa.agda </a>
 
-状態の受理と遷移は以下のようになる。
+--NAutomatonの受理と遷移
+
+非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
+入力を読み終わった後に、終了状態になれば受理されることになる。
+
+このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
+
+true になるものは複数あるので、やはり部分集合で表される。つまり、
+
+     exists : ( P : Q → Bool ) → Q → Bool
+
+このような関数を実現する必要がある。
+
+もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。
+
+--finiteSet
+
+Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。
+
+    record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
+         field
+            Q←F : Fin n → Q
+            F←Q : Q → Fin n
+            finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+            finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+
+という感じで、Data.Fin と 状態を対応させる。そうすると、
+
+     lt0 : (n : ℕ) →  n Data.Nat.≤ n
+     lt0 zero = z≤n
+     lt0 (suc n) = s≤s (lt0 n)
+
+     exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
+     exists1  zero  _ _ = false
+     exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
+
+     exists : ( Q → Bool ) → Bool
+     exists p = exists1 n (lt0 n) p 
+
+という形で、 exists を記述することができる。
+
+<a href="../agda/finiteSet.agda"> finiteSet.agda </a>
+
+
+--NAutomatonの受理と遷移
+
+状態の受理と遷移は exists を使って以下のようになる。
 
     Nmoves : { Q : Set } { Σ : Set  }
         → NAutomaton Q  Σ
         → {n : ℕ } → FiniteSet Q  {n}
-        →  ( Q → Bool )  → Σ → Q → Bool
+        →  ( Qs : Q → Bool )  → (s : Σ ) → Q → Bool
     Nmoves {Q} { Σ} M fin  Qs  s q  =
-          exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
+          exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
 
-    Naccept : { Q : Set } { Σ : Set  }
+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  Σ
         → {n : ℕ } → FiniteSet Q {n}
         → (Nstart : Q → Bool) → List  Σ → Bool
-    Naccept M fin sb []  = exists fin ( λ q → sb q ∧ Nend M q )
+    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 になるものであるとする。
+Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
 
 
 --例題
 
-    transition3 : States1  → In2  → States1 → Bool
-    transition3 sr i0 sr = true
-    transition3 sr i1 ss = true
-    transition3 sr i1 sr = true
-    transition3 ss i0 sr = true
-    transition3 ss i1 st = true
-    transition3 st i0 sr = true
-    transition3 st i1 st = true
-    transition3 _ _ _ = false
+例題1.36 を考えよう。状態遷移関数は以下のようになる。
+
+    transition136 : StatesQ  → A2  → StatesQ → Bool
+    transition136 q1 b0 q2 = true
+    transition136 q1 a0 q1 = true  -- q1 → ep → q3
+    transition136 q2 a0 q2 = true
+    transition136 q2 a0 q3 = true
+    transition136 q2 b0 q3 = true
+    transition136 q3 a0 q1 = true
+    transition136 _ _ _ = false
+
+教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
+ことしてしまう。
+
+    end136 : StatesQ → Bool
+    end136  q1 = true
+    end136  _ = false
+
+    start136 : StatesQ → Bool
+    start136 q1 = true
+    start136 _ = false
+
+    nfa136 :  NAutomaton  StatesQ A2
+    nfa136 =  record { Nδ = transition136; Nend = end136 }
+
+<a href=" ../agda/nfa136.agda"> 1.36 の例題  </a>
+
+    example136-1 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ [] )
+
+最初の状態 q1 から a0  ∷ b0  ∷ a0 ∷ [] の入力を受けとる場合を考える。
 
-    fin1 :  States1  → Bool
-    fin1 st = true
-    fin1 ss = false
-    fin1 sr = false
+a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、
+q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
+から行けないが、どれかの経路が成功すれば良いので受理となる。
+
+    example136-2 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
+
+
+--問題
+
+... 作成中...
+
+
+--非決定性オートマトンと決定性オートマトン
 
-    start1 : States1 → Bool
-    start1 sr = true
-    start1 _ = false
+    record Automaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+            δ : Q → Σ → Q
+            aend : Q → Bool
+
+の Q に Q → Bool を入れてみる。
+
+            δ : (Q → Bool ) → Σ → Q → Bool
+            aend : (Q → Bool ) → Bool
+
+これを、
+
+    record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              Nδ : Q → Σ → Q → Bool
+              Nend  :  Q → Bool
 
-    am2  :  NAutomaton  States1 In2
-    am2  =  record { Nδ = transition3 ; Nend = fin1}
+これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。
+
+NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。
+
+遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は
+
+              Nδ : Q → Σ → Q → Bool
+
+だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。
+
+    f q /\ Nδ NFA q i nq
 
-    example2-1 = Naccept am2 finState1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
-    example2-2 = Naccept am2 finState1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )
+これが true になるものを exists を使って探し出す。
+
+    δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
+    δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )
+
+ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。
+ 
+終了条件は
+
+    f q /\ Nend NFA q )
+'
+で良い。 これが true になるものを exists を使って探し出す。
+
+Q が FiniteSet Q {n} であれば
 
-    fin0 :  States1  → Bool
-    fin0 st = false
-    fin0 ss = false
-    fin0 sr = false
+    subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
+        (NAutomaton Q  Σ ) → (astart : Q ) → (Automaton (Q → Bool)  Σ )  
+    subset-construction {Q} { Σ} {n} fin NFA astart = record {
+            δ = λ f i  → δconv fin ( Nδ NFA ) f i 
+         ;  aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
+       } 
+
+という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。
+
+            λ f i  → δconv fin ( Nδ NFA ) f i 
+は
+            λ f i q → δconv fin ( Nδ NFA ) f i q
+
+であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。
+
+<a href=" ../agda/sbconst2.agda"> subset construction  </a>
+
+--subset constructionの状態数
 
-    test0 : Bool
-    test0 = exists finState1 fin0
+実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを
+自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、
 
-    test1 : Bool
-    test1 = exists finState1 fin1
+      q1    q2    q3
+      false false false
+      false false true
+      false true  false
+      false true  true
+      true  false false
+      true  false true
+      true  true  false
+      true  true  true
 
-    test2 = Nmoves am2 finState1 start1
+という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。
 
+アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。
+前もって、可能な状態を Automaton として探し出そうとすると、 指数関数的な爆発になってしまう。
+
+実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。
+
diff -r a46e0a2a3543 -r fba1cd54581d agda/finiteSet.agda
--- a/agda/finiteSet.agda	Wed Nov 13 09:04:48 2019 +0900
+++ b/agda/finiteSet.agda	Thu Nov 14 05:13:49 2019 +0900
@@ -10,6 +10,7 @@
 open import logic
 open import nat
 open import Data.Nat.Properties  hiding ( _≟_ )
+open import Data.List
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -38,6 +39,15 @@
      exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
      exists : ( Q → Bool ) → Bool
      exists p = exists1 n (lt0 n) p 
+
+     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q
+     list1  zero  _ _ = []
+     list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ≤ {m} {n} m<n))) true
+     ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p
+     ... | no  _ = list1 m (lt2 m<n) p
+     to-list : ( Q → Bool ) → List Q
+     to-list p = list1 n (lt0 n) p 
+
      equal? : Q → Q → Bool
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
diff -r a46e0a2a3543 -r fba1cd54581d agda/nfa136.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/nfa136.agda	Thu Nov 14 05:13:49 2019 +0900
@@ -0,0 +1,93 @@
+module nfa136 where
+
+open import logic
+open import nfa
+open import automaton hiding ( StatesQ )
+open import Data.List
+open import finiteSet
+open import Data.Fin
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+data  StatesQ   : Set  where
+   q1 : StatesQ
+   q2 : StatesQ
+   q3 : StatesQ
+
+data  A2   : Set  where
+   a0 : A2
+   b0 : A2
+
+finStateQ : FiniteSet StatesQ 
+finStateQ = record {
+        Q←F = Q←F
+      ; F←Q  = F←Q
+      ; finiso→ = finiso→
+      ; finiso← = finiso←
+   } where
+       Q←F : Fin 3 → StatesQ
+       Q←F zero = q1
+       Q←F (suc zero) = q2
+       Q←F (suc (suc zero)) = q3
+       F←Q : StatesQ → Fin 3
+       F←Q q1 = zero
+       F←Q q2 = suc zero
+       F←Q q3 = suc (suc zero)
+       finiso→ : (q : StatesQ) → Q←F (F←Q q) ≡ q
+       finiso→ q1 = refl
+       finiso→ q2 = refl
+       finiso→ q3 = refl
+       finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
+       finiso← zero = refl
+       finiso← (suc zero) = refl
+       finiso← (suc (suc zero)) = refl
+       finiso← (suc (suc (suc ()))) 
+
+transition136 : StatesQ  → A2  → StatesQ → Bool
+transition136 q1 b0 q2 = true
+transition136 q1 a0 q1 = true  -- q1 → ep → q3
+transition136 q2 a0 q2 = true
+transition136 q2 a0 q3 = true
+transition136 q2 b0 q3 = true
+transition136 q3 a0 q1 = true
+transition136 _ _ _ = false
+
+end136 : StatesQ → Bool
+end136  q1 = true
+end136  _ = false
+
+start136 : StatesQ → Bool
+start136 q1 = true
+start136 _ = false
+
+nfa136 :  NAutomaton  StatesQ A2
+nfa136 =  record { Nδ = transition136; Nend = end136 }
+
+example136-1 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
+
+example136-0 = Naccept nfa136 finStateQ start136( a0 ∷ [] )
+
+example136-2 = Naccept nfa136 finStateQ start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )
+
+open FiniteSet
+
+nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool
+nx now [] = now
+nx now ( i ∷ ni ) = (Nmoves nfa136 finStateQ (nx now ni) i )
+
+example136-3 = to-list finStateQ start136
+example136-4 = to-list finStateQ (nx start136  ( a0  ∷ b0 ∷ a0 ∷ [] ))
+
+open import sbconst2
+
+fm136 : Automaton ( StatesQ → Bool  )  A2
+-- fm136  = record { δ = λ qs q → transition136 {!!} {!!}  ; aend = λ qs → exists finStateQ end136 }
+fm136  = subset-construction finStateQ nfa136 q1
+
+open NAutomaton
+
+lemma136 : ( x : List A2 ) → Naccept nfa136 finStateQ start136 x  ≡ accept fm136 start136 x 
+lemma136 x = lemma136-1 x start136 where
+    lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
+        → Naccept nfa136 finStateQ states x  ≡ accept fm136 states x 
+    lemma136-1 [] _ = refl
+    lemma136-1 (h ∷ t) states = lemma136-1 t (δconv finStateQ (Nδ nfa136) states h)
diff -r a46e0a2a3543 -r fba1cd54581d agda/regular-language.agda
--- a/agda/regular-language.agda	Wed Nov 13 09:04:48 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 14 05:13:49 2019 +0900
@@ -282,32 +282,34 @@
 
     open Found
 
-    data AB-state (nq : states A ∨ states B → Bool ) (qa : states A) (x : List Σ) :  Set (Level.suc Level.zero) where
-       state-A  : ((q : states A ∨ states B ) → nq q ≡ true → q ≡ case1 qa ) → AB-state nq qa x
-       state-AB : ((q : states A ∨ states B ) → ( nq q ≡ true ) →
-           ( (q ≡ case1 qa)  ∨
-           ( ({ qa' : states A} → (¬ (q ≡ case1 qa'))) ∧ ({qb : states B} → nq (case2 qb) ≡ true →   ( accept (automaton B) qb x ≡ false ) ))))
-           → AB-state nq qa x
+    data AB-state (nq : states A ∨ states B → Bool ) (x : List Σ) :  Set (Level.suc Level.zero) where
+       state-A  : ((q : states A ∨ states B ) → nq q ≡ true → (exists (afin A) (λ qa → equal? finab q (case1 qa) ) ≡ true )) → AB-state nq x
+       state-AB : ((q : states A ∨ states B ) → nq q ≡ true → (exists (afin B) (λ qb → equal? finab q (case2 qb) /\ accept (automaton B) qb x ) ≡ true ))
+                → AB-state nq  x
 
     open AB-state
+
+    start-eq  : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → exists (afin A) (λ qa → equal? finab q (case1 qa)) ≡ true
+    start-eq q eq with equal→refl finab eq
+    ... | refl =  found (afin A) (astart A) eq
+
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
-          → (qa : states A )  → AB-state nq qa x
+          → (qa : states A )  → AB-state nq x
           → split (accept (automaton A) qa ) (contain B) x ≡ true
     contain-A [] nq fn qa cond with found← finab fn | found-q (found← finab fn) | cond | inspect found-q (found← finab fn)
-    contain-A [] nq fn qa cond | S | s | state-A nq=t | record { eq = refl }  with  nq=t (found-q S) (bool-∧→tt-0 (found-p S))
-    ... | refl  = bool-∧→tt-1 (found-p S)
+    contain-A [] nq fn qa cond | S | s | state-A q=qa | record { eq = refl }  = {!!}
+    -- ... | refl = bool-∧→tt-1 (found-p S)
     contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S)) 
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl =  bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | case2 accept-B = ⊥-elim ( lemma11 (proj2 accept-B) )  where
-        lemma11 :  (  nq (case2 qb ) ≡ true → aend (automaton B) qb ≡ false ) → ⊥
-        lemma11  accept-B = ¬-bool ( accept-B (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S ))
-    contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl }  | case2 accept-B = ⊥-elim ( (proj1 accept-B ) refl )
+    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | q=qb = ⊥-elim (lemma11 {!!}) where 
+        lemma11 :  ( {qb : states B } → ((found-q S) ≡ case2 qb) ∧ ((aend (automaton B) qb ) ≡ false)) → ⊥
+        lemma11 q=qb  = ¬-bool (proj2 q=qb ) (bool-∧→tt-1 (found-p S ))
+    contain-A [] nq fn qa cond | S | (case1 qa') | state-AB cond-b | record { eq = refl }   |  q=qb = {!!}
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
     ... | yes eq = bool-or-41 eq
     ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h)  {!!} ) where
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) {!!} where
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (state-A start-eq )
 
     closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
     closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C