--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a09/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,302 @@
+-title: Turing Machine
+
+Turing Machine は無限長のテープを持つAutomatonである。これは、stack を二つ持つ Automaton として構成できる。
+
+<a href="../agda/turing.agda"> turing.agda </a>
+
+テープへの操作は、書き込みと移動である。
+
+    data Write   (  Σ : Set  ) : Set  where
+       write   : Σ → Write  Σ
+       wnone   : Write  Σ
+
+    data Move : Set  where
+       left   : Move  
+       right  : Move  
+       mnone  : Move  
+
+Turing machineは状態と入力で、このコマンド二つを選択する。
+
+    record Turing ( Q : Set ) ( Σ : Set  ) 
+           : Set  where
+        field
+            tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
+            tstart : Q
+            tend : Q → Bool
+            tnone :  Σ
+
+書き込みと移動を二つのstack( List Σ)に対する関数として定義する。
+
+    {-# TERMINATING #-}
+    move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move q L [] = move q  L  ( tnone  ∷ [] ) 
+    move q [] R = move q  ( tnone  ∷ [] )  R 
+    move q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
+    ... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
+    ... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
+    ... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
+    ... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
+    ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
+    ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
+    {-# TERMINATING #-}
+    move-loop : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move-loop  q L R with tend q
+    ... | true = ( q , L , R )
+    ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+      where
+        next = move  q  L  R 
+    {-# TERMINATING #-}
+    move0 : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move0  q L R with tend q
+    ... | true = ( q , L , R )
+    move0 q L [] | false = move0 q  L  ( tnone  ∷ [] ) 
+    move0 q [] R | false = move0 q  ( tnone  ∷ [] )  R 
+    move0 q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
+    ... | nq , write x , left  = move0 nq ( RH ∷ x  ∷ LT ) RT 
+    ... | nq , write x , right = move0 nq LT ( x  ∷ RH  ∷ RT ) 
+    ... | nq , write x , mnone = move0 nq ( x  ∷ LT ) (  RH ∷ RT ) 
+    ... | nq , wnone , left    = move0 nq ( RH  ∷ LH  ∷ LT ) RT  
+    ... | nq , wnone , right   = move0 nq  LT ( LH  ∷ RH  ∷ RT ) 
+    ... | nq , wnone , mnone   = move0 nq ( LH  ∷ LT ) (  RH ∷ RT )  
+    {-# TERMINATING #-}
+    taccept : List  Σ → ( Q × List  Σ × List  Σ )
+    taccept L = move0 tstart L []
+
+--Turing Machine の例題
+
+    data CopyStates : Set where
+       s1 : CopyStates
+       s2 : CopyStates
+       s3 : CopyStates
+       s4 : CopyStates
+       s5 : CopyStates
+       H  : CopyStates
+
+
+    Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move 
+    Copyδ s1 0  = (H    , wnone       , mnone )
+    Copyδ s1 1  = (s2   , write 0 , right )
+    Copyδ s2 0  = (s3   , write 0 , right )
+    Copyδ s2 1  = (s2   , write 1 , right )
+    Copyδ s3 0  = (s4   , write 1 , left )
+    Copyδ s3 1  = (s3   , write 1 , right )
+    Copyδ s4 0  = (s5   , write 0 , left )
+    Copyδ s4 1  = (s4   , write 1 , left )
+    Copyδ s5 0  = (s1   , write 1 , right )
+    Copyδ s5 1  = (s5   , write 1 , left )
+    Copyδ H  _  = (H    , wnone   , mnone )
+    Copyδ _  (suc (suc _))      = (H    , wnone       , mnone )
+
+    copyMachine : Turing CopyStates ℕ
+    copyMachine = record {
+            tδ = Copyδ
+         ;  tstart = s1
+         ;  tend = tend
+         ;  tnone =  0
+      } where
+          tend : CopyStates →  Bool
+          tend H = true
+          tend _ = false
+
+    test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
+    test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
+
+    test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
+    test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
+
+
+-- Turing machine の停止問題
+
+---Universal Turing Machine
+
+文字列 x を判定する Turinging machine tm(x) があるとする。
+
+tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine
+
+   utm(tm , x)
+
+を構成することができる。utm(tm,x) は引数を二つ持つが、tm+x と結合した単一の文字列だと思えば単一引数になる。
+
+utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。
+
+  utm(tm,x) = 0  受け入れない
+             1  受け入れる
+             ⊥  止まらない
+
+utm の構成の詳細には立ち入らない。実際に utm を構成するのは良い演習になる。
+
+tm に対応する文字列を tm とすると、tm 自体を tm の入力とすることができる。utm は、そのためだけに導入したので、もう使わない。
+
+--Turinng Machine の停止性の判定
+
+halt(tm,x) は、以下のように定義される。これはまだ、Turing machine であるとは限らない。
+
+  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かを決めることができない場合があるということである。
+
+これは、述語論理の不完全性定理に対応する。
+
+この証明は自己参照を用いて矛盾を導く方法である。
+
+--対角線論法
+
+0,1 からなる無限長の文字列を考えよう。これを順に拾っていく。どんな順序で拾っても、自然数の範囲では拾い切れないことをしまそう。
+
+拾った順に、文字列を並べる。
+
+    00000000000000000000000000100000....
+    01000000000000000000000000001000....
+    01100000000000000000000000000100....
+    01110000000000000000000000000010....
+    01111000000000000000000000000000....
+    01111100000000000000000000000000....
+    01011100000000000000000000000000....
+            ...
+            ...
+            ...
+
+行y列xの文字を v(x,y) とする。これは 0 か 1 である。上の文字列の対角線の要素は v(x,x) となる。以下の . が対角線要素になる。
+
+    .0000000000000000000000000100000....
+    0.000000000000000000000000001000....
+    01.00000000000000000000000000100....
+    011.0000000000000000000000000010....
+    0111.000000000000000000000000000....
+    01111.00000000000000000000000000....
+    010111.0000000000000000000000000....
+            ...
+            ...
+            ...
+
+1-v(x,x) を考えると、
+
+    1000001 ...
+
+となる。この文字列は、最初に拾った文字列のどれとも、v(x,x)のところで異なる。つまり拾った文字列とは異なる文字列が必ず存在する。
+
+これは、順に取ってくるという方法では、無限長の文字列は尽くせないということを意味する。可算回と呼ぶ。
+
+--2^N
+
+この無限長の文字列は、自然数Nから{0,1} の写像と考えられる。あるいは、自然数Nの部分集合に1、それ以外に0を割り振ったものである。これを 2^N と書く。
+
+    自然数の部分集合全体
+    自然数から{0,1}への写像の全体
+
+である。自然数に1対1対応する集合を可算集合という。これらの集合は可算集合ではないことが対角線論法からわかる。
+
+この文字列の先頭に 0. を付けると、0から1 の実数を表す。実数の集合は可算集合でないことがわかる。
+
+また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。
+
+--対角線論法と Turing machine の対応
+
+halt(tm,x) は、文字列 tm+x から、{0,1 } への写像を与える。文字列は、bit pattern と考えると、巨大な自然数となる。 tm であれば、文字列表現を持つ。
+
+つまり、halt は 入力 x に対して Turing machine を、その表現の自然数順に並べた時に、止まるものを1、そうでないものを0とする文字列を与える。
+
+入力 x も文字列なので、halt(tm,x) は二次元の0,1のパターンになる。横軸が tm で、縦軸が x として、
+
+    00000000000000000000000000100000....
+    01000000000000000000000000001000....
+    01100000000000000000000000000100....
+    01110000000000000000000000000010....
+    01111000000000000000000000000000....
+    01111100000000000000000000000000....
+    01011100000000000000000000000000....
+            ...
+            ...
+            ...
+
+この文字列の表が halt(tm,x) を決めている。特性関数などと呼ばれる。
+
+halt(x,x) は対角線要素になる。その否定を考えよう。
+
+  not(tm) = 1  halt(tm,tm) が0                     (5)
+  not(tm) = 0  halt(tm,tm) が1                     (6)
+
+not(x) は、haltを入力順にした表の対角線要素を反転したものになる。(前の neg とは少し異なる)
+この文字列は、x 番目の入力文字列に対するnot(x)の値を示している。
+
+対角線論法から、not(x) の文字列は、haltを特徴付ける可算個のパターンに含まれてない。
+
+もし、halt(tm,x) の x に not(x) が含まれていれば、同じパターンが出てくるはずである。
+つまり、not(x) は、halt(tm,x) が判定できる範囲に含まれてないことがわかる。
+
+--対角線論法に対する考察
+
+tm(x) を実行して停止すれば、それは判定できる。しかし、停止しないかどうかはわからない。実際に、わからない tm を構成することはできて、それが not(x) である。
+
+neg(neg) の議論は ⊥ を使っていたが、not(x) では、halt(tm,x) の特徴関数の入力に not(x) が含まれるかどうかに変わっている。
+
+Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。
+
+--さまざまな決定不能問題
+
+多くの問題は Turing machine の停止性に帰着できる。
+
+    ディオファントス方程式
+    文脈依存文法
+    Automaton を含む方程式
+