--- a/a03/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a03/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -50,7 +50,7 @@
         true   : Bool
         false  : Bool
 
-で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか?)
+で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか? Set を使わないのはなぜか)
 
 start state はrecordで定義しない方が便利だと言うことがこの後わかる。
 
@@ -154,8 +154,26 @@
 
 文字列の部分集合を (Automaton の専門用語として) Language という。でたらめの発声の部分集合が日本語なので言語といえなくもない。
 
+    language : { Σ : Set } → Set
+    language {Σ} = List Σ → Bool
+
 なんらかのAutomaton が受け付ける文字列の部分集合を Regular Language という。この範囲に収まらない Language も後で調べる。
 
+
+--Agda によるRegular Languageの集合演算
+
+何かのAutomaton で判定される言語は ∃ automaton だが、これを record で書く。
+
+    record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
+       field
+          states : Set 
+          astart : states 
+          automaton : Automaton states Σ
+       contain : List Σ → Bool
+       contain x = accept automaton astart x
+
+contain が language の定義の形になっていることを確認しよう。
+
 --Regular Languageの演算
 
 Regular Languageは以下の演算に付いて閉じていることが知られている。閉じているとは以下の集合演算をしても、それはやはり
@@ -169,27 +187,7 @@
 
 <a href="../agda/regular-language.agda"> Agda での Regular Language </a>
 
-
---Agda によるRegular Languageの集合演算
-
-部分集合は true / false で判断する。
-
-    language : { Σ : Set } → Set
-    language {Σ} = List Σ → Bool
-
-何かのAutomaton で判定される言語は ∃ automaton だが、これを record で書く。
-
-    record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
-       field
-          states : Set 
-          astart : states 
-          automaton : Automaton states Σ
-       contain : List Σ → Bool
-       contain x = accept automaton astart x
-
-contain が language の定義の形になっていることを確認しよう。
-
-Unio は Bool 演算を使って簡単に表される。
+Union は Bool 演算を使って簡単に表される。
 
     Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
     Union {Σ} A B x = (A x ) \/ (B x)
@@ -201,7 +199,7 @@
 
 前半と後半の分け方には非決定性がある。
 
---Split
+--Split による List の分割
 
 i0 ∷ i1 ∷ i0 ∷ [] の分け方は and と or で以下のようになる。
 
@@ -210,7 +208,7 @@
        ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
        ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
 
-これを作ってやればよい。
+Agda は高階論理なので、これを任意長の List に対して定義できる。
 
     split : {Σ : Set} → (List Σ → Bool)
           → ( List Σ → Bool) → List Σ → Bool
@@ -235,9 +233,10 @@
 
     {-# TERMINATING #-}
     Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
-    Star {Σ} A = split A ( Star {Σ} A )
+    Star {Σ} A [] = true
+    Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)
 
-{-# TERMINATING #-}は Agda が停止性を判定できないというエラーを抑止する。
+{-# TERMINATING #-}は Agda が停止性を判定できないというエラーを抑止するのだった。
 
 --Union が RegularLanguage で閉じていること
 
@@ -256,13 +255,33 @@
 
 で、これは Automaton を具体的に作る必要がある。
 
-この証明は比較的やさしい。
+この証明は M-Union の定義とUnionが同じことなので簡単に証明できる。
 
 
 --Concat が RegularLanguage で閉じていること
 
 これは割と難しい。Automaton の状態が有限であることが必要になる。
 
+A x ≡ contain r x は両辺が true の場合と false の場合がある。これを示すことになる。
 
+    ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+
+をつかって
 
+    closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
+    closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
+    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
+    closed-in-concat→ = ?
+    closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
+    closed-in-concat← = ?
 
+とする。
+
+問題は  M-Concat A B つまり、Concat を受け付ける automaton をどうやって定義するかになる。
+
+これは次の lecture で行う。
+
+--Star が RegularLanguage で閉じていること
+
+これも問題は上と同じだが...
+