Loading article…
コンピュータ科学において、終了性解析とは、与えられたプログラムの評価が各入力に対して停止するかどうかを判定しようとするプログラム解析のことである。これは、入力されたプログラムが全関数を計算するかどうかを判定することを意味する。
これは停止問題と密接に関連しており、停止問題とは、与えられたプログラムが与えられた入力に対して停止するかどうかを判定する問題であり、決定不能である。停止解析は停止問題よりもさらに難しい。計算可能な関数を実装するプログラムのモデルとしてのチューリングマシンのモデルにおける停止解析の目標は、与えられたチューリングマシンが完全なチューリングマシンであるかどうかを判定することであり、この問題はレベル算術階層に属する問題であり、したがって停止問題よりも厳密に難しい。
計算可能な関数が全関数であるかどうかという問題は半決定可能ではないため、[ 1 ]各健全な終了アナライザ（つまり、終了しないプログラムに対して肯定的な答えは決して与えられない）は不完全であり、つまり、無限に多くの終了するプログラムに対して、永遠に実行し続けるか、不確定な答えで停止することによって、終了を判定することに失敗するに違いない。
停止性証明は、アルゴリズムの完全な正しさが停止性に依存するため、形式検証において重要な役割を果たす数学的証明の一種である。
終了証明を構築するためのシンプルで一般的な方法として、アルゴリズムの各ステップに尺度を関連付ける方法があります。この尺度は、順序数などの整礎関係の定義域から取得されます。尺度がアルゴリズムのあらゆるステップに沿って関係に従って「減少」する場合、整礎関係に関して無限に減少する連鎖は存在しないため、アルゴリズムは終了しなければなりません。
停止性解析の種類によっては、停止性証明の存在を自動的に生成したり、示唆したりすることができる。
終了する場合としない場合があるプログラミング言語の構成要素の例として、ループが挙げられます。ループは繰り返し実行できるためです。データ処理アルゴリズムでよく見られるように、カウンタ変数を使用して実装されたループは通常終了します。以下の擬似コード例でその様子を示します。
i := 0 i = SIZE_OF_DATA になるまでループする process_data(data[i])) // 位置 i のデータチャンクを処理する i := i + 1 // 処理する次のデータチャンクに移動する
SIZE_OF_DATAの値が非負で固定かつ有限である場合、process_dataも終了すると仮定すると、ループは最終的に終了します。
ループの中には、人間の目視検査によって必ず終了するものと決して終了しないものがあることが分かるものがあります。例えば、次のループは理論上は決して停止しません。しかし、物理マシン上で実行すると、演算オーバーフローによって停止する可能性があります。オーバーフローが発生すると、例外が発生したり、カウンタが負の値にラップアラウンドしてループ条件が満たされたりすることがあります。
i := 1 i = 0 になるまでループする i := i + 1
終了性解析では、未知の入力に応じてプログラムの終了動作を判定しようとする場合もある。以下の例はこの問題を示している。
i := 1 i = UNKNOWN になるまでループする i := i + 1
ここでは、ループ条件はUNKNOWNという値を用いて定義されていますが、UNKNOWNの値は不明です（例えば、プログラム実行時にユーザーが入力した値によって決まります）。この場合、終了解析ではUNKNOWNの考えられるすべての値を考慮し、UNKNOWN = 0（元の例と同様）の場合、終了を示すことができないことを明らかにする必要があります。
しかしながら、ループ命令を含む式が停止するかどうかを判定するための一般的な手順は、人間が検査を担当する場合であっても存在しない。その理論的な理由は、停止問題の不確定性にある。つまり、任意のプログラムが有限回の計算ステップ後に停止するかどうかを判定するアルゴリズムは存在し得ないのである。
実際には、アルゴリズムは限られた数のメソッドを用いて、与えられたプログラムから関連情報を抽出できるため、終了（または非終了）を示すことは困難です。あるメソッドは、ループ条件に関して変数がどのように変化するかを調べ（そのループの終了を示す可能性があります）、別のメソッドは、プログラムの計算を何らかの数学的構造に変換して処理し、この数学モデルの特性から終了動作に関する情報を取得する可能性があります。しかし、各メソッドは終了（または非終了）の特定の理由しか「見る」ことができないため、これらのメソッドを組み合わせても、終了（または非終了）のすべての可能性のある理由を網羅することはできません。
再帰関数とループは表現上同等です。ループを含む式はすべて再帰を用いて記述でき、その逆もまた同様です。したがって、再帰式の終了も一般には決定不能です。一般的に使用されている（つまり、異常ではない）ほとんどの再帰式は、さまざまな方法で終了することが示されており、通常は式自体の定義に依存します。例として、以下の階乗関数の再帰式の関数引数は常に 1 ずつ減少します。自然数の整列性により、引数は最終的に 1 に達し、再帰は終了します。
function factorial (引数は自然数) if argument = 0 or argument = 1 return 1 otherwise return argument * factorial(argument - 1)
終了性チェックは、依存型プログラミング言語や、RocqやAgdaのような定理証明システムにおいて非常に重要です。これらのシステムは、プログラムと証明の間でカリー・ハワード同型性を使用します。帰納的に定義されたデータ型の証明は、従来、帰納原理を用いて記述されていました。しかし、後に、パターンマッチングを用いた再帰的に定義された関数によってプログラムを記述する方が、帰納原理を直接使用するよりも自然な証明方法であることが分かりました。残念ながら、非終了定義を許容すると型理論に論理的な矛盾が生じるため、AgdaとRocqには終了性チェッカーが組み込まれています。
依存型プログラミング言語における終了性チェックの手法の一つに、サイズ型があります。その基本的な考え方は、再帰可能な型にサイズ注釈を付け、より小さい引数に対してのみ再帰呼び出しを許可するというものです。サイズ型は、Agdaでは構文拡張として実装されています。
終了性（または非終了性）を示す新しい手法に取り組んでいる研究チームは複数存在する。多くの研究者は、終了動作を自動的に（つまり人間の介入なしに）分析しようとするプログラムにこれらの手法を組み込んでいる[ 2 ]。研究の継続的な側面は、既存の手法を使用して「実世界の」プログラミング言語で書かれたプログラムの終了動作を分析できるようにすることである。Haskell 、Mercury、Prologなどの宣言型言語については、多くの成果が存在する[ 3 ] [ 4 ] [ 5 ]（主にこれらの言語の強力な数学的背景による）。研究コミュニティはまた、CやJavaなどの命令型言語で書かれたプログラムの終了動作を分析するための新しい手法にも取り組んでいる。
自動プログラム終了解析に関する研究論文には、以下のようなものがある。
自動終了解析ツールのシステム説明には以下が含まれます。
