制約処理ルール

制約処理ルール( CHR ) は、宣言型ルールベースのプログラミング言語で、1991 年にドイツのミュンヘンにある欧州コンピュータ産業研究センター (ECRC) の Thom Frühwirth によって導入されました。^{[ 1 ] [ 2 ]}元々は制約プログラミングを目的としていましたが、CHR は文法誘導、^{[ 3 ]}型システム、^{[ 4 ]}アブダクティブ推論、マルチエージェントシステム、自然言語処理、コンパイル、スケジューリング、時空間推論、テスト、検証などの分野で応用されています。

CHR プログラム（制約ハンドラとも呼ばれる）は、論理式の多重集合である制約ストアを維持する一連のルールです。ルールの実行により、ストアに式が追加または削除され、プログラムの状態が変わります。特定の制約ストアでルールが「発火」する順序は、抽象意味論によれば非決定論的であり^{[ 5 ]} 、洗練された意味論によれば決定論的（トップダウンのルール適用）です^{[ 6 ]}。

CHR はチューリング完全であるが、^{[ 7 ]}それ自体がプログラミング言語として一般的に使用されることはない。むしろ、制約によってホスト言語を拡張するために使用される。Prolog は圧倒的に人気のあるホスト言語であり、SICStusやSWI-Prologなど、いくつかの Prolog 実装に CHR が含まれているが、 Haskell、^{[ 8 ]} Java、C、^{[ 9 ]} SQL、^{[ 10 ]} JavaScript ^{[ 11 ]}用の CHR 実装も存在する。Prolog とは対照的に、CHR ルールはマルチヘッドであり、前方連鎖アルゴリズムを使用してコミット選択方式で実行される。

CHRプログラムの具体的な構文はホスト言語に依存し、実際には、プログラムはホスト言語のステートメントを埋め込んで、いくつかのルールを処理するために実行されます。ホスト言語は、論理変数を含む項を表すためのデータ構造を提供します。項は制約を表し、プログラムの問題領域に関する「事実」と考えることができます。従来、ホスト言語としてはPrologが使用されてきたため、そのデータ構造と変数が使用されます。このセクションの残りの部分では、CHR文献でよく用いられる中立的な数学的表記法を使用します。

CHRプログラムは、制約ストアと呼ばれるこれらの用語のマルチセットを操作するルールで構成されます。ルールには3つのタイプがあります。^{[ 5 ]}

• 簡略化ルールは次の形式をとる。${\displaystyle h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$彼らが頭を合わせるとき${\displaystyle h_{1},\dots ,h_{n}}$そして警備員たち${\displaystyle g_{1},\dots ,g_{m}}$保留、簡略化ルールにより、見出しが本文に書き換えられる可能性があります${\displaystyle b_{1},\dots ,b_{o}}$。
• 伝播規則は次の形式をとる${\displaystyle h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$これらのルールは、ヘッダーを削除せずに、ボディ内の制約をストアに追加します。
• 簡略化ルールは簡略化と伝播を組み合わせたものです。${\displaystyle h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$シンパゲーションルールが発火するには、制約ストアがヘッド内のすべてのルールに一致し、ガードが真である必要があります。${\displaystyle \ell }$制約の前に${\displaystyle \backslash }$伝播規則のように保持され、残りの${\displaystyle n-\ell }$制約が取り除かれる。

シンパゲーション規則は単純化と伝播を包含するため、すべてのCHR規則は次の形式に従います。

${\displaystyle H_{k}\,\backslash \,H_{r}\Longleftrightarrow G\,|\,B}$

それぞれの${\displaystyle H_{k},H_{r},G,B}$これは制約の論理積です。${\displaystyle H_{k},H_{r}}$そして${\displaystyle B}$CHR制約を含み、ガード${\displaystyle G}$内蔵されています。${\displaystyle H_{k},H_{r}}$空であってはならない。

ホスト言語は、項に対する組み込み制約も定義する必要があります。ルール内のガードは組み込み制約であるため、ホスト言語コードを効果的に実行します。組み込み制約理論には、少なくともtrue（常に成り立つ制約）、fail（決して成り立たず、失敗を通知するために使用される制約）、および項の等価性、つまり単一化が含まれている必要があります。^{[ 7 ]}ホスト言語がこれらの機能をサポートしていない場合は、CHR とともに実装する必要があります。^{[ 9 ]}

CHR プログラムの実行は、初期制約ストアから始まります。プログラムは、ストアに対してルールを照合しfailて適用し、一致するルールがなくなるか（成功）、制約が導出されるまで処理を進めます。前者の場合、制約ストアはホスト言語プログラムによって読み取られ、関心のある事実を検索できます。マッチングは「一方向統合」として定義されます。つまり、方程式の一方の側のみの変数を束縛します。パターンマッチングは、ホスト言語がサポートしている場合、統合として簡単に実装できます。^{[ 9 ]}

% X leq Y は、変数 X が変数 Y 以下であることを意味します。 反射律 @ X leq X <=> true。 反対称性@ X leq Y、Y leq X <=> X = Y。 推移性@ X leq Y、Y leq Z ==> X leq Z。 冪等性 @ X leq Y \ X leq Y <=> true。 

A ≤ B、B ≤ C、C ≤ A

特定の制約ストアに対してどのルールを「発火」させるかを決定するために、CHR の実装では何らかのパターンマッチングアルゴリズムを使用する必要があります。候補となるアルゴリズムにはRETEやTREAT ^{[ 12 ]}がありますが、ほとんどの実装ではLEAPSと呼ばれる遅延アルゴリズムを使用しています^{[ 13 ]}。

CHRのセマンティクスの元の仕様は完全に非決定論的でしたが、Duckらによるいわゆる「洗練された操作セマンティクス」によって非決定論性の多くが取り除かれ、アプリケーション開発者はプログラムのパフォーマンスと正確性のために実行順序に頼ることができるようになりました。^{[ 5 ] [ 14 ]}

CHRのほとんどのアプリケーションでは、書き換えプロセスが合流的である必要があります。そうでない場合、満足のいく割り当てを探す結果は非決定論的で予測不可能になります。合流性を確立するには、通常、次の3つの特性を使用します。^{[ 2 ]}

• CHRプログラムは、そのすべての重要なペアが結合可能である場合に、局所的に合流的である。
• CHRプログラムは、無限計算がない場合に終了するプログラムと呼ばれる。
• 終了型CHRプログラムは、そのすべての重要なペアが結合可能である場合に合流的である。

• 制約プログラミング
• 制約論理プログラミング
• 論理プログラミング
• 生産システム（コンピュータサイエンス）
• ビジネスルールエンジン
• 書き換え

• Christiansen, Henning. " CHR文法" 論理プログラミングの理論と実践 5.4-5 (2005): 467-501.

• 公式サイト
• CHR文献目録
• CHRのメーリングリスト
• ルーヴェン・カトリック大学CHRシステム
• WebCHR：CHRウェブインターフェース