--- 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 を含む方程式