制約処理ルール

制約処理ルール (CHR)
パラダイム	制約ロジック、宣言的
デザイン：	トム・フリューヴィルト
初登場	1991年; 33年前
Webサイト	制約処理ルール.org
影響を受けた
	プロローグ

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

CHRプログラムは、制約ハンドラとも呼ばれ、制約ストア（論理式の集合）を管理するルールのセットです。ルールを実行すると、ストアから式が追加または削除され、プログラムの状態が変わります。特定の制約ストアでルールが実行される順序は、その抽象セマンティクスに従って非決定的であり、^{[5] 、その}洗練されたセマンティクスに従って決定的（トップダウンのルール適用）です。^[6]

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

言語の概要

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

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

簡略化規則はという形式をとります。ヘッドが一致し、ガードが成立する場合、簡略化規則によってヘッドが本体に書き換えられることがあります。 $h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$ $h_{1},\dots ,h_{n}$ $g_{1},\dots ,g_{m}$ $b_{1},\dots ,b_{o}$
伝播ルールの形式はです。これらのルールは、ヘッドを削除せずに、本体の制約をストアに追加します。 $h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$
シンパゲーションルールは、簡略化と伝播を組み合わせたものです。と記述されます。シンパゲーションルールが発動するには、制約ストアがヘッド内のすべてのルールと一致し、ガードが true である必要があります。の前の制約は、伝播ルールののように保持され、残りの制約は削除されます。 $h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$ $\ell$ $\backslash$ $n-\ell$

単純化ルールは単純化と伝播を包含するため、すべてのCHRルールは次の形式に従います。

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

ここで、のそれぞれは制約の結合です。およびには CHR 制約が含まれ、ガードは組み込まれています。の 1 つだけが空でない必要があります。 $H_{k},H_{r},G,B$ $H_{k},H_{r}$ $B$ $G$ $H_{k},H_{r}$

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

CHR プログラムの実行は、最初の制約ストアから始まります。その後、プログラムは、ルールをストアと照合して適用し、一致するルールがなくなる (成功) か、fail制約が導出されるまで続行します。前者の場合、制約ストアは、興味のある事実を探すためにホスト言語プログラムによって読み取ることができます。マッチングは「一方向のユニフィケーション」として定義されます。つまり、方程式の片側でのみ変数をバインドします。パターンマッチングは、ホスト言語がサポートしている場合、ユニフィケーションとして簡単に実装できます。^[9]

サンプルプログラム

Prolog 構文の次の CHR プログラムには、以下または等しい制約のソルバーを実装する 4 つのルールが含まれています。便宜上、ルールにはラベルが付けられています (CHR ではラベルはオプションです)。

 % 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 。

規則は 2 つの方法で読むことができます。宣言的な読み方では、規則のうち 3 つが部分順序の公理を指定します。

反射性: X ≤ X
反対称性: X ≤ YかつY ≤ Xならば、X = Y
推移性: X ≤ YかつY ≤ Zならば、X ≤ Z

これら 3 つの規則はすべて暗黙的に全称量化されています (大文字の識別子は Prolog 構文の変数です)。べき等性規則は論理的観点からはトートロジーですが、プログラムの 2 回目の読み取りでは目的があります。

上記を解釈する 2 番目の方法は、オブジェクトに関する事実 (制約) のコレクションである制約ストアを維持するためのコンピュータプログラムとして解釈することです。制約ストアはこのプログラムの一部ではなく、別途提供する必要があります。ルールは、次の計算ルールを表します。

反射性は単純化の規則です。つまり、 X ≤ Xの形式の事実がストア内で見つかった場合、それを削除できることを表します。
反対称性も単純化規則ですが、ヘッドが 2 つあります。ストア内で形式X ≤ YおよびY ≤ Xの 2 つの事実 (一致するXおよびY )が見つかった場合、それらを単一の事実X = Yに置き換えることができます。このような等式制約は組み込みと見なされ、通常は基礎となる Prolog システムによって処理される統合として実装されます。
推移性は伝播ルールです。単純化とは異なり、制約ストアから何も削除しません。代わりに、X ≤ YおよびY ≤ Zの形式 ( Yの値が同じ) の事実がストア内にある場合、3 番目の事実X ≤ Zが追加されることがあります。
最後に、べき等性は単純化と伝播を組み合わせた単純化ルールです。重複する事実が見つかると、ストアから削除します。制約ストアは事実の複数のセットであるため、重複が発生する可能性があります。

クエリ

A ≤ B、B ≤ C、C ≤ A

次のような変換が発生する可能性があります。

推移規則によりが追加されますA leq C。次に、反対称規則を適用することで、A leq CとがC leq A削除され、に置き換えられますA = C。これで、反対称規則が元のクエリの最初の 2 つの制約に適用可能になります。これですべての CHR 制約が削除されたため、これ以上の規則は適用できず、次の回答A = B, A = Cが返されます。CHR は、3 つの変数すべてが同じオブジェクトを参照する必要があることを正しく推論しました。

CHRプログラムの実行

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

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

CHRのほとんどの応用では、書き換えプロセスが合流性を持つことが求められます。そうでない場合、満足のいく割り当てを検索した結果は非決定的で予測不可能なものになります。合流性の確立は通常、次の3つの特性によって行われます。^[2]

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

参照

参考文献

^ Thom Frühwirth.簡略化ルールの紹介。内部レポート ECRC-LP-63、ECRC ミュンヘン、ドイツ、1991 年 10 月、ワークショップ Logisches Programmieren、グーセン/ベルリン、ドイツ、1991 年 10 月およびワークショップ on Rewriting and Constraints、ダグストゥール、ドイツ、1991 年 10 月で発表。
^ ab Thom Frühwirth.制約処理ルールの理論と実践。制約論理プログラミング特集号（P. Stuckey および K. Marriott 編）、Journal of Logic Programming、Vol 37(1-3)、1998 年 10 月。doi : 10.1016/S0743-1066(98)10005-5
^ Dahl, Veronica、J. Emilio Miralles。「Womb grammars: 文法誘導のための制約解決」制約処理ルールに関する第 9 回ワークショップの議事録。第 624 巻、技術レポート CW。2012 年。
^ Alves、Sandra、Mário Florido。「制約処理ルールを使用した型推論」Electronic Notes in Theoretical Computer Science 64 (2002): 56-72。
^ abc Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). 「時が経つにつれ: 制約処理ルール - 1998 年から 2007 年までの CHR 研究の調査」(PDF) .論理プログラミングの理論と実践. 10 : 1. arXiv : 0906.4474 . doi :10.1017/S1471068409990123. S2CID 11044594.
^ Frühwirth, Thom (2009).制約処理ルール. Cambridge University Press. ISBN 978-0521877763。
^ ab Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). 「制約処理ルールの計算能力と複雑さ」(PDF) . ACM Transactions on Programming Languages and Systems . 31 (2): 1–42. doi :10.1145/1462166.1462169. S2CID 2691882.
^ 「CHR: 制約処理ルールライブラリ」。GitHub 。 2021年9月5日。
^ abc ピーター・ヴァン・ウィールト;ピーター・ウィーレ;トム・シュライバース。バート・デモエン。「命令型ホスト言語の CHR」。制約処理ルール: 現在の研究トピック。スプリンガー。
^ 「CHR2からSQLへのコンバーター」。GitHub 。 2021年3月15日。
^ CHR.js - JavaScript 用の CHR トランスパイラ
^ ミランカー、ダニエル P. (1987 年 7 月 13 ～ 17 日)。「TREAT: AI 生産システム向けのより優れたマッチングアルゴリズム」(PDF)。AAAI'87 : 第 6 回全国人工知能会議の議事録。ワシントン州シアトル: 人工知能推進協会、AAAI。pp. 42 ～47。ISBN 978-0-262-51055-4。
^ レスリー・デ・コーニンク (2008)。制約処理ルールの実行制御(PDF) (博士論文)。ルーヴェンカトリック大学。 12～14ページ。
^ Duck, Gregory J.; Stuckey, Peter J.; García de la Banda, María ; Holzbaur, Christian (2004). 「制約処理ルールの洗練された操作的意味論」(PDF) .論理プログラミング. コンピュータサイエンスの講義ノート。第 3132 巻。pp. 90–104。doi : 10.1007 /978-3-540-27775-0_7。ISBN 978-3-540-22671-0. 2011年3月4日時点のオリジナル（PDF）からアーカイブ。2014年12月23日閲覧。

さらに読む

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

外部リンク

公式サイト
CHR 書誌
CHRメーリングリスト
KULeuven CHR システム
WebCHR: CHR ウェブインターフェース

[1] Thom Frühwirth.簡略化ルールの紹介。内部レポート ECRC-LP-63、ECRC ミュンヘン、ドイツ、1991 年 10 月、ワークショップ Logisches Programmieren、グーセン/ベルリン、ドイツ、1991 年 10 月およびワークショップ on Rewriting and Constraints、ダグストゥール、ドイツ、1991 年 10 月で発表。

[chrtheorypractice-2] Thom Frühwirth.制約処理ルールの理論と実践。制約論理プログラミング特集号（P. Stuckey および K. Marriott 編）、Journal of Logic Programming、Vol 37(1-3)、1998 年 10 月。doi : 10.1016/S0743-1066(98)10005-5

[3] Dahl, Veronica、J. Emilio Miralles。「Womb grammars: 文法誘導のための制約解決」制約処理ルールに関する第 9 回ワークショップの議事録。第 624 巻、技術レポート CW。2012 年。

[4] Alves、Sandra、Mário Florido。「制約処理ルールを使用した型推論」Electronic Notes in Theoretical Computer Science 64 (2002): 56-72。

[timegoesby-5] Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). 「時が経つにつれ: 制約処理ルール - 1998 年から 2007 年までの CHR 研究の調査」(PDF) .論理プログラミングの理論と実践. 10 : 1. arXiv : 0906.4474 . doi :10.1017/S1471068409990123. S2CID 11044594.

[chrbook-6] Frühwirth, Thom (2009).制約処理ルール. Cambridge University Press. ISBN 978-0521877763。

[complexity-7] Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). 「制約処理ルールの計算能力と複雑さ」(PDF) . ACM Transactions on Programming Languages and Systems . 31 (2): 1–42. doi :10.1145/1462166.1462169. S2CID 2691882.

[8] 「CHR: 制約処理ルールライブラリ」。GitHub 。 2021年9月5日。

[imperative-9] ピーター・ヴァン・ウィールト;ピーター・ウィーレ;トム・シュライバース。バート・デモエン。「命令型ホスト言語の CHR」。制約処理ルール: 現在の研究トピック。スプリンガー。

[10] 「CHR2からSQLへのコンバーター」。GitHub 。 2021年3月15日。

[11] CHR.js - JavaScript 用の CHR トランスパイラ

[12] ミランカー、ダニエル P. (1987 年 7 月 13 ～ 17 日)。「TREAT: AI 生産システム向けのより優れたマッチングアルゴリズム」(PDF)。AAAI'87 : 第 6 回全国人工知能会議の議事録。ワシントン州シアトル: 人工知能推進協会、AAAI。pp. 42 ～47。ISBN 978-0-262-51055-4。

[13] レスリー・デ・コーニンク (2008)。制約処理ルールの実行制御(PDF) (博士論文)。ルーヴェンカトリック大学。 12～14ページ。

[14] Duck, Gregory J.; Stuckey, Peter J.; García de la Banda, María ; Holzbaur, Christian (2004). 「制約処理ルールの洗練された操作的意味論」(PDF) .論理プログラミング. コンピュータサイエンスの講義ノート。第 3132 巻。pp. 90–104。doi : 10.1007 /978-3-540-27775-0_7。ISBN 978-3-540-22671-0. 2011年3月4日時点のオリジナル（PDF）からアーカイブ。2014年12月23日閲覧。