![[PukiWiki]](image/pukiwiki.png "[PukiWiki]")
本ページ作成の目的 †上田研究室言語班ではLMNtal言語を主に研究対象としているが、これと類似点を持つ言語との比較は重要なテーマである。 宣言型プログラミング言語Constraint Handling Rules(CHR)もその一つである。 しかし2018/08/07現在、CHRにはほとんど日本語の資料が存在しない。 故に英語での読解を苦手とする学生には学ぶためのハードルが高く、研究を始める上で障害となっている。 そこでここに日本語で表記法を示し、日本語話者である初学者の参入を容易にする。 目次 †CHRとは †CHRことConstraint Handling Rulesとは、論理プログラミング、制約論理プログラミングそして、平行論理プログラミング言語を直接の祖先とする、多重集合の書き換え規則に基づく実在のプログラミング言語である。また、一階述語論理及び線形論理に基づく論文上の記述形式でもある。 CHRの特徴 †CHRは理論と実践、論理的な書き方と処理可能なコードのギャップを制約と計算可能な論理の抽象化によって橋渡しすることを試みている。制約を意識することによってCHRはデータと操作をハッキリ区別することを避け、その規則が記述に適していてかつ処理可能なものとなっている。 CHR自体も言語としての機能を備えているのだが、実際にはPrologやHaskellなどの拡張機能として、主にライブラリとして提供さされている。 CHRの起動手続き †CHRの実行時にはホスト言語においてCHRを使う宣言などのための前書きが必要とされるのだが、これについてこのページでは解説書内で解説されているPrologの場合についてのみ述べる。 Prologの場合、前書きは例えば以下に記述するような三行でなされる。 :- module(weather, [rain/0]). :- use_module(library(chr)). :- chr_constraint rain/0, wet/0, umbrella/0. これはrain,wet,umbrellaという、引数が0個の制約3つを導入する場合の宣言である。 一行目はPrologのモジュール宣言で、CHRプログラムをweatherという名前で置くものである。 このように書いた場合、モジュールは指定した制約 rain/0 しか出力しないことになる。 c/nというfunctorの宣言はc(t_1,t_2...,t_n)という制約の名前と引数の数を表しており、PrologやそのライブラリとしてのCHRにおいて制約の名前は必ず小文字から始まることになっている。 二行目は実際のCHRプログラムが読み込まれる前にCHRライブラリが読み込まれることを明確に指示するものである。 三行目は実際に使用される前に制約を宣言している場所である。CHRにおいて、制約は定義されルールで使用される前にchr_constraintというキーワードを用いて宣言されていなければならない。 最低でも名前と、引数の数だけは与えられなくてはならないが、入出力モードや引数の型はオプションとなっている。 CHRの記法 †まずCHRのコードを分解すると、CHRのコードは制約とルールで書かれている。 制約は名前と引数という二つの要素を持ち、C言語でいう関数呼び出しのように以下のような書き方をする。 name(arg1,arg2,...) これは実行時の入力に書くことも、コードに書いておくこともできる。 ルールには 単純化規則 伝播規則 単純化伝播規則 の三種類があるが、いずれもネーム、ヘッド、ガード、ボディの四つの部分にわけられ、それぞれ以下のように書く。 単純化規則 name @ head <=> guard | body. 伝播規則 name @ head ==> guard | body. 単純化伝播規則 name @ head1 \ head2 <=> guard | body. このうち、 name @ と guard | は省略が可能である。 それぞれの規則の動作についてはCHRの動作の項に記述する。 CHRの動作 †CHRが扱う制約は原子論理式（それを構成する部分論理式がない論理式、例えば変数一つ等）であり、基本的な問題ではそれを条件に沿って等価なものに書き換える（ルールが発火する）ことでより単純な制約にする。 前述のルールの動作は以下の通りである。 単純化規則 guard部に記述した条件が満たされているとき、head部に対応する制約をbody部に書き換える。 基本的な問題では、等価でより単純な制約に書き換える時に使う。 伝播規則 guard部に記述した条件が満たされており、head部に対応する制約が存在しているとき、body部を新たに追加する。 このルールは同じ制約群をhead部としては一度しか発火しない。 基本的な問題では制約としては冗長であっても、より単純な制約に書き換えるのに繋がる新たな制約を追加する時に使う。 単純化伝播規則 guard部に記述した条件が満たされており、head部に対応する制約が存在しているとき、head2部をbody部に書き換える。 他の二つの規則の組み合わせである。 用意されたルールが一つも発火しない状態になると(親言語であるSWI-Prologにとって)処理は成功した扱いになり、fail/0という制約が出力されると処理は失敗した扱いになる。なお、複数のルールが適用可能な状態になった場合、より上に記述されたものが優先されて発火する。 以下、CHRの例題を挙げてその動作を解説する。 例題1 基本的な問題 †制約 A leq B, B leq C, C leq A ルール reflexivity @ X leq X <=> true. antisymmetry @ X leq Y, Y leq X <=> X = Y. transitivity @ X leq Y, Y leq Z ==> X leq Z. idempotence @ X leq Y \ X leq Y <=> true. この問題において、制約leq/2は引数1が引数2以下であることを表す制約である。4つのルールはそのことを根拠として可能な操作である。 この問題の出力は以下のようになる。 出力 A = B, A = C. 何故このような結果になったのか、順を追って説明する。 まず、ルールtransitivityが A leq B, B leq C をhead部として発火し、制約群は以下のように変化する。 A leq B, B leq C, C leq A, A leq C. ここでルールantisymmetryが A leq C, C leq A をhead部として発火し、制約群が以下のように変化する。 A leq B, B leq C, A = C. このとき、C = A によって制約 B leq C は B leq A と等価になるため、制約群は以下のようにも解釈できることになる。 A leq B, B leq A, A = C. 従ってここでルールantisymmetryが A leq B, B leq C (= A leq B, B leq A) をhead部として発火し、制約群が以下のように変化する。 A = B, A = C. これ以上発火するルールがないためここで処理は終了し、残った単純な制約が出力される。 例題2 ナップサック問題 †CHRは前述の通り様々な言語の拡張機能として提供されているわけだが、そのために親言語の機能を利用して問題を解く場合もある。 以下はナップサック問題と呼ばれる問題を解くためのSWI-Prolog用CHRプログラムである。 :- use_module(library(chr)). :- chr_option(optimize,off). :- chr_constraint knapsack/1, labelk/0, wlimit/1, ptotalw/1, in/2, item/2, count/1, ptotalv/1, labelmem/0, listitems/1. % make domains for variables item(V,W) <=> in(item(V,W,count(0)),[0,1]). % generate auxiliary constraints etc. knapsack(WL) <=> retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(WL), ptotalw(0), ptotalv(0), listitems([]), labelk, labelmem. % if an item can't be added to the set, constrain its domain to be [0] wlimit(WL), ptotalw(TW) \ in(item(V,W, count(0)),[0,1]) <=> TW2 is TW+W, TW2 > WL | in(item(V,W,count(0)),[0]). % if an item is labeled to be added to the set, update the partial total weight wlimit(WL) \ in(item(V,W,count(0)),[1]), ptotalw(TW) <=> TW2 is TW+W, TW2 =< WL | ptotalw(TW2), in(item(V,W,count(1)),[1]). % labeling labelk \ in(item(V,W,count(0)), [0,1]) <=> member(P,[0,1]), in(item(V,W,count(0)),[P]). % calculating total value of the solution in(item(V,W,count(1)),[1]), ptotalv(TV) <=> TV2 is TV+V, in(item(V,W,count(2)),[1]), ptotalv(TV2). % listing items included in the solution in(item(V,W,count(2)),D), listitems(L) <=> in(item(V,W,count(3)),D), listitems([item(V,W) | L]). % if the current solution has a value greater than the previous ones, update the greatest value
% (and the corresponding set), print intermediate result, then backtrack
labelmem \ listitems(L), ptotalv(TV) <=>
memtotalv(TV1), TV > TV1, memlistitems(L1) |
retract(memtotalv(TV1)), asserta(memtotalv(TV)), retract(memlistitems(L1)), asserta(memlistitems(L)),
print('best set '), print(L), nl,
print('with value '), print(TV), nl, nl,
fail.
% ...otherwise just backtrack labelmem \ ptotalv(TV) <=> memtotalv(TV1), TV =< TV1 | fail. ナップサック問題とは価値と重さを持ついくつかの物品から、一定の重さまで入れられる箱になるべく価値の総計が大きくなるように物品を選んで入れる組み合わせを探す問題である。 ここで、このプログラムの以下の部分に注目してほしい。 % labeling labelk \ in(item(V,W,count(0)), [0,1]) <=> member(P,[0,1]), in(item(V,W,count(0)),[P]). この中に出てくる P という変数について説明する。 SWI-Prologの動作の話になるのだが、SWI-Prologはこのように変数名を渡された時、適当なものを探して代入(パターンマッチング)し、その場合の検討が終わったら処理前の状態に戻ってきて(バックトラック)別の適当なものを代入するという形で全ての解を網羅する、という動作をする。 今回はmember/2という関数(SWI-Prologでは述語と呼ぶ)が親言語のSWI-Prologにおいて、第一引数が第二引数のリストの要素であるときにTrueを返すという機能をもっているため、ここで言えば第二引数のリストに存在する0、または1を代入するとmember/2はTrueを返す。 よって、in/2制約の第二引数のリストにはひとまず0が代入される形でこのルールの処理が完了する。 しかし実行を続けると、このプログラムは必ずfail/0が返るようになっている。そのたびにmember/2のもう一つの解である1を代入して処理をやり直すが、結局最後までfail/0が返らない組み合わせは見つからない。つまりすべての組み合わせを試した後で、SWI-Prologは「解なし」と返答する。 CHRにバックトラックの機能はなく、以上のように親言語から提供される機能を利用してこういった問題を解くことになる。 具体的には以下のような動作をすることになる。 入力例 item(1,1), item(1,2), item(2,4), item(3,4), item(4,3), knapsack(10). まず、一番上と、上から二番目のルールによって入力された制約は整形される。 in(item(1,1,count(0)),[0,1]), in(item(1,2,count(0)),[0,1]), in(item(2,4,count(0)),[0,1]), in(item(3,4,count(0)),[0,1]), in(item(4,3,count(0)),[0,1]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(0), ptotalv(0), listitems([]), labelk, labelmem. memlistitemsやmemtotalvの引数Xは前述の通り変数で、解が見つかり次第代入される。ここではassertaの引数になったmemtotalv(0)からX=0が解の候補となる。 三番目のルールは今のところ、ptotalvの引数と重さを足してwlimitの引数より大きくなる物品がないので飛ばす。四番目のルールも第二引数が[1]のin/2制約がないので飛ばして、最初に説明した五番目のルールが発火する。第二引数が[0]のin/2制約に対応するルールはここより上にはないので、全てのin/2制約の第二引数が[0]になる。 in(item(1,1,count(0)),[0]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(0), ptotalv(0), listitems([]), labelk, labelmem. 六番目のルールは第二引数が[1]のin/2制約に対応しており、七番目のルールも第一引数の第三引数の引数が2のin/2制約に対応しているので、どちらも飛ばす。 八番目のルールはTV1にasserta(memtotalv(0))となっていたのを根拠として0が代入される。TV>TV1が満たされないため飛ばす。 結局、九番目のルールにマッチングして、failが返る。 制約には順番がないため、連続して選ばれたmember/2の解はどれが次の候補に移るか不明なのだが、SWI-Prologではどうやら一旦すべてなかったことにするらしく、以下の解についての探索が始まる。 in(item(1,1,count(0)),[1]), in(item(1,2,count(0)),[0,1]), in(item(2,4,count(0)),[0,1]), in(item(3,4,count(0)),[0,1]), in(item(4,3,count(0)),[0,1]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(0), ptotalv(0), listitems([]), labelk, labelmem. 三番目のルールは今回も発火しないため、解の候補は以下のように選択される。 in(item(1,1,count(0)),[1]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(0), ptotalv(0), listitems([]), labelk, labelmem. 今度は四番目のルールが発火し、重さ1のアイテムがナップサックに入る。さらに、このアイテムのカウンターが1になる。 in(item(1,1,count(1)),[1]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(1), ptotalv(0), listitems([]), labelk, labelmem. 続けて六番目のルールが発火し、ナップサック内の価値が1になる。アイテムのカウンターは2になる。 in(item(1,1,count(2)),[1]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(1), ptotalv(1), listitems([]), labelk, labelmem. もう入れることになっているアイテムがないので、この解を保存することになる。 七番目のルールが発火し、listitems内のリストの頭にitemが挿入される。アイテムのカウンターは3になる。 in(item(1,1,count(3)),[1]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]), retractall(memlistitems(X)), retractall(memtotalv(X)), asserta(memlistitems([])), asserta(memtotalv(0)), wlimit(10), ptotalw(1), ptotalv(1), listitems([item(1,1)]), labelk, labelmem. memtotalvの引数をptotalvの引数が上回っているので、八番目のルールが発火する。 結果、memtotalvの引数はptotalvの引数に上書きされ、asserta(memtotalv(1))とretract(memlistitems(L))制約が作成される。 そしてこれも親言語の機能であるprintによって今回ナップサックに入れた物品の組み合わせとその総価値が出力され、failが返ってバックトラックする。 これを繰り返して最高総価値は更新され続け、そのたびに物品の組み合わせが出力される。 in(item(1,1,count(0)),[0]), in(item(1,2,count(0)),[1]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]). は総価値がすでに出た1を上回らないのでリストの更新は起きず、 in(item(1,1,count(0)),[1]), in(item(1,2,count(0)),[1]), in(item(2,4,count(0)),[0]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]). では最高総価値が2に更新されて組み合わせと総価値が出力され、バックトラックする。 その次は in(item(1,1,count(0)),[1]), in(item(1,2,count(0)),[0]), in(item(2,4,count(0)),[1]), in(item(3,4,count(0)),[0]), in(item(4,3,count(0)),[0]). で最高総価値が3に更新される、という動きを辿っていくが、member/2の解を選択するとき、例えば in(item(1,1,count(0)),[1]), in(item(1,2,count(0)),[1]), in(item(2,4,count(0)),[1]), in(item(3,4,count(0)),[0,1]), in(item(4,3,count(0)),[0,1]). のように、次の解を1にするとナップサックの最大容量を超える場合には三番目のルールが発火し、member/2が実行される前にin/2の第二引数を[0]にする。 最終的にすべての組み合わせを調べ終え、そのどれもfail/0が返ったことで、SWI-Prologがnoを出力してこのプログラムの処理は終了する。 例題3 ユークリッドの互除法 †応用として、制約と全く関係ない問題も場合によっては解くことができる。 2つの自然数の最大公約数を求める問題は以下のように記述されたコードで解くことができる。アルゴリズムや動作は有名なので省略する。 制約 gcd(A), gcd(B). ※処理系にかけるときはA,Bを任意の自然数にすること ルール cleanup @ gcd(0) <=> true. gcd(N) \ gcd(M) <=> 0<N, N=<M | L is M mod N, gcd(L). 用語解説 † |
