LoginSignup
16
10

More than 3 years have passed since last update.

@x_x_l

ライスの定理について

Last updated at Posted at 2018-09-24

はじめに

　ライスの定理とは，簡単に言ってしまうと「プログラムに関する述語の決定不能性をまとめて示す定理」 のことである．
　Haskellなどでプログラムを書いていて，関数に対する同値性などを定義したくなったことはないだろうか？しかし，各種言語において関数の同値性はデフォルト実装はされていないはずである．その理由について，ライスの定理が1つの答えになるかもしれない．

  • 決定不能な述語とは，述語相当のプログラム（入力に対して，TrueかFlaseを返す）を作成することが数学的に不可能な述語である

  • つまり，決定不能な述語について知っておくと，数学的に不可能な問題に取り組んで時間を無駄にするということがない

    • なので，プログラマーがライスの定理を理解する，またそのステートメント相当の感覚をもっておくことは有意義だと思われる（この記事を書くことも有意義だと思われる）
    • 実際に，私は作ろうとしていたプログラムが，ライスの定理の系から作成不可能だと気づいたことで，不可能な問題に取り組むことで人生をすべて消費せずに済んだ1

  • ライスの定理の証明には立ち入らないで，そのステートメントについて解説する（だけどパラメタ定理からわりとすぐに証明できるから，時間があったら追記するかも）

本記事で紹介する定理等の表記は，参考文献にあげる「コンピュータと数学」に準ずる．
本記事では，証明や議論などを，プログラミングが浸透している今日における直感に委ね済ませている部分もあるが，上記の本ではそれを厳密に定義し証明している（ので，みなさん購入しましょう！）

準備・前提

ライスの定理のステートメントを述べるために，いくか用語を準備する．

  • 指標
  • 万能プログラム（関数）
  • 決定不能（述語，問題）

指標

　今更ここに書くまでもなく，（大半のプログラミング言語で）プログラムとは文字列でありプログラムを表す文字列はある自然数に対応させることができる（マトリックスとかデジモンとか観て育ってきた私達には，プログラムが01列ということを皮膚感覚で分かっているし，01列を2進数列とみなせば1つの自然数になる）
　文字列を自然数にうまく（自然数化後に文字列に戻すことも可能であるように）対応させる方法はいくつかあるが，1つの方法は記事を書いたのでみて．

　ところで，漠然とプログラムといっても，現代では様々なプログラミング言語があり具体的なイメージが定まるものではない．そこで，今回は以下のような条件を満たすプログラミング言語について考えることにする．

  1. チューリング完全である
  2. この言語におけるプログラムは，自然数を入力と出力にとるプログラムであり，入力に対して出力結果が毎回同じである
  • 1番目の条件は，標準的なプログラミング言語と同等の計算力があるということである（大体のプログラミング言語はチューリング完全になってしまう)
  • 2番目の条件は，この言語におけるプログラムが自然数上の関数としてみなせることを表している（つまり，C言語の「関数」のように，外部変数の値によって関数の出力が変わったりしない，ということである）．ただし，チューリング完全なプログラミング言語でのプログラムは無限ループをする可能性があるため，部分関数とみなせるというのが正確である．
  • なお，2番めの条件によって，このプログラミング言語が他のモダンな言語（自然数以外も扱える）のプログラムよりも計算能力において劣るということはない（1番目のチューリング完全という条件から，計算能力においては等価であることに変わりない）

上記の条件を満たすようなプログラム$P$を自然数化した値$e$を，（$P$の）指標$e$という．

万能プログラム（関数）

　これもここに書くまでのことでないが，現代のプログラムは，プログラムごとに計算用機械を用意する必要はなく，プログラム（文字列）を渡せばそのプログラムをシミュレートする万能な（かつある種メタな）プログラム2，素朴な意味でのコンパイラ，インタプリタのようなものがある．

　よって，ある有能な$n+1$引数のプログラム$\gamma$は，任意の$n$引数プログラムの指標$e$を受け取り，そのプログラムをシミュレートし$e$と同じ様に振る舞える．
　今回はプログラムを自然数の部分関数とみなしているので，$e$が表す関数を$f_e$とすると 

f_e(x_1,x_2,...,x_n) = \gamma(e,x_1,x_2,...,x_n)

が成り立つ（部分関数としての$=$であるため，未定義$=$未定義の場合があることに注意．また，$e$に相当するプログラムがない場合，無限ループするプログラム，つまり定義域が空の関数だとする）．
$\gamma$に$e$のみ適用させたもの，つまり指標$e$のプログラムが計算する関数を$\{e\}_ n$と表す．以下の式が成り立つことに注意する．

\forall e \in \mathbb{N}, \exists e’ \in \mathbb{N} [ e \neq e’ \text{かつ} 
 \{e\} _n = \{e’\} _n ]

これは，プログラムの機能（関数）としては同じであるが，プログラム文字列として違うものが存在するということを述べている．例えば，余分なスペースをn個追加するであったり，無害で無意味な操作（$x:=x$などの意味のない代入）をn回繰り返すであったりを元のプログラムに施すことを考えれば明らかである．

決定不能（述語，問題）

※以下に述べることは，停止性問題（Halting Problem）のことなので知っている方はスキップしてください．

　指標の章に書いたとおり，プログラムは停止せずに答えが永久に帰ってこないことがありうる．では，あるプログラムの指標を受け取り，「その指標が表すプログラムが，ある自然数の入力に対し，停止するか否か」を事前に判定するプログラム（コンパイラによるチェックに近い）を作ることができるだろうか？
実は，以下の議論から，そのような停止性を判定するプログラムが作成できないことが判明している．

  • $halt(x,y)$という，指標$x$が表すプログラムに$y$を適用させた場合に，停止（True）か非停止（False)を返すプログラムが存在すると仮定して矛盾を導く
  • $X(x)$というプログラムを考え，このプログラムは，$halt(x,x)$がTrueの場合には何かしらの方法で無限ループをし，Falseの場合には何かしらの値を返し停止する天の邪鬼だとする
  • $X(x)$の指標を$e$とした場合，$halt(e,e)$の値を考えると，Trueと仮定しても， Falseと仮定しても矛盾する（ともにTrueかつFalseということになってしまう）
  • よってその様なプログラム $halt$ は作成することができない．

このように，メンバーシップを判定するプログラムが原理的に作れない述語を決定不能述語といい，述語が決定不能述語となるような問題を決定不能問題という．

ライスの定理（ステートメント）

以下の条件を満たす1引数述語$p$は決定不能である．

\begin{align}
&\forall x, x’ \in \mathbb{N}  [ \{x\}_n = \{x’\}_n → p(x)=p(x’) ]\tag{1} \\
&\exists x, y  \  \in \mathbb{N}  [ p(x)\neq p(y) ] \tag{2}
\end{align}
  • $(1)$については，プログラムの Syntax Property ではなく， Semantic Property によって真偽がきまる述語 だよということである
    • つまり，指標の指すプログラムの中身をちゃんと考えて，文字列として異なるプログラムでも関数的に等しい（同じ機能）ならば，同じ真偽値を返す必要がある
    • 一方で，このプログラムが特定の文字列を含むかといった情報では，この述語の真偽は決まらない（なぜならば，指標を構成する文字列に関して真偽がどうであるかについての要請はしていないので）
  • $(2)$については，この述語が恒真や恒偽ではない（から，ちゃんと指標の中身知らないとだよー）ということである

ライスの定理からの系

各自然数$n$に対して以下の述語は決定不能である．

$total_n(z)$ ：指標$z$の関数は全域である
$const_n(z)$ ：指標$z$の関数は定数関数である
$undef_n(z)$ ：指標$z$の関数の定義域が空集合である
$eq_n(z, z’)$ ：指標$z$の関数と指標$z’$の関数が，外延的に等しい


  • $eq_n$は１引数述語ではないが，この述語が作成可能だと，定義域が空のプログラム（無限ループするプログラム）の指標を渡すことで$undef_n$相当の述語が作成可能であるため，この述語も決定不能であることがわかる
  • $eq_n$が私が作ろうと一瞬思ってしまった，関数の等価性を判定するプログラム．．．
    • 関数の等価性判定がプログラム言語にデフォルトでない理由もここから帰結されるのではないだろうか？

注意事項

　ライスの定理は確かに，述語の決定不能性，ひいてはその述語に対応する判定プログラムの作成についてネガティブな主張になっている．しかし，理論的なUpperboundがあるからといって，実用的・現実的な可能性に希望が全くないわけではない．
例えば，$eq_n$などは，有限領域を動く型の関数でかつ停止する関数であれば実際に判定できるであろう．また，$halt$についても，「$n$ステップは確実にとまらない」みたいに実用観点のある述語 $halt500$みたいなものがであれば決定可能でありかつ有意義な場合もあるかもしれないし，特定の文字列を含む条件の停止性問題を判定する述語であれば，決定可能でかつそれだけでも有意義である可能性もある3．

そのような観点で，興味深い記事があったので紹介．
https://qiita.com/nwtgck/items/8371855594e6e1b2aca6

また，詳しく読めてませんが，kinabaさんのツイートも興味深かったので紹介．
https://twitter.com/kinaba/status/1005299252573102081
（Int->Intでは無理でも，特定の型だったらいけそうということかな・・・？）

上記2つは，（比較する2つの関数の）ドメインに制約があることだけではなく，その2つの関数が停止することも重要なので注意！

まとめ

  • ライスの定理を用いることで，決定不能な問題に関する嗅覚を身につけることが多少でき．場合によっては実現不可能なコードを書くことを事前に回避できる可能性がある
  • ただし，理論的に決定不能だとしても，実用的な範囲においては決定可能で意義のあるプログラムが作れる可能性は0でもない

参考文献

証明について

ライスの定理の証明は，パラメタ定理（$s_{m,n}$定理とも呼ばれる）からすぐに導くことができる．
証明の流れとしては，パラメタ定理 → （クリーネの第二）再帰定理 → （ロジャースの）不動点定理 → ライスの定理 として導ける．
※時間があれば追記する．．．
（時間がジェネレイトされた音）
よし，ステートメントと証明を書きます．

パラメタ定理

$\forall m,n \in \mathbb{N} \exists S_{m,n} \in \mathbb{PR} e \in \mathbb{N} <a_1,a_2,...,a_n> \in \mathbb{N}^n <b_1,b_2,...,b_m> \in \mathbb{m}^n$
$\gamma_{n+m}(e,a_1,a_2,...,a_n,b_1,b_2,...,b_n) = \guma$

（クリーネの第二）再帰定理

  1. 私がライスの定理相当を一人で思いつくか，諦めるかすれば，同じ様に無駄なことをせずに済んだかもしれないが，知っていたことでより多くの時間をセーブできた． ↩

  2. チューリングマシンも，万能チューリングマシンによって任意のチューリングマシンをシミュレートできる．ただのチューリングマシンは1つのプログラム相当の振る舞いしかできない（抽象）機械を指している．なんとなく，万能チューリングマシンをチューリングマシンとよんでそうな動画や解説が時々ある気がしてて，それは違うのではという気持ちがある． ↩

  3. すべての意味的に同じプログラムに同じ真偽値という要求を緩め，特定の文字列が一致した上で意味的に同じということであれば，ライスの定理の条件に当てはまらない（特定文字列が一致しないけど同じ機能のプログラムの判定については諦めることになるが）．もちろん，ライスの定理に当てはまらないことは，述語が決定可能であることの十分条件にはならず，必要条件にしかならない． ↩

16
10
1

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
16
10