Turing Machine
MenuTuring Machine は無限長のテープを持つAutomatonである。これは、stack を二つ持つ Automaton として構成できる。
turing.agda テープへの操作は、書き込みと移動である。
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 を構成した例がある。
utm.agda これには足りないものが結構ある。実際に 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 を含む方程式