同時制約論理プログラミング

並行制約論理プログラミングは、制約充足問題を解決するのではなく（またはそれに加えて） 、並行プロセスをプログラミングすることを主な目的とした制約論理プログラミングのバージョンです。制約論理プログラミングの目標は並行して評価されるため、並行プロセスはインタープリタによる目標の評価としてプログラムされます。

構文的には、並行制約論理プログラムは非並行プログラムに似ていますが、唯一の例外は、節にガード (いくつかの条件下では節の適用可能性をブロックする制約) が含まれることです。意味的には、並行制約論理プログラミングは、目標評価が問題の解決策を見つけることではなく、並行プロセスを実現することを目的としているため、非並行バージョンとは異なります。最も顕著なのは、この違いが、複数の節が適用可能な場合のインタープリタの動作に影響することです。非並行制約論理プログラミングはすべての節を再帰的に試行しますが、並行制約論理プログラミングは 1 つの節だけを選択します。これは、インタープリタの意図された方向性の最も明白な効果であり、インタープリタは以前に選択した選択を修正することはありません。これによるその他の効果は、評価全体が失敗しない間に証明できない目標を持つ意味上の可能性、および目標と節の先頭を同一視する特定の方法などです。

制約処理ルールは、並行制約論理プログラミングの一種と見なすことができますが、^[1]並行プロセスではなく、制約単純化器またはソルバーをプログラミングするために使用されます。

制約論理プログラミングでは、現在の目標の目標が順番に評価されます。通常は、新しい目標が最初に評価されるLIFO順序で進行します。並行バージョンの論理プログラミングでは、目標を並行して評価できます。すべての目標はプロセスによって評価され、プロセスは並行して実行されます。これらのプロセスは制約ストアを介して対話します。つまり、あるプロセスが制約ストアに制約を追加している間に、別のプロセスが制約がストアによって必然的に含まれるかどうかをチェックします。

ストアへの制約の追加は、通常の制約論理プログラミングと同様に行われます。制約の含意のチェックは、節のガードを介して行われます。ガードには構文拡張が必要です。並行制約論理プログラミングの節は、節のガードと呼ばれる制約として記述されますH :- G | B。G大まかに言えば、ガードがリテラルの等式と節のヘッドが追加された後に制約ストアによって含意される場合にのみ、この節の新しいバリアントを使用してゴール内のリテラルを置き換えることができます。このルールの正確な定義はより複雑で、以下で示します。

非並行制約論理プログラミングと並行制約論理プログラミングの主な違いは、前者は検索を目的としているのに対し、後者は並行プロセスの実装を目的としていることです。この違いは、選択を元に戻せるかどうか、プロセスを終了させないかどうか、目標と節の先頭がどのように等しくなるかに影響します。

通常の制約論理プログラミングと並行制約論理プログラミングの最初の意味上の違いは、ゴールの証明に複数の節を使用できる条件に関するものです。非並行論理プログラミングでは、ゴールを書き換えるときにすべての可能な節を試します。つまり、ゴールを新しい節の変形の本体に置き換えてもゴールが証明できない場合は、別の節があればそれが証明されます。これは、ゴールを証明することが目的であるためです。ゴールを証明するためのすべての可能な方法が試されます。一方、並行制約論理プログラミングは、並列プロセスのプログラミングを目的としています。一般的な並行プログラミングでは、プロセスが選択を行うと、その選択を元に戻すことはできません。並行バージョンの制約論理プログラミングでは、プロセスが選択を行うことを許可し、選択後はその選択にコミットすることでプロセスを実装します。技術的には、ゴールのリテラルを書き換えるために複数の節を使用できる場合、非並行バージョンではすべての節を順番に試しますが、並行バージョンでは任意の節を 1 つ選択します。非並行バージョンとは異なり、他の節が試されることはありません。複数の選択肢を処理するこれら 2 つの異なる方法は、しばしば「知らない非決定性」と「気にしない非決定性」と呼ばれます。

ゴール内のリテラルを書き換える場合、考慮される節は、制約ストアとリテラルと節のヘッドの等式との結合によってガードが伴う節だけです。ガードは、どの節をまったく考慮しないかを伝える方法を提供します。これは、同時制約論理プログラミングの単一の節へのコミットメントを考えると特に重要です。節が一度選択されると、この選択は再検討されません。ガードがなければ、インタープリタはリテラルを書き換えるために「間違った」節を選択する可能性がありますが、他の「適切な」節が存在する可能性があります。非同時プログラミングでは、インタープリタは常にすべての可能性を試すため、これはそれほど重要ではありません。同時プログラミングでは、インタープリタは他の可能性を試すことなく単一の可能性にコミットします。

非並行バージョンと並行バージョンの違いによる 2 つ目の影響は、並行制約論理プログラミングは、プロセスが終了せずに実行できるように特別に設計されていることです。並行処理では、一般的に非終了プロセスが一般的です。制約論理プログラミングの並行バージョンでは、失敗の条件を使用しないことで非終了プロセスを実装します。つまり、目標の書き換えに適用できる節がない場合、非並行制約論理プログラミングのように評価全体が失敗するのではなく、この目標を評価するプロセスが停止します。その結果、続行できる節がないため、目標を評価するプロセスが停止する可能性がありますが、同時に他のプロセスは実行を継続します。

異なる目標を解決しているプロセス間の同期は、ガードの使用によって実現されます。使用可能なすべての節に制約ストアによって伴われないガードがあるために目標を書き換えることができない場合、この目標を解決しているプロセスは、他のプロセスが少なくとも 1 つの適用可能な節のガードを伴わせるために必要な制約を追加するまでブロックされます。この同期はデッドロックの影響を受けます。すべての目標がブロックされると、新しい制約は追加されず、したがって目標のブロックが解除されることはありません。

並行論理プログラミングと非並行論理プログラミングの違いによる 3 つ目の影響は、目標が節の新しい変種のヘッドと等しくなる方法にあります。操作的には、ヘッド内の変数が、ヘッドが目標と等しくなるような方法で項と等しくなるかどうかをチェックすることで、これが行われます。このルールは、制約論理プログラミングの対応するルールとは異なり、変数がヘッドの 1 つである場合に、変数 = 項の形式でのみ制約を追加できます。この制限は、目標と節のヘッドが異なる方法で扱われるという点で、方向性の一形態と見なすことができます。

H:-G|B正確には、節の新しい変種を使用してゴールを書き換えることができるかどうかを判断するルールはA次のとおりです。まず、とが同じ述語を持つかどうかがチェックされますA。次に、現在の制約ストアを与えられた場合にとH等しくする方法が存在するかどうかがチェックされます。通常の論理プログラミングとは異なり、これは片側ユニフィケーションの下で行われ、ヘッドの変数が項と等しくなることのみが許可されます。3 番目に、制約ストアと第 2 ステップで生成された方程式からガードが含意されているかどうかがチェックされます。ガードには、節のヘッドで言及されていない変数が含まれている場合があります。これらの変数は存在的に解釈されます。ゴールを置き換えるために節の新しい変種の適用可能性を決定するこの方法は、次のように簡潔に表現できます。現在の制約ストアは、ヘッドとガードの変数の評価が存在し、ヘッドがゴールと等しくガードが含意されることを含意します。実際には、含意は不完全な方法でチェックされる場合があります。 ${\displaystyle A}$${\displaystyle H}$

並行論理プログラミングの構文とセマンティクスの拡張は、アトミック tellです。インタープリタが節を使用すると、そのガードが制約ストアに追加されます。ただし、本体の制約も追加されます。この節へのコミットメントにより、インタープリタは、本体の制約がストアと一致していない場合にバックトラックしません。この状態は、アトミック tell を使用することで回避できます。これは、節に、一貫性のみがチェックされる一種の「第 2 のガード」が含まれるバリアントです。このような節は と記述されます。この節は、が制約ストアによって含意され、それと一貫性があるH :- G:D|B場合にのみ、リテラルを書き換えるために使用されます。この場合、と の両方が制約ストアに追加されます。 GDGD

並行制約論理プログラミングの研究は、並行論理プログラミングの原理の一部がマイケル・J・マーハーによって制約論理プログラミングに統合された1980年代末に始まりました。並行制約論理プログラミングの理論的特性は、その後、マーティン・リナードやビジェイ・A・サラスワットを含むさまざまな著者によって研究されました。^[2]

• Curryは、並行システムのプログラミングを可能にする論理関数型プログラミング言語です[1]。
• トゥーントーク
• ヤヌス
• アリス

• Marriott, Kim; Peter J. Stuckey (1998)。制約付きプログラミング: 入門。MIT プレス。  0-262-13341-5出版年月日
• Frühwirth, Thom; Slim Abdennadher (2003).制約プログラミングの基礎. Springer.  3-540-67623-6出版年月日
• Jaffar, Joxan; Michael J. Maher (1994). 「制約論理プログラミング: 概観」. Journal of Logic Programming . 19/20: 503– 581. doi : 10.1016/0743-1066(94)90033-7 .