Constraint Handling Rules

Constraint Handling Rules（CHR）は1991年にThom Frühwirthが発表した、ユーザ定義の制約が書けるように設計された宣言型プログラミング言語である^{[1] [2]}。 多重集合の書き換え規則に基づく制約処理モデルを特徴とし、ルールにより制約をより単純な制約に書き換えることで、様々な制約下での解を求める。CHRはチューリング完全だが^[3]、 独立した言語としてではなく既存言語の拡張機能として、主にPrologなどのホスト言語上に実装されたライブラリとして提供される。 CHRの典型的な応用分野はアブダクションなどの推論サービス、マルチエージェントシステム、自然言語処理、スケジューリング、型システム、ソフトウェアのテストと診断、セマンティックウェブなどである。

Constraint Handling Rules

パラダイム	並行制約プログラミング、制約論理プログラミング
登場時期	1991年
設計者	Thom Frühwirth
型付け	動的型付け
主な処理系	Prolog (SICStus Prolog、SWI Prolog、XSB Prolog、YAP Prolog、ECLiPSe Prolog、TinyCHRなど)、Java (JCK、JCHR)、Haskell (HaskellCHR、CCHR)
影響を受けた言語	Prolog、Concurrent Prolog、GHC
影響を与えた言語	LMNtal
プラットフォーム	クロスプラットフォーム

■カテゴリ / ■テンプレート

概要

Constraint Handling Rules（CHR）はコミッテッドチョイス（committed-choice）型並行制約プログラミング言語で、ガード付き書換え規則により、原子論理式（制約）をより単純なものに書き換える。 CHRは元々制約充足系（constraint solver）の記述のために開発されたが、高水準の汎用の並行制約プログラミング言語としても用いられるようになってきた^[4]。

CHRの特徴は以下の通りである。

• 頭部に制約の多重集合が書ける
• 多重集合書換えに基づく言語の中では強力
• 多くの応用プログラムがある

CHRは単純化規則（Simplification rule）と伝播規則（Propagation rule）、およびそれらの組み合わせである単純化伝播規則（"Simpagation" rule）からなる。

単純化規則（Simplification rule）は、複数の制約を論理的に等価なより単純な制約に変換する。(例えば、X≦Y, Y≦X ⇔ X=Y. や X≦X ⇔ true.)

伝播規則（Propagation rule）は、論理的には冗長だが単純化に結び付くような制約を新しく追加する。(例えば、X≦Y, Y≦Z ⇒ X≦Z.)

これらの規則の組み合わせることにより、例えば A≦B, B≦C, C≦A は A=B, A=C に単純化される。

それぞれの規則は以下の形式で記述する。ヘッド(H) にマッチした要素がガード(G) の制約を満たすときにヘッドをボディ(B) に書き換える。ガード部がない（条件が"true"のみの）場合ガード部とその後のコミット演算子"|"は省略できる。RuleNameはルール名で、続く"@"と共に用いられ、省略可能である。

• 単純化規則（Simplification rule）

RuleName @ H1, ..., Hi ⇔ G1, ..., Gj| B1, ..., Bk .

ヘッドH₁, ...,H_iを除去して, ボディB₁, ..., B_kを生成する。

• 伝播規則（Propagation rule）

RuleName @ H1, ..., Hi ⇒ G1, ..., Gj| B1, ..., Bk .

ヘッドH₁, ..., H_iを残したまま, ボディB₁, ..., B_kを生成する。

• 単純化伝播規則（Simpagation rule）

RuleName @ H1, ..., Hh\ Hh+1, ..., Hi ⇔ G1, ..., Gj| B1, ..., Bk .

ヘッドH_h+1, ..., H_iを除去して, ボディB₁, ..., B_kを生成する。

以下に順序集合を表す二項関係"≦"の制約を扱う、SWI-Prolog上での4つのCHRの規則からなるプログラムの例を示す。"%"以降はコメントを表す。

:- use_module(library(chr)).
:- op(500, xfx, leq).
:- chr_constraint leq/2.
% X leq Y は変数Xが変数Yに対しless-or-equalの関係であることを示す
 
reflexivity  @ X leq X <=> true.                  % 反射律
antisymmetry @ X leq Y , Y leq X <=> X=Y.         % 半対称律
idempotence  @ X leq Y \ X leq Y <=> true.        % 冪等性
transitivity @ X leq Y , Y leq Z ==> X leq Z.     % 推移律

これらの使い方は、たとえば

?- X leq Y, Y leq Z, Z leq X.
Y = X,
Z = X.
yes

といった具合である。

歴史

CHRの直接の祖先は、論理プログラミング、制約論理プログラミング、および並行論理プログラミングである^[4]。 1970年代初めに生まれた論理プログラミングの考え方は、その宣言的な性格を活かしつつより表現力を大きくするため、一般的な制約を扱うように拡張された制約論理プログラミングとなった。Prolog Ⅱ(1980)、Prolog Ⅲ(1987)、CHIPやCLP(X)など様々な言語が作成された。 それと並行して、1980年頃に論理プログラミングのプロセス的解釈をもとに論理プログラミングの考え方を並行プログラミングに応用する並行論理プログラミングの考え方が生まれ、ガード付きコマンドの考えに基づいたガード付きホーン節で並行実行の制御や通信を行うShapiroのConcurrent Prolog（1983）や上田によるGHC (1985)などの様々なプログラミング言語や各種のプログラミングテクニックが開発された。Thom Frühwirthは1991年に並行論理プログラミングでの考え方と意味論を制約論理プログラミングに応用して単純で表現力の高い言語としてまとめ上げ、また理論的な解析を行った。

実装

CHRは、Prolog、Haskell、Javaなどの各ホスト言語上で実装されている。

Prologは最も一般的なホスト言語で、SICStus PrologやSWI Prolog、XSB Prolog、YAP Prolog、ECLiPSe Prologなど多くの処理系上のライブラリとしてサポートされている。Java上ではJava Constraint Kit(JCK)やJCHR(Java Constraint Handling Rules)のライブラリがあり、Javaから呼び出して使うことができる。Haskell上ではHaskell CHRやCCHRなどのライブラリがある。

合流性

合流性（Confluence）とは、書き換えが可能な部分式が複数存在する際に、どの書き換え規則をどの部分式に適用して書き換えたとしても最終的な結果が合流する(一意に定まる) という性質のことである。合流性の無いプログラムは、最終的な実行結果が実行ごとに異なる可能性がある。一般的な項書き換えシステムと同様、停止性を持つCHRプログラムの合流性には、決定可能な必要条件と十分条件がある^[5]。停止性と合流性を持つCHRプログラムはルールの適応順序によらない一貫性のある論理的な意味を持ち、解くべき問題の異なった部分に対してルールを並列に適用できるような、並行してインクリメンタルに問題を解くアルゴリズムをインプリメントできる^[4]。

プログラム例

CHRのプログラム例を示す。

最大公約数

ユークリッドの互除法を用いて最大公約数を求めるプログラムの例を示す。

% 最大公約数
gcd(0) <=> true.
gcd(N), gcd(M) <=> 0<N, N=<M | L is M mod N, gcd(N), gcd(L).

素数

エラストテネスのふるいにより素数を求めるプログラムの例を示す。generate0/1の2つのルールはprime(2)、...、prime(N)のデータを生成し、siftルールは素数のみを選び出す。generate0/1ルールとsiftルールは(もし必要であれば)並行して実行することも可能である。

% エラストテネスのふるい
generate0 @ prime(N) <=> N=<2 | fail.
generate1 @ prime(N) ==> N> 2 | M is N-1, prime(M).
sift      @ prime(X), prime(Y) <=> Y mod X =:= 0 | prime(X).

フィボナッチ数

フィボナッチ数を求めるプログラムの例を示す。トップダウンにもボトムアップにも求めることができる。

% フィボナッチ数をボトムアップに評価
f0-1 @ upto(_) ==> fib(0,1), fib(1,1).
fn   @ upto(Max), fib(N1,M1), fib(N2,M2) ==> Max>N2, N2=:=N1+1 | 
            N is N2+1, M is M1+M2, fib(N,M).

% フィボナッチ数をトップダウンに評価
f0 @ fib(0,M) <=> M=1.
f1 @ fib(1,M) <=> M=1.
fn @ fib(N,M) <=> N>=2 | 
        N1 is N-1, N2 is N-2, fib(N1,M1), fib(N2,M2), M is M1+M2.