停止性問題には明確な解決策がないことが知られています。a)プログラムが実際に停止し、b)任意の入力を処理するというものですが、問題に対する十分な解決策があるかどうか疑問に思いました。特定の種類のプログラムフローを完全に処理できるもの、問題を正しく解決できない場合を特定できるもの、または正しい割合が高いものなど。
もしそうなら、彼らはどれほど優れていますか、そして彼らはどのようなアイデア/制限に依存していますか?
停止性問題には明確な解決策がないことが知られています。a)プログラムが実際に停止し、b)任意の入力を処理するというものですが、問題に対する十分な解決策があるかどうか疑問に思いました。特定の種類のプログラムフローを完全に処理できるもの、問題を正しく解決できない場合を特定できるもの、または正しい割合が高いものなど。
もしそうなら、彼らはどれほど優れていますか、そして彼らはどのようなアイデア/制限に依存していますか?
通常のアプローチは、プログラムの動作を効果的に計算可能なアルゴリズムに制限することです。たとえば、単純に型付きラムダ計算を使用して、アルゴリズムが常に停止することを決定できます。これは、単純に型付きラムダ計算がチューリング完全ではないことを意味しますが、それでも多くの興味深いアルゴリズムを表すのに十分強力です。
特定の種類のプログラムフローを完全に処理できるもの
これは簡単で、「特定のタイプ」が狭くなるほど簡単になります。原始的な例:任意の開始値について、次のコードが終了するかどうかを決定しますx
。
void run(int x)
{
while(x != 0)
{
x = x > 0 ? x-2 : x+2;
}
}
ソリューションはコード自体よりも短いです。
または、問題を正しく解決できない場合を特定できます
繰り返しますが、上記のプログラムを使用して、プログラムが固定の狭いスキーマに適合しない場合は「no」と応答するようにします。
または正しい割合が高いもの
可能な入力の無限のセットに対して「高い」パーセンテージをどのように定義しますか?
ループが停止していることを証明する1つの方法は、ループが実行されるたびに常に減少し、その変数がゼロ未満になるとループが終了する整数変数(必ずしもプログラム内で明示的にではない)を識別することです。この変数をループ変種と呼ぶことができます。
次の小さなスニペットについて考えてみます。
var x := 20;
while (x >= 0) {
x := x - 1
}
ここでは、ループが実行されるたびにxが減少し、x <0になるとループが終了することがわかります(明らかに、これはそれほど厳密ではありませんが、理解できます)。したがって、xをバリアントとして使用できます。
もっと複雑な例はどうですか?整数の有限リスト、L = [L [0]、L [1]、...、L[n]]を考えてみましょう。in(L, x)
xがLのメンバーである場合はtrueです。次に、次のプログラムについて考えてみます。
var x := 0;
while (in(L, x)) {
x := x + 1
}
これは自然数(0、1、2、...)を検索し、Lにないxの値が見つかると停止します。では、これが終了することをどのように証明しますか?Lには最大値が必要です-それをmax(L)と呼びます。次に、バリアントをとして定義できますmax(L) - x
。終了を証明するには、まずそれmax(L) - x
が常に減少していることを証明する必要があります。xが常に増加していることを証明できるので、それほど難しくはありません。次に、ループが。のときに終了することを証明しますmax(L) - x < 0
。の場合max(L) - x < 0
、max(L) < x
これはxがLに含まれない可能性があることを意味するため、ループは終了します。
ターミネータープロジェクトに関連する論文を参照してください。
http://research.microsoft.com/en-us/um/cambridge/projects/terminator/
非常に大きくても、マシンが停止するかどうかが明らかな場合があります。「カウントダウン」変数の存在など、パターンを特定したら、それを備えたすべてのマシンで機能する小さなマシンを作成できます。それは無限の家族ですが、すべての可能なマシンのごくわずかな断片です。ほとんどの人間が書いた機械は、そのサイズに対して非常に単純な振る舞いをしているので、それらの多くが実際の時間/空間で解決できればそれほど驚くことではありませんが、それを測定する方法がわかりません。
「それらがどれだけ優れているか」という問題がどれほど難しいかを知るために、理論的に非常に興味深い質問があります。特定のサイズNに対して、サイズNのマシンがいくつ停止するのでしょうか。これは計算不可能であり(計算できるマシンを使用して停止性問題を解決できるため)、N>4では不明です。
はい、状態空間を有限にするだけで、(理論的には)すべての入力で可能になります。(すべての可能性を繰り返すだけです。)
したがって、理論的には、実際のコンピューターで実行されているすべてのプログラムで可能です。(分析を行うには、プログラムを実行するコンピューターよりも大量のRAMを搭載したコンピューターを使用する必要がある場合があります。もちろん、分析には非常に長い時間がかかります。)
おそらくあなたはもっと実用的なものが欲しいでしょう。この場合、言語について考えてください。構文の正しさ/不正確さの問題は、(言語の種類と入力の長さに応じて)非常に迅速に判断できますが、入力として提供できるプログラムは無限にあります。(注:入力プログラムの実行について話しているのではなく、構文的に正しいかどうかを判断するだけです。)