実行時アルゴリズムの特殊化

コンピュータ サイエンスにおいて、実行時アルゴリズムの特殊化は、特定の種類のコストのかかる計算タスクに対して効率的なアルゴリズムを作成するための方法論です。この方法論は、自動定理証明の分野、より具体的には、ヴァンパイア定理証明プロジェクトに端を発しています。

このアイデアは、プログラム変換を最適化する際に部分評価を使用することからヒントを得ています。定理証明器の多くのコア操作は、次のパターンを示します。の値が、潜在的に多くの異なる値に対して固定されている状況で、何らかのアルゴリズムを実行する必要があるとします。これを効率的に行うには、固定されたすべての に対しての特殊化、つまり を実行することがを実行することと同等であるようなアルゴリズムを見つけようとすることができます。 ${\displaystyle {\mathit {alg}}(A,B)}$${\displaystyle A}$ ${\displaystyle B}$${\displaystyle {\mathit {alg}}}$${\displaystyle A}$${\displaystyle {\mathit {alg}}_{A}}$${\displaystyle {\mathit {alg}}_{A}(B)}$${\displaystyle {\mathit {alg}}(A,B)}$

特殊なアルゴリズムは、固定値 の特定の特性を利用できるため、汎用アルゴリズムよりも効率的である可能性があります。通常、 は、この特定のパラメータ に対して冗長であることがわかっている場合、実行する必要がある一部の操作を回避できます。特に、 に対して真または偽となるテストを特定したり、ループや再帰を展開したり できることがよくあります。${\displaystyle A}$${\displaystyle {\mathit {alg}}_{A}(B)}$${\displaystyle {\mathit {alg}}(A,B)}$${\displaystyle A}$${\displaystyle A}$

実行時の特殊化と部分評価の主な違いは、特殊化されるの値が静的にわかっていないため、特殊化が実行時に行われるという点です。 ${\displaystyle A}$${\displaystyle {\mathit {alg}}}$

重要な技術的な違いもあります。部分評価は、何らかのプログラミング言語でコードとして明示的に表現されたアルゴリズムに適用されます。実行時には、 の具体的な表現は必要ありません。特殊化手順をプログラムするときに想像するだけで済みます。必要なのは、特殊化されたバージョンの の具体的な表現だけです。これはまた、部分評価では通常そうであるように、アルゴリズムを特殊化するための普遍的な方法を使用できないことを意味します。代わりに、特定のアルゴリズムごとに特殊化手順をプログラムする必要があります。そうすることの重要な利点は、 の特殊性とおよびの表現を利用する強力なアドホックなトリックを使用できることです。これは、普遍的な特殊化方法では対応できないものです。 ${\displaystyle {\mathit {alg}}}$ ${\displaystyle {\mathit {alg}}}$ ${\displaystyle {\mathit {alg}}_{A}}$${\displaystyle {\mathit {alg}}}$${\displaystyle {\mathit {alg}}}$${\displaystyle A}$${\displaystyle B}$

特殊なアルゴリズムは、解釈可能な形式で表現する必要があります。多くの場合、通常、を連続した多くの値で計算する必要がある場合、 を特殊な抽象マシンのコードとして記述でき、 はコンパイルされるとよく言われます。次に、抽象マシンの命令のセマンティクスのみに依存する答え保存変換によって、コード自体をさらに最適化できます。 ${\displaystyle {\mathit {alg}}_{A}(B)}$${\displaystyle B}$${\displaystyle {\mathit {alg}}_{A}}$${\displaystyle A}$

抽象マシンの命令は通常、レコードとして表すことができます。このようなレコードの 1 つのフィールドには、命令の種類を識別する整数タグが格納され、他のフィールドは、命令のセマンティクスでジャンプが必要な場合、ラベルを表す別の命令へのポインタなど、命令の追加パラメータを格納するために使用される場合があります。コードのすべての命令は、配列、リスト、またはツリーに格納できます。

解釈は、命令をある順序でフェッチし、そのタイプを識別し、このタイプに関連付けられたアクションを実行することによって行われます。Cまたは C++ では、switch ステートメントを使用して、いくつかのアクションを異なる命令タグに関連付けることができます。最近のコンパイラは通常、値に対応するステートメントのアドレスを特別な配列の -番目のセルに格納することにより、狭い範囲の整数ラベルを持つswitchステートメントを効率的にコンパイルします。小さな整数間隔から命令タグの値を取得することで、これを利用できます。 ${\displaystyle i}$${\displaystyle i}$

の多くのインスタンスが長期保存を目的としており、 の呼び出しがとともに予測できない順序で発生する状況があります。たとえば、最初に をチェックし、次に、次になどをチェックする必要がある場合があります。このような状況では、メモリの使用量が多くなるため、コンパイルによる全面的な特殊化は適切でない可能性があります。ただし、とともに、または の代わりに を保存できる、 すべての に対してコンパクトな特殊化表現が見つかる場合があります。また、この表現で機能し、 への呼び出しが に置き換えられるバリアントも定義します。これは、同じジョブをより高速に実行することを目的としています。 ${\displaystyle A}$${\displaystyle {\mathit {alg}}(A,B)}$${\displaystyle B}$${\displaystyle {\mathit {alg}}(A_{1},B_{1})}$${\displaystyle {\mathit {alg}}(A_{2},B_{2})}$${\displaystyle {\mathit {alg}}(A_{1},B_{3})}$${\displaystyle A^{\prime}}$${\displaystyle A}$${\displaystyle A}$${\displaystyle {\mathit {alg}}^{\prime}}$${\displaystyle {\mathit {alg}}(A,B)}$${\displaystyle {\mathit {alg}}^{\prime }(A^{\prime },B)}$

• Psyco 、 Pythonに特化したランタイムコンパイラ
• 多段階プログラミング

• A. Voronkov、「ヴァンパイアの解剖学: コードツリーによるボトムアップ手順の実装」、Journal of Automated Reasoning、15(2)、1995 (オリジナルのアイデア)

• A. Riazanov およびA. Voronkov、「用語順序制約の効率的なチェック」、Proc. IJCAR 2004、人工知能講義ノート 3097、2004 (簡潔だが自己完結的な方法の解説)
• A. Riazanov および A. Voronkov、「標準およびリレーショナル パス インデックスによる効率的なインスタンス検索」、Information and Computation、199(1-2)、2005 (この方法の別の図解が含まれています)
• A. リアザノフ、「効率的な定理証明器の実装」、マンチェスター大学博士論文、2003 年 (最も包括的な方法の説明と多くの例が含まれています)