「Postの対応問題」の決定丌能性の証明
k.inaba
http://www.kmonos.net/2009/10/10 第１回決定丌能の会

Postの対応問題(PCP : Post’s Correspondence Problem)• 入力– Σ : 文字集合 （有限）– {(α1, β1), …, (αn, βn)} :Σ上の有限文字列のペアの有限集合• 出力– 有限列 i1, …, ik で•αi1 … αik ＝ βi1 … βikになるものは存在するか 否か？

例１
• 入力
– (α1, β1 ) = (“e”,“abcde”)– (α2, β2 ) = (“ababc”, “ab” )– (α3, β3 ) = (“d”,“cab” )• 出力– Yes!
α 2 α2 α3 α1 = β 2 β2 β3 β1– ababcababcde– ababcababcde

例２
• 入力
– (α1, β1 ) = (“ab”, “ca” )– (α2, β2 ) = (“acb”, “a”)
– (α3, β3 ) = (“b”,“caab” )• 出力– No!
• 一つ目のペアとしては α2 , β2 をとるしかないが、“cb” がβ側にないので作れない一般にはYesかNoか決定丌可能• 参考にした資料– An Introduction to the Theory of Computation• Eitan Gurari, Ohio State University• Computer Science Press, 1989,
ISBN 0-7167-8182-4• http://www.cse.ohio-state.edu/~gurari/theorybk/theory-bk.html– 4.7 節証明

方針
• 主参考文献では 0型文法でやっていたけど面倒なのでこれで。実質ほぼ同じ– 「チューリングマシンの停止問題」 から…
• TMの停止問題は決定丌能– 「Semi-Thue System のワード問題」 経由で…
• どんなTM停止問題も、答えがそれと一致するSTSワード問題に変換できる ∴STSワード問題は決定丌能

– PCP に帰着
• どんなSTSワード問題も、答えがそれと一致するPCPに変換できる ∴PCPは決定丌能Semi-Thue System (STS) とは• G = (Δ, P )– Δ : 文字集合 (有限)– P : 以下の形の文法規則の有限集合• α→β(α , β ∈ Δ+)• Δ+ 上の二項関係 w ⇒ v– w = x0 y1 x1 … yn xn,– ∀i. yi→zi ∈Pを以下で定義

v = x0 z1 x1 … zn xn

STSのワード問題とは？
• 入力– G = (Δ, P) : Semi-Thue System– ws : Δ上の(有限長の)文字列– wf : Δ上の(有限長の)文字列• 出力– ws から ⇒ を有限回繰り返して wf に書き換えられるなら “Yes”、できないなら “No”

STSのワード問題：例• G– Δ= {a, b}– P = {aa→ab, bb→bbb}• ws = “aab”, wf = “abbbbbbb”– Yes! (“aab”⇒”abb”⇒…中略… ⇒”abbbbbbb”)• ws = “bab”, wf = “aabaa”– No! (Pにbの数が増える規則しかないので絶対無理)

STSのワード問題は決定丌能 (1/2)• 「チューリングマシンの停止問題」
からの帰着–チューリングマシンの 「状態 q でテープの文字が 0 だったらテープに 1を書いて左に動き状態 p になる」 といった規則を•0q0 → p01と1q0 →p11のようにSemi-Thue Systemの規則にエンコードできるSTSのワード問題は決定丌能 (2/2)• 「チューリングマシンの停止問題」
からの帰着–チューリングマシンの受理状態を f とし、•0f→f と 1f→f と f0→0 と f1→1という規則をさらに付け加えて、テープ端に関する規則を幾つか追加すると、「TMが停止する iff “初期状態”⇒*“f”」 となる
QED

話を戻してPCPの決定丌能性• 不えられたSTSワード問題 (G,ws,wf) から
STSワード問題の解が”Yes”
if and only if
PCPの解が”Yes”になるようなPCPを作れる

具体的な作り方 （ちょっと間違ってる）• STSメンバシップ問題のインスタンス– G = (Δ, P )ws , wf ∈ Δ +• 対応する PCP のインスタンス– Σ = {始, 終, 次} ∪ Δ– (始,始次ws )– (次wf終,終)– ( x, x )for all x ∈ {次}∪Δ– ( α, β )for all α→β ∈ P

作り方の例 （左: STS、右: PCP）
• Δ= {a, b}•• P = {aa→ab, bb→bbb}• ws = “aab”• wf = “abb”• Σ={始, 次, 終, a, b}• (始,始次aab )• (次abbb終, 終)• ( a, a )• ( b, b )• ( 次, 次 )• ( aa, ab )• ( bb, bbb )作り方の例：
PCPの方を解いてみる• (始,始次aab ) でスタート

始始次aab(始,始次aab )(次abbb終, 終)( a, a )( b, b )( 次, 次 )( aa, ab )( bb, bbb )• つぎは、上側に次 が来ないといけない

始次
始次aab次作り方の例：
PCPの方を解いてみる• (aa, ab) を使ってみる

始次aa
始次aab次ab• つぎは、(b, b) しかない

始次aab
始次aab次abb(始,始次aab )(次abbb終, 終)( a, a )( b, b )( 次, 次 )( aa, ab )( bb, bbb )作り方の例：
PCPの方を解いてみる• （中略）

始次aab次abb
始次aab次abb次abbb• 最後は 終 ペア

始次aab次abb次abbb終始次aab次abb次abbb終(始,始次aab )(次abbb終, 終)( a, a )( b, b )( 次, 次 )( aa, ab )( bb, bbb )作り方の例：
PCPの方を解いてみる• PCPの解は”Yes”

始次aab次abb次abbb終始次aab次abb次abbb終(始,始次aab )(次abbb終, 終)( a, a )( b, b )( 次, 次 )( aa, ab )( bb, bbb )• STSの解は？ “Yes”“次”で区切られた部分に着目すると…
– ws = aab ⇒ abb ⇒ abbb = wf

• フォーマルに言うと、次ページの補題が成り立つ

補題• ws =γ0 ⇒γ1 ⇒ … ⇒ γm = wfという書き換え列がSTSにある
if and only if• 始次γ0 次γ1次γ2次 … 次γm 終で一致するようなマッチングがPCPにある

補題の証明帰納法で m≧0 に関して以下を示す• γ 0 ⇒ γ 1 ⇒ … ⇒ γ m = wf
if and only if• ∃i1 … inxi1…x1n =次γ0 次γ1次 … 次γm 終
yi1…yi n =次γ1次 … 次γm 終（γ0 = ws の場合を考えれば補題がすぐ従う）

補題の証明• γ0⇒γ1⇒…⇒γm = wf
if and only if• ∃i1 … in

(始,(次wf終,( x, x )( α, β )始次ws )終)for all x ∈ {次}∪Δfor all α→β ∈ P

xi1…x1n =次γ0 次γ1次 … 次γm 終
yi1…yi n =次γ1次 … 次γm 終• m = 0 の場合– (次 wf 終, 終) がPCPのペアにあるので成立

補題の証明• γ0⇒γ1⇒…⇒γm = w• ∃i1 … inxi1…x1nyi1…yi n(次w終,終)( x, x )for all x ∈ {次}∪Δ(α , β)for all α→β ∈ P=次γ0 次γ1次 … 次γm 終=
次γ1次 … 次γm 終• m ＞ 0 の場合(“only if” part)– γ0 ⇒ γ1 ⇒ … ⇒ γm = w– implies γ0 ⇒γ1 かつ γ1 ⇒ … ⇒ γm = w– by IH 次γ1 次γ2次 … 次γm 終と次γ2次 … 次γm 終 がマッチ
– γ0 ⇒γ1 なので 次γ0 と次γ1もマッチ [要証明]– よって、合わせると全体もマッチ

補題の証明• γ0 ⇒γ1 ⇒… ⇒γm = w• ∃i1 … inxi1…x1nyi1…yi n=次γ0 次γ1次 … 次γm 終=次γ1次 … 次γm 終• m ＞ 0 の場合–(次w終,終)( x, x )for all x ∈ {次}∪Δ(α , β)for all α→β ∈ P(“if” part)次γ0 次γ1次γ2次… 次γm 終と次γ1次γ2 次… 次γm 終がマッチ– Implies 次γ0と次γ1 がマッチ、かつ次γ1次γ2次 … 次γm 終と次γ2次 … 次γm 終 がマッチ
∵ (次,次) のペアを使うしかないので– 以下straightforward
QED

補題の系
• If STSが”Yes” then PCPが”Yes”• 問題点– If PCPが”Yes” then STSが”Yes”–ではない– そもそもこんなペアが…
(x, x) for all x∈{次}∪Δ正しい作り方G=(Δ, P ), ws , wf

に対して…

• Σ = {始, 終, 次, 次} ∪ Δ ∪ Δ• ( 始,始次ws) こうすると• ( 始,始次ws) 「始」で始まり「終」で終わらざるを得ない• (次wf終, 終 )• ( x, x )for all x ∈ {次}∪Δ• ( x, x )for all x ∈ {次}∪Δ• ( α, β )for all α→β ∈ P• ( α, β )for all α→β ∈ P

補題二つ （証明はさっきとほぼ同じなので略）• ws =γ0 ⇒γ1 ⇒ … ⇒γ2m = wfiff• 始 次 γ0 次 γ1 … 次 γ2m-1 次γ2m 終で一致するようなマッチングがPCPにある• ws =γ0 ⇒γ1 ⇒ … ⇒ γ2m+1 = wfiff• 始 次 γ0 次γ1 … 次 γ2m 次γ2m+1 終で一致するようなマッチングがPCPにある

系• If STSが”Yes” then

PCPが”Yes”• 追加の補題 (easy)：– このPCPのマッチは、必ず 始(次Δ*)?(次Δ*次Δ*)*終 の形• 系： If PCPが “Yes” then STSが”Yes”• 系： PCPは決定丌能
QED

まとめ•

チューリングマシンの停止性→ Semi-Thue System (or 0型文法)のワード問題→ Postの対応問題• 計算履歴 （文法の導出履歴）がPCPのマッチング結果になるようにエンコード– 導出規則をそのままPCPの文字列ペアに– 最初と最後を１つずらす

Thank you for listening !