-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 TM ( Q : Set ) ( Σ : Set  ) 
           : Set  where
        field
            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 Σ)に対する関数として定義する。

    {-# 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 )

    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

Automaton と違って入力文字列はテープ(stack)上に置かれている。

終了状態に遷移すると計算は終了する。

つまり入力と同時に計算が終了するとは限らない。


-- Turing machine の停止問題

---Universal Turing Machine

文字列 x を判定する Turinging machine tm(x) があるとする。

    record TM : Set where
       field
          tm : List Bool → Maybe Bool

tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine

    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 は引数をtとxの二つ持つが、encode t ++ x  と結合した単一の文字列だと思えば単一引数になる。


utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。

             just true  受け入れない
             ust false  受け入れる
             nothing  止まらない

実際に 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) 自体は Bool  、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?

--対角線論法

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 の実数を表す。実数の集合は可算集合でないことがわかる。

また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。

-- Agda による対角線論法

    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)

これで対角線部分の否定を采関数を定義する。

    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

それに対して、HBijection  ( S → Bool ) S があるとすると、

        not (diag b n) ≡ diag b n

となっている。証明の各段階を追ってみよ。


--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 は存在しない。

-- Agda での構成

Halt は languageなので、存在すれば UTM で simulation できることに注意しよう。

Halt と UTM から HBijection (List Bool → Bool) (List Bool) を示す。

    TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)

すると、

    TNL1 : UTM → ¬ Halt 
    TNL1 utm halt = diagonal ( TNL halt utm )

となる。TNL は以下のように構成する。

    λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)

は (List Bool → Bool) →  List Bool になっている。

     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←  を導けば良い。

    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

f-extensionality は関数の入出力がすべて一致すれば関数自体が等しいという仮定である。これは Agda では証明できない。

Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。

HBijection を使わずに diag1 を直接つかって証明することもできる。この場合は halt が UTM で simulation できること
から矛盾がでる。

--さまざまな決定不能問題

多くの問題は Turing machine の停止性に帰着できる。

    ディオファントス方程式
    文脈依存文法の判定
    Automaton を含む方程式