--- a/a02/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a02/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -284,8 +284,142 @@
 
 <a href="agda/record1.agda"> record1</a> <!---  Exercise 2.2 --->
 
---Sum type
+--data -- Sum type
+
+record は  ∧ に対応するが、∨はどうすれば良いのか。残念ながら∧と対称につくることはできない。(なぜか?)
+
+Agda では data という場合分けをする型を導入する。Curry Howard対応が成立する様に、論理記号に対応する
+型を導入する。型には導入と削除がある。
+
+導入のない data を定義すると、それを矛盾として使うことができる。それを使って否定を定義する。
+
+さらに
+
+  有限な要素を持つ集合(型)
+  自然数
+  λ項の等しさとしての等式
+  不等号
+
+も data を使って定義できる。
+
+data は invariant あるいは、制約付きのデータ構造を表すこともできる。
+
+さらに、
+
+　規則にしたがって生成される集合
+
+も表すことができる。一つ一つ、ゆっくり片付けていこう。
 
 <a href="sumtype.html"> Sum type 排他的論理和</a> 
 
+以下は必要に応じて説明していく。
 
+--λ計算の進み方
+
+Agda の値と型は項で定義されていて、それを簡約化することにより計算が進む。
+   
+Agda (そして Haskell )は、項を簡約化していくことにより計算が進むプログラミング言語である。
+
+簡約化の順序には自由度があり、それは実装にって変わる。
+
+　関数適用にる置き換え
+　場合分けによる変数の確定
+  確定した変数での置き換え
+
+自由度に関係なく、項は決まった形に簡約化されるようにλ計算は作られている。(合流性 -- 要証明だが、割と難しい)
+
+(Agda で Agda を実装できるのか?)
+
+合流性があるので、data で定義された等号が正しく動作する。
+
+変数が含まれている場合の等号は単一化と呼ばれる。変数の置き換えが置きるのは data の場合分けと、関数呼び出しの二種類になる。
+
+--停止性の問題
+
+入力を data の場合分けで分解していくことは、入力が決まった大きさの項なので、必ず有限回しかできない。
+
+つまり、そういう計算が止まることは Agda にはわかる。例えば List や Nat の分解である。
+
+分解は再帰的なので、再帰呼び出しがとまるかどうかは、再帰呼び出しの引数が、dataの分解になっているかどうかで判断される。
+
+これは一般的なプログラムでは自明にはならない。その時には型チェックエラーになる。 {-# TERMINATING #-} を指定することにより
+それを抑制できる。その場合は、そういう止まるとすればという仮定を持つ計算あるいは証明になる。
+
+-- induction
+
+自明な停止条件でない推論もいくつかある。
+
+   引数が直接 data を分解しないが、引数が減少する自然数に対応する場合
+   生成される引数パターンが有限だと分かっている場合
+
+の二つの場合は Agda で induction を定義できる。
+
+--古典論理、一階述語論理との差
+
+Agda の → ∧ ∨ は、項の型として定義されている。
+
+  _∧_  : Set → Set → Set 
+
+古典論理では真と偽の二つしかない。
+
+   data Bool : Set where
+       true : Bool
+       false : Bool
+
+この差は、二重否定の扱いに現れる。
+
+    _/\_ : Bool → Bool → Bool 
+    true /\ true = true
+    _ /\ _ = false
+
+    _\/_ : Bool → Bool → Bool 
+    false \/ false = false
+    _ \/ _ = true
+
+    not_ : Bool → Bool 
+    not true = false
+    not false = true 
+
+
+とする。
+
+以下は Bool では証明できるが、Set では示せない。
+
+    lem-in-bool :  (b : Bool) →  not p \/ p
+    lem-in-bool = ? 
+
+    double-negation-bool :  {B : Bool}  → not (not B) → B
+    double-negation-bool = ?
+
+Set の方では対偶は一方向しか成立しない。また、二重否定や排中律も成立しない。
+
+    contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+    contra-position {n} {m} {A} {B}  f ¬b a ?
+
+これは、Agdaの Set が具体的なλ項を要求するためである。つまり、
+
+　　実際に構成できる証明しか Set は受け付けない
+
+Bool の場合は最初から true / false がわかっている。Set の場合は、そこに入る項がある、入らないことを証明する項がある。
+そして、どちらかわからない場合がある。
+
+実際にわからない場合があることが証明されている(不完全性定理)。一方で、
+
+　　証明するべき式が恒真(すべての可能な入力について真)なら、証明がある(完全性)
+
+であることも証明されている。恒真かどうかはわからないので、この二つは矛盾しない。
+
+
+--一階述語論理の定義
+
+Agda を使って一階述語論理を定義することもできる。
+
+
+
+
+
+
+
+
+
+

--- 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 で閉じていること
+
+これも問題は上と同じだが...
+

--- 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 を実行することになる。
+
+
+
+
+
+
+
+
+
+
+
+

--- a/a05/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a05/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -1,11 +1,10 @@
 -title: 正規表現
 
+Regular language は union / concat / * について閉じているので、この演算を
+使って構築する方法がある。
+
 --受理集合と演算
 
-automaton で受理されるのは文字列。あるautomatonnは受理される文字列の集合を決める。
-
-文字列の集合への演算を考えよう
-
    x      文字列そのもの
    x+y    文字列の結合
    *      文字列の繰り返し
@@ -41,6 +40,10 @@
 
 Option : 実行時間を測定してみよう。
 
+  (a|b)*a(a|b)n
+
+(a|b)n は(a|b)のn個の連続は指数関数時間がかか4ることが知られている。 ReDOS 攻撃と呼ばれている。
+
 --正規表現を表すデータ構造
 
 再帰的な構文木を表すには data を使うことができる。
@@ -53,7 +56,7 @@
 
 List Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
 
-<a href="../agda/regex1.agda"> regex1.agda </a>
+<a href="../agda/regex.agda"> regex.agda </a>
 
 上の例題は、
 
@@ -71,6 +74,8 @@
 
 となる。
 
+<a href="../agda/regex1.agda"> regex1.agda </a>
+
 --正規言語
 
 ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。
@@ -99,7 +104,7 @@
     regular-language < h > f (i1  ∷ [] ) = true
     regular-language < h > f _ = false
 
-で良い。そうっでないなら、
+で良い。そうでないなら、
 
     cmp : (x y : Σ )→ Dec ( x ≡ y )
 
@@ -123,83 +128,6 @@
       yes : ( p :   P) → Dec P
       no  : (¬p : ¬ P) → Dec P
 
---Finite Set
-
-有限集合 Fin n は、
-
-    test1 : Fin 2 → Bool
-    test1 0 → true
-    test1 1 → true
-    test1 2 → true
-
-などのように使いたい。0,1,2 は Data.Nat なのでだめである。Agda には Data.Fin が用意されている。
-
-    data Fin : ℕ → Set where
-      zero : {n : ℕ} → Fin (suc n)
-      suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
-
-実際に test1 がどのようになるかを Agda で確認すると、
-
-    test4 : Fin 2 → Bool
-    test4 zero = { }0
-    test4 (suc zero) = { }1
-    test4 (suc (suc ()))
-
-ここで () はあり得ない入力を表す。あり得ないので body は空である。
-
-(Agda での否定を思い出そう)
-
---Finite Set の構成
-
-<a href="../agda/nfa.agda"> nfa.agda </a>
-
-    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
-         lt0 : (n : ℕ) →  n Data.Nat.≤ n
-         lt0 zero = z≤n
-         lt0 (suc n) = s≤s (lt0 n)
-         lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
-         lt2 {zero} lt = z≤n
-         lt2 {suc m} {zero} ()
-         lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
-         exists : ( Q → Bool ) → Bool
-         exists p = exists1 n (lt0 n) p where
-             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
-
-    finState1 : FiniteSet States1
-    finState1 = record {
-            Q←F = Q←F
-          ; F←Q  = F←Q
-          ; finiso→ = finiso→
-          ; finiso← = finiso←
-       } where
-           Q←F : Fin 3 → States1
-           Q←F zero = sr
-           Q←F (suc zero) = ss
-           Q←F (suc (suc zero)) = st
-           Q←F (suc (suc (suc ())))
-           F←Q : States1 → Fin 3
-           F←Q sr = zero
-           F←Q ss = suc (zero)
-           F←Q st = suc ( suc zero )
-           finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
-           finiso→ sr = refl
-           finiso→ ss = refl
-           finiso→ st = 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 ())))
-
-
 
 -- x & y
 
@@ -207,15 +135,16 @@
 
     split : {Σ : Set} → (List Σ → Bool)
           → ( List Σ → Bool) → List Σ → Bool
+    split x y  [] = x [] ∧ y []
+    split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
+      split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
+
 
 があれば、
 
-    _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
-    x ・ y = λ z → split x y z
+    regular-language (x & y) cmp  = split ( λ z → regular-language x  cmp z ) (λ z →  regular-language y  cmp z )
 
-    regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
-
--- x & y
+-- x *
 
     repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
     repeat x [] = true
@@ -224,14 +153,6 @@
     regular-language (x *) f = repeat ( regular-language x f )
 
 
---split
-
-    split : {Σ : Set} → (List Σ → Bool)
-          → ( List Σ → Bool) → List Σ → Bool
-    split x y  [] = x [] ∧ y []
-    split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
-      split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
-
 
 --問題5.2 - 5.7
 

--- a/a06/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a06/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -1,21 +1,116 @@
 -title: 正規表現とオートマトン
 
---ε遷移とオートマトンの組合せ
+正規表現は、Automaton と同じ言語であることが期待される。つまり、
+
+　正規表現から、それと同じ language を受け付ける Automaton 
+
+を作ればよい。
+
+--ε遷移と非決定性オートマトンの合成による方法
+
+教科書にはこの方法が記述されている。
 
 文字の入力がなくても状態遷移が可能であるとすると、オートマトンの組合せが楽になる。
 
 文字を消費しない遷移を ε遷移と言う。ε遷移可能な状態をまとめて一つの状態と見れば、ε遷移のないNFAに変換できる。
 
-<a href="../agda/epautomaton.agda"> ε automatocn </a>
+そして、それを subset construction で DFA にすれば良い。
 
---正規表現とオートマトンの組合せ
+実際に、M-Concat などで合成を実行することができる。
 
-<a href="../agda/regex.agda"> regex.agda </a>
+しかし、もう少し直接的な方法も存在する。
 
 --微分法
 
+ある正規表現を考えた時に、それを
+
+　　空列を受け付けるかどうか
+　　個々の文字列を一文字受け付けたらどうなるか
+
+と考える。
+
 <center><img src="fig/derivation.svg"> </center>
 
+まず空列を受け付けるかどうか判定する。
+
+    empty? : Regex  Σ → Bool
+    empty?  ε       = true
+    empty?  φ       = false
+    empty? (x *)    = true
+    empty? (x & y)  = empty? x /\ empty? y
+    empty? (x || y) = empty? x \/ empty? y
+    empty? < x >    = false
+
+正規表現の変形を実行する
+
+    derivative :  Regex  Σ → Σ → Regex  Σ
+    derivative ε s = φ
+    derivative φ s = φ
+    derivative (x *) s with derivative x s
+    ... | ε = x *
+    ... | φ = φ
+    ... | t = t & (x *)
+    derivative (x & y) s with empty? x
+    ... | true with derivative x s | derivative y s
+    ... | ε | φ = φ
+    ... | ε | t = y || t
+    ... | φ | t = t
+    ... | x1 | φ = x1 & y
+    ... | x1 | y1 = (x1 & y) || y1
+    derivative (x & y) s | false with derivative x s 
+    ... | ε = y
+    ... | φ = φ
+    ... | t = t & y
+    derivative (x || y) s with derivative x s | derivative y s
+    ... | φ | y1 = y1
+    ... | x1 | φ = x1
+    ... | x1 | y1 = x1 || y1
+    derivative < x > s with eq? x s
+    ... | yes _ = ε
+    ... | no  _ = φ
+
+ここで、
+
+     eq? : (x y : Σ) → Dec (x ≡ y)
+
+があることを使っている。
+
+これの繰り返しで選れる正規表現の集合を data を使って表現できる。
+
+    data regex-states (x : Regex  Σ ) : Regex  Σ → Set where
+        unit   : regex-states x x
+        derive : { y : Regex  Σ } → regex-states x y → (s : Σ)  → regex-states x ( derivative y s )
+
+    record Derivative (x : Regex  Σ ) : Set where
+        field
+           state : Regex  Σ
+           is-derived : regex-states x state
+
+これを状態にして Automaton を構成できる。
+
+    regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
+    regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s 
+            ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) }  where
+        derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
+        derive-step d0 s = derive (is-derived d0) s
+
+実際に match を実行するには以下のようにする。
+
+    regex-match : (r : Regex   Σ) →  (List Σ) → Bool
+    regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
+
+ここではいくつかの問題が残っている。
+
+　　生成される状態は有限か? (つまり微分法は停止するのか)
+
+停止するかどうかに関係なく、regex-match は具体的な有限文字列に対して実行可能である。
+
+ただし、Agda では具体的ではない文字列も用意できる。
+
+    微分法で定義した Automaton は、正規表現でしていされた言語に一致するのか?
+
+これも証明する必要がある。
+
 --オートマトンから正規表現を生成する
 
 状態遷移の条件を正規表現した一般化オートマトンを考える。

--- a/a08/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a08/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -2,54 +2,204 @@
 
 任意のnについて 0{n}1{n} に対応する有限オートマトンはない。
 
-    inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
-    inputnn {zero} {_} _ _ s = s
-    inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )                     
+    inputnn0 : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ 
+    inputnn0 zero {_} _ _ s = s
+    inputnn0 (suc n) x y s = x  ∷ ( inputnn0 n x y ( y  ∷ s ) )
 
 inputnn だけ受け付けて、それ以外を受け付けないということができない。
 
+かっこの対応が取れないことに相当する。
+
+    inputnn :  List  In2 → Maybe (List In2)
+    inputnn [] = just []
+    inputnn  (i1 ∷ t) = just (i1 ∷ t)
+    inputnn  (i0 ∷ t) with inputnn t
+    ... | nothing = nothing
+    ... | just [] = nothing
+    ... | just (i0 ∷ t1) = nothing   -- can't happen
+    ... | just (i1 ∷ t1) = just t1   -- remove i1 from later part
+
+    inputnn1 :  List  In2 → Bool
+    inputnn1  s with inputnn  s 
+    ... | nothing = false
+    ... | just [] = true
+    ... | just _ = false
+
+こちらは  0{n}1{n} を受け付けるかどうか調べるプログラムである。
+
+inputnn1 が inpuynn0 を受けつけるかどうかを証明する必要がある。
+
+    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
+    nn01  = ?
+
+これはやさしくない。一般的にプログラムが正しく動くことを証明することに相当する。
+
+--pumping lemma
+
+まず Trace を定義する。
+
+    data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → Q → Set where
+        tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
+        tnext : (q : Q) → {i : Σ} { is : List Σ} 
+            → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 
+
+これは Automaton が受け付ける文字列を生成する data である。実際、
+
+    tr-accept→ : { Q : Set } { Σ : Set  }
+        → (fa : Automaton Q  Σ )
+        → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
+    tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
+    tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
+
+    tr-accept← : { Q : Set } { Σ : Set  }
+        → (fa : Automaton Q  Σ )
+        → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
+    tr-accept← {Q} {Σ} fa [] q ac = tend ac
+    tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
+    tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 
+
+もし、ある文字列を受け付ける Automaton の状態に重複があれば
 
 
-かっこの対応が取れないことに相当する。
+    record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
+        field
+           x y z : List Σ
+           xyz=is : x ++ y ++ z ≡ is 
+           trace-xyz  : Trace fa (x ++ y ++ z)  q
+           trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
+           non-nil-y : ¬ (y ≡ [])
 
+    pumping-lemma : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
+         → (tr : Trace fa is q )
+         → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
+         → TA fa q is
+
+を示すことができる。(Agda ではあんまりやさしくないが、割と自明)
+
+状態数よりも長い文字列を使えば、必ずこの方法で延長できる。 inputnn0 は、この性質を持たないので(なぜか?)
+inputnn0 が正規言語でないことがわかる。
 
 --push down automaton
 
+Automatonを拡張して、これを受け付けるようにすることができる。
 
     data PushDown   (  Γ : Set  ) : Set  where
        pop    : PushDown  Γ
        push   :  Γ → PushDown  Γ
+       none   :  PushDown  Γ
 
-    record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
+    record PDA ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
            : Set  where
         field
-            pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
-            pstart : Q
-            pz0 :  Γ
-        pmoves :  Q → List  Σ → ( Q × List  Γ )
-        pmoves q L = move q L [ pz0 ]
-               where
-                  move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × List  Γ )
-                  move q _ [] = ( q , [] )
-                  move q [] S = ( q , S )
-                  move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
-                  ... | (nq , pop )     = move nq T ST
-                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
-        paccept : List  Σ → Bool
-        paccept L = move pstart L [ pz0 ]
-               where
-                  move : (q : Q ) ( L : List  Σ ) ( L : List   Γ ) → Bool
-                  move q [] [] = true
-                  move q _ [] = false
-                  move q [] (_ ∷ _ ) = false
-                  move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
-                  ... | (nq , pop )     = move nq T ST
-                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+            automaton : Automaton Q Σ
+            pδ : Q →  PushDown  Γ 
+        open Automaton
+        paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
+        paccept q [] [] = aend automaton q 
+        paccept q (H  ∷ T) [] with pδ  (δ automaton q H) 
+        paccept q (H ∷ T) [] | pop     = paccept (δ automaton q H) T []
+        paccept q (H ∷ T) [] | none    = paccept (δ automaton q H) T []
+        paccept q (H ∷ T) [] | push x  = paccept (δ automaton q H) T (x  ∷ [] )
+        paccept q [] (_ ∷ _ ) = false
+        paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ (δ automaton q H) 
+        ... | pop      = paccept (δ automaton q H) T ST
+        ... | none     = paccept (δ automaton q H) T (SH ∷ ST)
+        ... | push ns  = paccept (δ automaton q H) T ( ns  ∷  SH ∷ ST )
+
+例えば
 
+    pnnp : PDA States2 In2 States2
+    pnnp = record {
+             automaton = record { aend = aend ; δ = δ }
+           ; pδ  = pδ
+       } where
+            δ : States2 → In2 → States2
+            δ ph1 i0 = ph1
+            δ ph1 i1 = ph2
+            δ ph2 i1 = ph2
+            δ _ _ = phf
+            aend : States2 → Bool
+            aend ph2 = true
+            aend _ = false
+            pδ  : States2 → PushDown States2
+            pδ ph1 = push ph1 
+            pδ ph2 = pop   
+            pδ phf = none   
+
+これと inputnn1 が同じ動作をすることを示せれば良い。
 
 --文脈自由文法
 
+PDA で受け付ける言語を文脈自由文法(context free grammer)という。
 
+実際のプログラミング言語は、型宣言とかの文脈に依存するので、CFGではない。
+
+しかし、文法自体は CFG で定義されることが多い。
+
+文法定義には BNF (Buckas Noar Form)を使う。ここでは Agda で以下のように定義する。
+
+    data Node (Symbol  : Set) : Set where
+        T : Symbol → Node Symbol 
+        N : Symbol → Node Symbol 
+
+    data Seq (Symbol  : Set) : Set where
+        _，_   :  Symbol  → Seq Symbol  → Seq Symbol 
+        _．    :  Symbol  → Seq Symbol 
+        Error    :  Seq Symbol 
+
+    data Body (Symbol  : Set) : Set where
+        _｜_   :  Seq Symbol  → Body Symbol  → Body Symbol 
+        _；    :  Seq Symbol  → Body Symbol 
+
+    record CFGGrammer  (Symbol  : Set) : Set where
+       field
+          cfg : Symbol → Body Symbol 
+          top : Symbol
+          eq? : Symbol → Symbol → Bool
+          typeof : Symbol →  Node Symbol
+
+これを split を使って言語として定義できる。
+
+    cfg-language0 :  {Symbol  : Set} → CFGGrammer Symbol   → Body Symbol  →  List Symbol → Bool
+
+    {-# TERMINATING #-}
+    cfg-language1 :  {Symbol  : Set} → CFGGrammer Symbol   → Seq Symbol  →  List Symbol → Bool
+    cfg-language1 cg Error x = false
+    cfg-language1 cg (S ， seq) x with typeof cg S
+    cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' /\ cfg-language1 cg seq t
+    cfg-language1 cg (_ ， seq) [] | T x = false
+    cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
+    cfg-language1 cg (S ．) x with typeof cg S
+    cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eq? cg x x'
+    cfg-language1 cg (_ ．) _ | T x = false
+    cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
+
+    cfg-language0 cg _ [] = false
+    cfg-language0 cg (rule ｜ b) x =
+         cfg-language1 cg rule x  \/ cfg-language0 cg b x  
+    cfg-language0 cg (rule ；) x = cfg-language1 cg rule x  
+
+    cfg-language :  {Symbol  : Set} → CFGGrammer Symbol   → List Symbol → Bool
+    cfg-language cg = cfg-language0 cg (cfg cg (top cg )) 
+
+これらを実際に parse するのには再帰下降法が便利なことが知られている。
+
+現在のコンパイラは。だいたいそれで実装されている。
+
+文法規則がプログラムで直接記述されるという利点もある。
+
+--文脈依存文法
+
+          cfg  : Symbol → Body Symbol 
+
+の部分を
+
+          cdg  : List Symbol → Body Symbol 
+
+とすると、文脈依存文法になる。これを判定して停止するプログラムは、stack を二つ持つ Automaton になるが、
+Turing Machine と呼ばれる。 その停止性を判定することはできない。それを次の講義で示す。
+
+実用的には文法規則の適当な subset を停止することが分かっているアルゴリズムで決めれば良い。
 
 ---問題8.1 push down automaton
 

--- a/a09/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a09/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -17,13 +17,14 @@
 
 Turing machineは状態と入力で、このコマンド二つを選択する。
 
-    record Turing ( Q : Set ) ( Σ : Set  ) 
+    record TM ( Q : Set ) ( Σ : Set  ) 
            : Set  where
         field
-            tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
-            tstart : Q
-            tend : Q → Bool
+            automaton : Automaton  Q Σ
+            tδ : Q → Σ → Write  Σ  ×  Move 
             tnone :  Σ
+        taccept : Q → List  Σ → ( Q × List  Σ × List  Σ )
+        taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L []
 
 書き込みと移動を二つのstack( List Σ)に対する関数として定義する。
 
@@ -87,22 +88,21 @@
     Copyδ H  _  = (H    , wnone   , mnone )
     Copyδ _  (suc (suc _))      = (H    , wnone       , mnone )
 
-    copyMachine : Turing CopyStates ℕ
-    copyMachine = record {
-            tδ = Copyδ
-         ;  tstart = s1
-         ;  tend = tend
+    copyTM : TM CopyStates ℕ
+    copyTM = record {
+            automaton = record { δ = λ q i → proj₁ (Copyδ q i) ; aend = tend }
+         ;  tδ = λ q i → proj₂ (Copyδ q i )
          ;  tnone =  0
       } where
           tend : CopyStates →  Bool
           tend H = true
           tend _ = false
 
-    test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
-    test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
+Automaton と違って入力文字列はテープ(stack)上に置かれている。
 
-    test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
-    test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
+終了状態に遷移すると計算は終了する。
+
+つまり入力と同時に計算が終了するとは限らない。
 
 
 -- Turing machine の停止問題
@@ -111,93 +111,50 @@
 
 文字列 x を判定する Turinging machine tm(x) があるとする。
 
+    record TM : Set where
+       field
+          tm : List Bool → Maybe Bool
+
 tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine
 
-   utm(tm , x)
+    record UTM : Set where
+       field
+          utm : TM
+          encode : TM → List Bool
+          is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x
 
-を構成することができる。utm(tm,x) は引数を二つ持つが、tm+x と結合した単一の文字列だと思えば単一引数になる。
+
+を構成することができる。utm は引数をtとxの二つ持つが、encode t ++ x  と結合した単一の文字列だと思えば単一引数になる。
+
 
 utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。
 
-  utm(tm,x) = 0  受け入れない
-             1  受け入れる
-             ⊥  止まらない
+             just true  受け入れない
+             ust false  受け入れる
+             nothing  止まらない
 
-utm の構成の詳細には立ち入らない。実際に utm を構成するのは良い演習になる。
+実際に utm を構成した例がある。
 
-tm に対応する文字列を tm とすると、tm 自体を tm の入力とすることができる。utm は、そのためだけに導入したので、もう使わない。
+<a href="../agda/utm.agda"> utm.agda </a>
+
+これには足りないものが結構ある。実際に utm は正しく動くのか? ( record UTM を構成できるのか?)
 
 --Turinng Machine の停止性の判定
 
 halt(tm,x) は、以下のように定義される。これはまだ、Turing machine であるとは限らない。
 
+    record Halt : Set where
+       field
+          halt :  (t : TM ) → (x : List Bool ) → Bool
+          is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
+          is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
+
+つまり、
+
   halt(tm,x) = 0  tm(x) が止まらない (halt が停止しない)    (1)
   halt(tm,x) = 1  tm(x) が止まる                            (2)
 
-halt(tm+x) 自体は ⊥ 、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?
-
---halt が tm ではあり得ないこの証明
-
-halt の否定を考えよう。
-
-  neg(tm) = 1  halt(tm,tm) が0                     (3)
-  neg(tm) = ⊥  halt(tm,tm) が1                     (4)
-
-つまり、halt(tm,tm) が1 の時、つまり、tm(tm) が停止する時には、neg(tm) は停止しない。neg 自体は halt があればtmとして簡単に作れる。
-
-  neg(neg) = 1
-
-かどうか調べよう。ここで 引数の neg は Turing machine neg を表す文字列である。
-
-まず、neg(neg) =1 と仮定する。(3) から、
-
-  halt(neg,neg) が 0
-
-なことがわかる。つまり、neg(neg) は停止しない。neg(neg) = ⊥ 。これは最初の仮定 neg(neg)=1に矛盾する。
-
-逆に、
-
-  neg(neg) = ⊥
-
-とすると、(4) から、
-
-  halt(neg,neg) = 1
-
-つまり、neg(neg) は止まる。つまり、neg(neg)=1。これも矛盾。
-
-つまり、halt(tm,x) が⊥にならないようなものは存在しない。
-
-つまり、Turinng machine が停止するかどうかを、必ず判定できる停止する Turing machine は存在しない。
-
---証明の考察
-
-ここで用いているのは、Turing machine の詳細ではなく、
-
-   Turing machine に対応する文字列 tm がある
-   tm を入力として用いることができる
-
-ということと、
-
-   tm が停止する、停止しない
-   tm が停止して、1から0
-
-を返すという性質である。
-
-    neg(neg) 
-
-は自分自身を参照しているので、自己参照と呼ばれる。
-
-halt は、neg が Turing machine になるためには、Turing machine である必要がある。
-
-tm(x) は停止するかしないかどちらかだから、halt(tm,x) という述語自体はある。
-
-しかし、halt(neg,neg) は 0 か 1 かを決めることはできない。
-
-これは述語を定義しても、それが0か1かを決めることができない場合があるということである。
-
-これは、述語論理の不完全性定理に対応する。
-
-この証明は自己参照を用いて矛盾を導く方法である。
+halt(tm+x) 自体は Bool  、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?
 
 --対角線論法
 
@@ -237,6 +194,8 @@
 
 これは、順に取ってくるという方法では、無限長の文字列は尽くせないということを意味する。可算回と呼ぶ。
 
+
+
 --2^N
 
 この無限長の文字列は、自然数Nから{0,1} の写像と考えられる。あるいは、自然数Nの部分集合に1、それ以外に0を割り振ったものである。これを 2^N と書く。
@@ -250,53 +209,157 @@
 
 また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。
 
---対角線論法と Turing machine の対応
+-- Agda による対角線論法
 
-halt(tm,x) は、文字列 tm+x から、{0,1 } への写像を与える。文字列は、bit pattern と考えると、巨大な自然数となる。 tm であれば、文字列表現を持つ。
+    record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+       field
+           fun←  :  S → R
+           fun→  :  R → S
+           fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
+
+fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x  もあるのだが、ここでは使わない。
+
+    diag : {S : Set }  (b : HBijection  ( S → Bool ) S) → S → Bool
+    diag b n = not (fun← b n n)
+
+これで対角線部分の否定を采関数を定義する。
 
-つまり、halt は 入力 x に対して Turing machine を、その表現の自然数順に並べた時に、止まるものを1、そうでないものを0とする文字列を与える。
+    diagonal : { S : Set } → ¬ HBijection  ( S → Bool ) S
+    diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
+        diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
+        diagn1 n dn = ¬t=f (diag b n ) ( begin
+               not (diag b n)
+            ≡⟨⟩
+               not (not fun← b n n)
+            ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
+               not (fun← b (fun→ b (diag b))  n)
+            ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
+               not (fun← b n n)
+            ≡⟨⟩
+               diag b n 
+            ∎ ) where open ≡-Reasoning
 
-入力 x も文字列なので、halt(tm,x) は二次元の0,1のパターンになる。横軸が tm で、縦軸が x として、
+それに対して、HBijection  ( S → Bool ) S があるとすると、
+
+        not (diag b n) ≡ diag b n
 
-    00000000000000000000000000100000....
-    01000000000000000000000000001000....
-    01100000000000000000000000000100....
-    01110000000000000000000000000010....
-    01111000000000000000000000000000....
-    01111100000000000000000000000000....
-    01011100000000000000000000000000....
-            ...
-            ...
-            ...
+となっている。証明の各段階を追ってみよ。
+
+
+--halt が tm ではあり得ないこの証明
+
+halt の否定を考えよう。
+
+  neg(tm) = 1  halt(tm,tm) が0                     (3)
+  neg(tm) = ⊥  halt(tm,tm) が1                     (4)
+
+つまり、halt(tm,tm) が1 の時、つまり、tm(tm) が停止する時には、neg(tm) は停止しない。neg 自体は halt があればtmとして簡単に作れる。
+
+  neg(neg) = 1
+
+かどうか調べよう。ここで 引数の neg は Turing machine neg を表す文字列である。
+
+まず、neg(neg) =1 と仮定する。(3) から、
+
+  halt(neg,neg) が 0
+
+なことがわかる。つまり、neg(neg) は停止しない。neg(neg) = ⊥ 。これは最初の仮定 neg(neg)=1に矛盾する。
+
+逆に、
+
+  neg(neg) = ⊥
+
+とすると、(4) から、
+
+  halt(neg,neg) = 1
+
+つまり、neg(neg) は止まる。つまり、neg(neg)=1。これも矛盾。
+
+つまり、halt(tm,x) が⊥にならないようなものは存在しない。
+
+つまり、Turinng machine が停止するかどうかを、必ず判定できる停止する Turing machine は存在しない。
 
-この文字列の表が halt(tm,x) を決めている。特性関数などと呼ばれる。
+-- Agda での構成
+
+Halt は languageなので、存在すれば UTM で simulation できることに注意しよう。
+
+Halt と UTM から HBijection (List Bool → Bool) (List Bool) を示す。
 
-halt(x,x) は対角線要素になる。その否定を考えよう。
+    TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
+
+すると、
+
+    TNL1 : UTM → ¬ Halt 
+    TNL1 utm halt = diagonal ( TNL halt utm )
 
-  not(tm) = 1  halt(tm,tm) が0                     (5)
-  not(tm) = 0  halt(tm,tm) が1                     (6)
+となる。TNL は以下のように構成する。
+
+    λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
+
+は (List Bool → Bool) →  List Bool になっている。
 
-not(x) は、haltを入力順にした表の対角線要素を反転したものになる。(前の neg とは少し異なる)
-この文字列は、x 番目の入力文字列に対するnot(x)の値を示している。
+     h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
+     h1 h x with h x
+     ... | true =  just true
+     ... | false = nothing 
+     λ h  → encode utm record { tm = h1 h }
+
+は、List Bool → (List Bool → Bool である。
+
+これから、fiso←  を導けば良い。
 
-対角線論法から、not(x) の文字列は、haltを特徴付ける可算個のパターンに含まれてない。
-
-もし、halt(tm,x) の x に not(x) が含まれていれば、同じパターンが出てくるはずである。
-つまり、not(x) は、halt(tm,x) が判定できる範囲に含まれてないことがわかる。
+    TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
+    TNL halt utm = record {
+           fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
+         ; fun→  = λ h  → encode utm record { tm = h1 h } 
+         ; fiso← = λ h →  f-extensionality (λ y → TN1 h y )
+      } where
+         open ≡-Reasoning
+         h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
+         h1 h x with h x
+         ... | true =  just true
+         ... | false = nothing
+         tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool
+         tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y
+         h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing
+         h-nothing h y eq with h y
+         h-nothing h y refl | false = refl
+         h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
+         h-just h y eq with h y
+         h-just h y refl | true = refl
+         TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
+         TN1 h y with h y | inspect h y
+         ... | true  | record { eq = eq1 } = begin
+            Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
+            true ∎  where
+              tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ just true
+              tm-tenc = begin
+                  tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
+                  h1 h y ≡⟨ h-just h y eq1  ⟩
+                  just true  ∎  
+         ... | false | record { eq = eq1 } = begin
+            Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
+            false ∎  where
+              tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ nothing
+              tm-tenc = begin
+                  tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
+                  h1 h y ≡⟨  h-nothing h y eq1 ⟩
+                  nothing  ∎  
+         -- the rest of bijection means encoding is unique
+         -- fiso→ :  (y : List Bool ) → encode utm record { tm = λ x →  h1 (λ tm → Halt.halt halt (UTM.utm utm) tm  ) x } ≡ y
 
---対角線論法に対する考察
-
-tm(x) を実行して停止すれば、それは判定できる。しかし、停止しないかどうかはわからない。実際に、わからない tm を構成することはできて、それが not(x) である。
-
-neg(neg) の議論は ⊥ を使っていたが、not(x) では、halt(tm,x) の特徴関数の入力に not(x) が含まれるかどうかに変わっている。
+f-extensionality は関数の入出力がすべて一致すれば関数自体が等しいという仮定である。これは Agda では証明できない。
 
 Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。
 
+HBijection を使わずに diag1 を直接つかって証明することもできる。この場合は halt が UTM で simulation できること
+から矛盾がでる。
+
 --さまざまな決定不能問題
 
 多くの問題は Turing machine の停止性に帰着できる。
 
     ディオファントス方程式
-    文脈依存文法
+    文脈依存文法の判定
     Automaton を含む方程式
 

--- a/a10/lecture.ind	Sat Jan 15 01:12:43 2022 +0900
+++ b/a10/lecture.ind	Fri Jan 21 10:45:42 2022 +0900
@@ -27,6 +27,20 @@
 
 実際には係数も問題になることが多い。
 
+
+--o(n)
+
+--o(n^2)
+
+    naive append
+
+--o(n*log n)
+
+    quick sort
+
+--o(exp n)
+
+
 --P
 
 Turing machine で多項式時間がかかる計算量。
@@ -66,8 +80,14 @@
 
 --NPの例
 
+Boolean formula の satifiberbilty を調べる
+
    SAT 
 
+--coNPの例
+
+Boolean formula の validity を調べる
+
 --P=NP?
 
 NP はあまりに強力だが、EXP(指数的な計算量)では押さえられる。
@@ -82,16 +102,10 @@
 
 量化記号を含むSAT。
 
---o(n)
-
---o(n^2)
-
-    naive append
+--計算量の階層
 
---o(n*log n)
+どこの隙間も空でないことは証明されていない。
 
-    quick sort
-
---o(exp n)
+<center><img src="fig/comp-hier.svg"></center>
 
 

--- a/automaton-in-agda/src/logic.agda	Sat Jan 15 01:12:43 2022 +0900
+++ b/automaton-in-agda/src/logic.agda	Fri Jan 21 10:45:42 2022 +0900
@@ -74,6 +74,10 @@
 
 open import Relation.Binary.PropositionalEquality
 
+not-not-bool : { b : Bool } → not (not b) ≡ b
+not-not-bool {true} = refl
+not-not-bool {false} = refl
+
 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
    field
        fun←  :  S → R

--- a/automaton-in-agda/src/omega-automaton.agda	Sat Jan 15 01:12:43 2022 +0900
+++ b/automaton-in-agda/src/omega-automaton.agda	Fri Jan 21 10:45:42 2022 +0900
@@ -14,9 +14,9 @@
 
 open Automaton 
 
-ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) →  ℕ → ( ℕ → Σ )  → Q
-ω-run Ω x zero s = x
-ω-run Ω x (suc n) s = δ Ω (ω-run Ω x n s) ( s n )
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → Q →  ( ℕ → Σ )  → ( ℕ → Q )
+ω-run Ω x s zero = x
+ω-run Ω x  s (suc n) = δ Ω (ω-run Ω x s n) ( s n )
 
 --
 -- accept as Buchi automaton
@@ -24,7 +24,7 @@
 record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         from : ℕ
-        stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x n S ) ≡ true
+        stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true
 
 open Buchi
 
@@ -36,15 +36,15 @@
 --                   <-----------
 --                       p
 
-    
 --
 -- accept as Muller automaton
 --
 record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
-        infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x (n + (next n)) S ) ≡ true 
+        infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x  S (n + (suc (next n)))) ≡ true 
 
+open  Muller 
 --  always sometimes p
 --
 --                       not p
@@ -53,6 +53,46 @@
 --                   <-----------
 --                       p
 
+open import nat
+open import Data.Nat.Properties
+
+LEMB : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S ∨ (¬ ( Buchi Ω S ))
+LEMB = {!!}
+
+LEMM : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S ∨ (¬ ( Muller Ω S ))
+LEMM = {!!}
+
+B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+B→M {Q} {Σ} Ω S q b m = ¬t=f (aend Ω ( ω-run Ω bm00 S (from b + suc ( next m (from b ) ))))  {!!} where
+   bm00 : Q
+   bm00 = ω-run Ω q S (from b + suc (Muller.next m (from b)))
+   bm02 :  aend Ω (ω-run Ω bm00 S (from b + suc (next m (from b) ))) ≡ true
+   bm02 = stay b bm00 (from b + suc (next m (from b) )) {!!}
+   Ω' : Automaton Q Σ
+   Ω' = record { δ = δ Ω ; aend = λ q → not (aend Ω q) }
+   bm03 : aend  Ω' (ω-run  Ω' bm00 S (from b + suc (next m (from b) ))) ≡ true
+   bm03 = infinite m bm00  (from b)
+   bm05 : (q : Q) → (n : ℕ) → ω-run  Ω' q S n ≡ ω-run  Ω q S n
+   bm05 q zero = refl
+   bm05 q (suc n) = begin
+    ω-run  Ω' q S (suc n) ≡⟨⟩
+    δ Ω (ω-run Ω' q S n) (S n) ≡⟨ cong (λ k → δ Ω  k (S n) ) (bm05 q n) ⟩
+    δ Ω (ω-run Ω q S n) (S n) ≡⟨⟩
+    ω-run Ω q S (suc n) ∎ where open ≡-Reasoning
+   bm04 : (q : Q) → (n : ℕ) → aend  Ω' (ω-run  Ω' q S n) ≡ not aend  Ω (ω-run  Ω q S n) 
+   bm04 q zero = refl
+   bm04 q (suc n) = begin
+     aend Ω' (ω-run Ω' q S (suc n)) ≡⟨⟩
+     not aend Ω (δ Ω (ω-run Ω' q S n) (S n)) ≡⟨ cong (λ k → not aend Ω ( δ Ω k (S n))) (bm05 q n) ⟩
+     not aend Ω (δ Ω (ω-run Ω q S n) (S n)) ≡⟨⟩
+     not aend Ω (ω-run Ω q S (suc n)) ∎ where open ≡-Reasoning
+   bm01 :  (not aend Ω (ω-run Ω bm00 S (Muller.next m (from b) + from b))) ≡ aend Ω (ω-run Ω bm00 S (Muller.next m (from b) + from b))
+   bm01 = {!!}
+
+M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
+M→B = {!!}
+
+
 data  States3   : Set  where
    ts* : States3
    ts  : States3
@@ -83,26 +123,22 @@
 flip-seq zero = false
 flip-seq (suc n) = not ( flip-seq n )
 
-lemma0 : Muller ωa1 flip-seq 
-lemma0 = record {
-        next = λ n → suc (suc n)
-      ; infinite = lemma01
-   } where
-        lemma01 :  (x : States3) (n : ℕ) →
-           aend ωa1 (ω-run ωa1 x (n + suc (suc n)) flip-seq) ≡ true
-        lemma01 = {!!}
+-- flip-seq is acceepted by Muller automaton ωa1 
 
 lemma1 : Buchi ωa1 true-seq 
 lemma1 = record {
         from = zero
       ; stay = {!!}
    } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} n true-seq ) ≡ true
+      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} true-seq n ) ≡ true
       lem1 zero ()
-      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} n true-seq 
+      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} true-seq n
       lem1 (suc n) (s≤s z≤n) | ts* = {!!}
       lem1 (suc n) (s≤s z≤n) | ts = {!!}
 
+lemma0 : Muller ωa1 flip-seq 
+lemma0 = {!!}
+
 ωa2 : Automaton States3 Bool
 ωa2 = record {
         δ = transition3
@@ -131,15 +167,15 @@
 
 lemma2 : Muller ωa2 flip-seq 
 lemma2 = record {
-          next = next
+          next = next1
        ;  infinite = {!!}
    }  where
-     next : ℕ → ℕ
-     next = {!!}
+     next1 : ℕ → ℕ
+     next1 = {!!}
      infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
      infinite' = {!!}
-     infinite : (n : ℕ) → aend ωa2 {!!} ≡ true
-     infinite = {!!}
+     infinite2 : (n : ℕ) → aend ωa2 {!!} ≡ true
+     infinite2 = {!!}
 
 lemma3 : Buchi ωa1 false-seq  →  ⊥
 lemma3 = {!!}
@@ -148,8 +184,47 @@
 lemma4 = {!!}
 
 
+data LTTL ( V : Set )  : Set where
+    s :  V → LTTL V
+    ○ :  LTTL V → LTTL V
+    □ :  LTTL V → LTTL V
+    ⋄ :  LTTL V → LTTL V
+    _U_  :  LTTL V → LTTL  V → LTTL  V
+    t-not :  LTTL V → LTTL  V
+    _t\/_ :  LTTL V → LTTL  V → LTTL  V
+    _t/\_ :  LTTL V → LTTL  V → LTTL  V
 
-
+{-# TERMINATING #-}
+M1 : { V : Set } → (ℕ → V → Bool) → ℕ →  LTTL V  → Set
+M1 σ i (s x) = σ i x ≡ true
+M1 σ i (○ x) = M1 σ (suc i) x  
+M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1  σ j p
+M1 σ i (⋄ p) = ¬ ( M1 σ i (t-not p) )
+M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
+M1 σ i (t-not p) = ¬ ( M1 σ i p )
+M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ 
+M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁ 
 
+data LITL ( V : Set )  : Set where
+    iv :  V → LITL V
+    i○ :  LITL V → LITL V
+    _&_  :  LITL V → LITL  V → LITL  V
+    i-not :  LITL V → LITL  V
+    _i\/_ :  LITL V → LITL  V → LITL  V
+    _i/\_ :  LITL V → LITL  V → LITL  V
 
+open import Relation.Binary.Definitions
+open import Data.Unit using ( tt ; ⊤ )
 
+{-# TERMINATING #-}
+MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j  →  LITL V  → Set
+MI σ i j lt (iv x) = σ i x ≡ true
+MI σ i j lt (i○ x) with <-cmp i j
+... | tri< a ¬b ¬c = MI σ (suc i) j {!!} x
+... | tri≈ ¬a b ¬c = ⊤
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
+MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p))
+MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p )
+MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁ 
+MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁ 
+

--- a/automaton-in-agda/src/prime.agda	Sat Jan 15 01:12:43 2022 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jan 21 10:45:42 2022 +0900
@@ -106,6 +106,7 @@
 factorial : (n : ℕ) → ℕ
 factorial zero = 1
 factorial (suc n) = (suc n) * (factorial n)
+
 factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
 factorial-mono n = begin
      factorial n  ≤⟨ x≤x+y ⟩