制約論理プログラミングのソースを表示

'''制約論理プログラミング'''（せいやくろんりプログラミング、{{lang-en-short|constraint logic programming}}）は[[制約プログラミング]]の一種で、[[制約充足問題|制約]]という問題表現・解決の考え方を導入することによって[[論理プログラミング]]を拡張した[[プログラミングパラダイム]]である。論理プログラミングの持っている宣言的な表現力に制約の考え方を導入し、より一般化したものとも言うことができる。

== 概要 ==
問題の対象間の関係を''制約''（例えば<code> V=I*R </code>）という形で宣言的に記述する[[制約プログラミング]]の考え方は、述語という形で関係を宣言的に記述する論理プログラミングと多くの特徴を共有している。理論的に、論理プログラミングは[[エルブランの定理|エルブラン領域(Herbrand universe)]]という有限木で表される領域上での[[ユニフィケーション]]による等号制約を扱う制約プログラミングと見なすことができ、制約論理プログラミングはその自然な拡張となっている。論理プログラミングの代表的な言語である[[Prolog]]処理系の多くには、何らかの制約論理プログラミングの機能やライブラリが用意されている。

制約論理プログラミングの応用分野は、スケジューリング、要員計画・輸送・資源割り当て、アナログ回路設計、トレーディングなどさまざまなものがある。

一般に、制約論理プログラムは[[Prolog]]などの論理プログラムと同様の形式で記述するが、''節''（clause）のボディ部に制約を含めることができる。以下の例では<code> V = I*R </code>などが制約である。手続型言語の代入文とは異なり、これらの式は関係を表現している。
<syntaxhighlight lang="prolog">
register(V,I,R) :- V = I*R.     % オームの法則
parallel_register(V,I,R1,R2) :- I1+I2=I, register(V,I1,R1), register(V,I2,R2).  % 並列回路
serial_register(V,I,R1,R2)   :- V1+V2=V, register(V1,I,R1), register(V2,I,R2).  % 直列回路
</syntaxhighlight>
例えば、上記のプログラムで<code> ?- parallel_register(50,I,10,25). </code>を実行すると<code> I = 7 </code>が結果として返る。

プログラムの実行は、論理プログラムと同じように、規則が順次呼び出されることで行われる。途中で現れた制約（例えば<code> I1+I2=I </code>）は、いったんシステム内部の''制約ストア''と呼ばれる領域に格納され、順次内部の制約評価系でより単純な形に簡約化が行われる（例えば<code> I1+I2=I & 50=I1*10 →  5+I2=I </code>）。

== 歴史 ==
制約をソフトウェアに応用する試みは、初期の対話型グラフィックシステムである''SKETCHPAD''(1963)<ref>
I. Sutherland., ''A Man-Machine Graphical Communication System''. PhD thesis, MIT, January 1963.</ref>にまでさかのぼることができる。
プログラミング言語への応用としては、Steeleらにより開発された''CONSTRAINTS''(1980)
<ref>G. Steele and  G. Sussman, ''CONSTRAINTS - A Language for Expressing Almost Hierarchical Descriptions''. Artificial Intelligence 14(1). 1980.</ref>
<ref>G. Steele, ''The Implementation and Definition of a Computer Programming Language Based on Constraints''. Ph.D. Dissertation (MIT-AI TR 595) Dept. of Electrical Engineering and Computer Science, MIT. 1980.</ref>があり、制約を変数間の関係の規則として記述し、局所制約伝播（local constraints propagation）により変数の値を順次決めていくことで、制限された範囲ではあるが制約を扱うことができた。

1972年にカルメラウアらにより開発された''[[Prolog]]''は、関係の宣言的な表現という視点を汎用プログラミング言語に持ち込むことに成功し、論理プログラミングという考え方をもたらした。しかしそれは[[エルブランの定理|エルブラン領域(Herbrand universe)]]を対象とした限定されたもので、実数や有理数など他の領域のデータの扱いは通常の関数型言語や手続型言語と変わりがなかった。Prologは、論理プログラミングの宣言的な性格を活かしつつ表現力や処理効率を上げるため、より多くの領域での一般的な制約を扱うように拡張された。カルメラウアによる''Prolog Ⅱ''(1980)<ref>
A. Colmerauer. ''Prolog-II Manuel de Reference et Modele Theorique''. Groupe Intelligence Artificelle, U. d'Aix-Marseille II. 1982.</ref>は制約という言葉を明示的に使用した最初の論理プログラミング言語である。<ref>
A. Colmerauer. ''Prolog in 10 Figures''. Proc. 8th International Joint Conference on Artificial Intelligence. 1983.</ref>
<ref name=Jaffer1994>Jaffar, J., and Maher, M.J., ''Constraint Logic Programming: A Survey''. in Journal of Logic Programming, Volume 19/20, pp.503-581, 1994</ref>
これはさらに''Prolog Ⅲ''(1987)<ref>
A. Colmerauer. ''Opening the Prolog III Universe''. BYTE Magazine. August 1987.</ref>などの制約論理プログラミング言語に発展した。
IBMのJafferやLassezらは1987年に制約論理プログラミングスキーマ''CLP(X)''を発表し<ref name=Jaffer1994></ref>、制約論理プログラミングの理論化を行った。CLP(X)に基づき実数領域の制約を扱う''CLP(R)''、有限領域を扱う''CLP(FD)''などの各種言語が開発された。また、''CHIP''(Constraint Handling In Prolog)や''CAL''など多くの制約論理プログラミング言語が開発された。また制約論理プログラミングの機能を持つProlog処理系も多数作成されている。
これらの制約論理プログラミングの研究と並行して、論理プログラミングの並行処理への応用として1980年代に研究された[[並行論理プログラミング]]も制約論理プログラミングの影響を受け、制約で並行処理を制御する[[並行制約プログラミング]]として理論化が行われた。<ref name=Saraswat1990>Saraswat, V. A., and Rinard M. ''Concurrent Constraint Programming''. In Proceedings of Seventeenth ACM Symposium on Principles of Programming Languages, January 1990</ref>

== 領域 ==
制約論理プログラミングにおける制約は何らかの特定の''領域（Domain）''に関するものである。対象とする領域ごとに制約の指定方法や処理方法は異なる。制約論理プログラミングでの一般的な領域としては、論理プログラミングの基本的な計算領域である木以外に、有限領域、ブール領域、有理数や実数などを扱う算術領域がある。

=== 木（tree） ===
論理プログラミングでは任意の有限[[木 (数学)|木]](tree)を表す''項（term）''を基本データとしているため、制約論理プログラミングでも木は基本的な計算領域として扱うことができる。[[ユニフィケーション]]による等号制約（＝）が基本的な制約である。項は以下の再帰的な定義で表される。
* 任意の定数 ''c'' は項である。
* 任意の変数 ''X'' は項である。
* 任意の関数記号 ''f'' と複数の項からなる複合項 ''f(t<sub>1</sub>, .. ,t<sub>n</sub>)'' は項である。
例えば、<code>f(X,g(a,b,h(Y))) </code>は項である。データの並びを表す[[線形リスト|リスト]]（例：<code> [1,2,3] </code>）も先頭要素と残りの要素の2つの引数からなる項の特別な表現方法と見なすことができる。

制約論理プログラミング言語のProlog Ⅲは無限木の等号制約と不等号制約を扱うことができる。
=== 有限領域 ===
有限領域（Finite Domains）は、[[有限集合]]について制約を扱う領域である。多くの[[制約充足問題]]はこの領域で表現することができる。変数の値として有限領域の要素をとるもので、特定の範囲内の整数などがその代表である。個々の変数について、例えば1から5までの整数であれば<code> X::[1..5] </code>（あるいは<code> X::[1,2,3,4,5] </code>）のように領域が指定される。数値以外であれば<code> X::[george,mary,john] </code>のような形になる。
有限領域での制約としては算術式による制約や記号的制約などが使われ、言語により指定方法は異なる。以下は古典的な[[覆面算]] SEND+MORE=MONEY を解くプログラムの例である。
<syntaxhighlight lang="prolog">
sendmore(Digits) :-
    Digits = [S,E,N,D,M,O,R,Y],        % 変数生成
    Digits :: [0..9],                  % 変数の領域を定義
    S #\= 0,                           % 制約: S, M は 0 ではない
    M #\= 0,
    alldifferent(Digits),              % 制約: 要素はそれぞれ異なった値となる
    1000*S+100*E+10*N+D + 1000*M+100*O+10*R+E
      #= 10000*M+1000*O+100*N+10*E+Y,  % 制約: SEND+MORE=MONEY
    labeling(Digits).                  % 探索開始
</syntaxhighlight>
有限領域では、制約の一貫性チェックにより各変数の取りえる領域が変化した場合、その変化を制約伝播により他の関連する変数の領域に反映し、解の範囲を順次狭めていくことで最終的な解を求めることが多い。全体の一貫性が取れなくなった場合は[[バックトラック]]を行い途中からやり直す。
=== 算術領域 ===
算術領域（Arithmetic Domain）は、''[[整数]]領域''、''[[有理数]]領域''、''[[実数]]領域''などがある。扱える制約は代数式で表される代数制約で、大きく以下の2種類に分かれる。
* [[線型]]制約　：線型代数方程式／不等式
* [[非線型]]制約：非線型代数方程式／不等式
線型制約は[[シンプレックス法]]などにより効率的に解け、多くの制約論理プログラミング言語でサポートされている。非線型制約は一般的な解法が無いため、遅延評価により非線型の式が線型になった後（例えば、<code> X*Y+Y*Y=-3 & Y=2 → 2*X+4=-3 </code>）に評価したり、代数方程式をより扱いやすくするため[[グレブナー基底#ブッフベルガーアルゴリズム|ブッフバーガーアルゴリズム]]で求めた[[グレブナー基底]]（Gröbner basis）で正規化した式で評価するなどの方法がとられる。
以下は実数領域での非線型制約を扱う制約論理プログラミング言語CLP(R)のプログラム例である。<ref name=Jaffer1987>
Jaffar J. and Lassez J. L. ''Constraint logic programming'' In Proceedings of the 14th ACM Symposium on Principles of Programming Languages, Munich. pp.111-119. ACM, January 1987.</ref>
<syntaxhighlight lang="prolog">
zmul(R1, I1, R2, I2, R3, I3) :-
    R3 = R1*R2 - I1*I2,
    I3 = R1*I2 + R2*I1.
</syntaxhighlight>
以下はプログラムの実行例で、具体的な値が求まればその値が、そうでなければ各値の方程式が結果として返る。
<syntaxhighlight lang="prolog">
?- zmul(1, 2, 3, 4, R3, I3).
  R3 = -5
  I3 = 10
  *** Yes
?- zmul(1, 2, R2, I2, R3, I3).
  I2 = 0.2*I3 - 0.4*R3
  R2 = 0.4*I3 + 0.2*R3
  *** Yes
</syntaxhighlight>
制約が矛盾しなかった場合は解と"Yes"を、矛盾すれば"No"を結果として返すが、非線型のままの制約が残ってしまいYes/Noとも判定できない場合もあり、その場合は残った制約の式と"maybe"を結果として返すようになっている。

=== ブール領域 ===
[[ブール領域]]（Boolean Domain）は真偽値の制約だけを扱う領域である。制約は一般的な[[論理演算子]]で構成される等式として表現される。制約処理方法としては、Booleの変数除去に基づいたブーリアン・ユニフィケーションやSL-導出（SL-resolution）のブール式への応用など様々なものがある。Prolog ⅢやCHIP(Constraint Handling In Prolog)などの処理系ではブール領域の制約を扱うことができる。

== セマンティック ==
制約論理プログラミングの[[公理的意味論|論理的意味]]や[[操作的意味論|操作的意味]]、[[表示的意味論|不動点意味論]]上の分析はIBMのJafferやLassezらにより与えられている<ref name=Jaffer1994></ref>。以下では操作的意味について扱う。
=== 操作的意味 ===
制約論理プログラミングを状態遷移システムとしてとらえた場合の操作的意味は状態 <math>\langle A,C,S \rangle</math> の遷移として表現できる<ref name=Jaffer1994></ref>。
<code> A </code>は[[原子論理式]]や制約の多重集合、<code> C </code>、<code> S </code>は制約の多重集合を表す。<code> C </code>と<code> S </code>とは制約を格納する制約ストアを表し、システム内部の制約評価系の処理対象となる。
<code> A </code>はまだ見えていない[[原子論理式]]や制約の集まりを表し、[[Prolog]]などの論理プログラミング言語でのゴールの集合にあたる。<code> C </code>は能動的な(利用可能な)制約の集まりで、<code> S </code>はまだ利用できない受動的な制約の集まりである。例えば、制約評価系が線型連立方程式のみを扱える場合、<code> x*y=z </code>のような非線型な式は利用できないため<code> S </code>に格納されるが、もし<code> x＝2 </code>の制約が追加された場合は線型な式<code> 2*y=z </code>に変わるため能動的な制約の集まりである<code> C </code>に格納され、制約評価系で簡約化が行われる。
実行の最初のゴール<math> G </math>は、システムの初期状態 <math>\langle G,\empty,\empty \rangle</math> で表される。[[導出]]が成功した場合、最後の状態は <math>\langle \empty,C,S \rangle</math> であり、<code> C </code>と<code> S </code>が実行結果となる。

状態遷移システムの遷移は以下のように表現できる。

* <math>\langle A \cup a,C,S \rangle \rightarrow_r \langle A \cup B,C,S \cup (a=h) \rangle</math>
:<code> A </code>内の原子論理式<code> a </code>（<math>L(t_1,\ldots,t_n)</math>）について、ルール <math>h \leftarrow B</math> があり、ヘッド部<code> h </code>（<math>L(t_1',\ldots,t_n')</math>）が変数の書き換えで同じにできる場合。この場合は原子論理式<code> a </code>を書き換える。ここで <math>\left( a=h \right)</math> は <math>t_1=t_1',\ldots,t_n=t_n'</math> を表す。
* <math>\langle A \cup a,C,S \rangle \rightarrow_r fail</math>
:原子論理式<code> a </code>を書き換え可能なルール <math>h \leftarrow B</math> がない場合。失敗（fail）する。
* <math>\langle A \cup c,C,S \rangle \rightarrow_c \langle A,C,S \cup c \rangle</math>
:<code> A </code>内に制約<code> c </code>があれば制約ストアに移動する。
* <math>\langle A,C,S \rangle \rightarrow_i \langle A,C',S'\rangle</math>
:制約ストア内の制約を制約評価系で簡約化する（<math>\left( C',S' \right) = infer \left( C,S \right)</math>）。まだ利用できない受動的な制約の集まり<code> S </code>で利用可能なものがあれば<code> C </code>に移し、利用可能な制約の集まり<code> C </code>はより単純な制約に簡約化する。
* <math>\langle A,C,S \rangle \rightarrow_s \langle A,C,S\rangle</math>
:能動的な制約の集まり<code> C </code>の一貫性チェック <math>consistent\left( C \right)</math> に問題がない場合。そのまま遷移を続ける。
* <math>\langle A,C,S \rangle \rightarrow_s fail</math>
:能動的な制約の集まり<code> C </code>の一貫性チェックが成立しない場合（<math>\neg consistent(C)</math>）。失敗（fail）する。

ここで<math>infer \left( C,S \right)</math>は制約評価の関数、<math>consistent\left( C \right)</math>は制約の一貫性チェック述語を表し、制約の領域ごとに異なる。
多くの制約論理プログラミングシステムの操作的意味は <math>\rightarrow_r \rightarrow_i \rightarrow_s</math> と <math>\rightarrow_c \rightarrow_i \rightarrow_s</math> の遷移の組み合わせで表される。

また、<code> A </code>からの原子論理式や制約の取り出しと追加は[[LIFO]]の順番に行われることが多い。この場合はPrologと同様の[[深さ優先探索]]の動作になり、途中で失敗（fail）した場合は[[バックトラッキング|バックトラック]]が行われる。

== 処理系 ==
以下に制約論理プログラミング言語の例を挙げる:
*[http://www.probp.com/ B-Prolog] （[[Prolog]]ベース、プロプライエタリ）
*[http://www.cosytec.com/production_scheduling/chip/optimization_product_chip.htm CHIP V5] （Prologベース、C++/C言語のライブラリも含む、プロプライエタリ）
*[http://clip.dia.fi.upm.es/Software/Ciao/ Ciao Prolog] （Prologベース、フリーソフトウェア: GPL/LGPL）
*[http://eclipseclp.org/ ECLiPSe] （Prologベース、オープンソース）
*[http://www.gprolog.org/ GNU Prolog]（Prologベース、フリーソフトウェア）
*[http://www.mozart-oz.org/ Mozart]（[[Oz (プログラミング言語)|Oz]]言語の処理系、フリーソフトウェア）
*[http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] （Prologベース、プロプライエタリ）
*[http://www.dcc.fc.up.pt/~vsc/Yap/index.html YAP Prolog]（Prologベース、オープンソース）
*[http://www.jipdec.or.jp/icot/ARCHIVE/Museum/IFS/abst/014-J.html CAL] （非線型代数方程式等を対象。ICOTで開発。オープンソース）
*[http://www.jipdec.or.jp/icot/ARCHIVE/Museum/IFS/abst/015-J.html CHAL] （階層制約論理型言語。ICOTで開発。オープンソース）
*[http://www.jipdec.or.jp/icot/ARCHIVE/Museum/IFS/abst/018-J.html GDCC] （並列制約論理型言語。ICOTで開発。オープンソース）
*[http://www.jipdec.or.jp/icot/ARCHIVE/Museum/IFS/abst/009-J.html Cu Prolog] （ICOTで開発。オープンソース）

== 並行制約プログラミング ==
{{ main|並行制約プログラミング }}

[[並行制約プログラミング]](Concurrent Constraint Programming)は、[[制約プログラミング|制約論理プログラミング]]の研究と[[並行論理プログラミング]]の研究とから生まれた、[[並行プログラミング]]のためのパラダイムである。並行制約プログラミングでは[[並行論理プログラミング]]をより一般化し、制約の出力(追加, tell)と入力(観測, ask)を行う複数のプロセス（エージェント）でプログラミングを行う。
並行制約プログラミングは、制約充足系（constraint solver）の記述ではなく、複数のプロセス（エージェント）の制御やプロセス間通信の記述を目的としている。

== Constraint Handling Rules ==
{{ main|Constraint Handling Rules }}

[[Constraint Handling Rules]]（CHR）は1991年にThom Frühwirthが発表した、ユーザ定義の制約が書けるように設計された[[宣言型プログラミング]]言語である<ref> Frühwirth T., ''Introducing Simplification Rules''. Internal Report ECRC-LP-63, ECRC Munich, Germany, October 1991, Presented at the Workshop Logisches Programmieren, Goosen/Berlin, Germany, October 1991 and the Workshop on Rewriting and Constraints, Dagstuhl, Germany, October 1991.</ref>
<ref>Frühwirth T., ''Theory and Practice of Constraint Handling Rules''. Special Issue on Constraint Logic Programming (P. Stuckey and K. Marriott, Eds.), Journal of Logic Programming, Vol 37(1-3), October 1998.</ref>。
多重集合の書換え規則に基づく制約処理モデルを特徴とし、ルールにより制約をより単純な制約に書き換えることで、さまざまな制約下での解を求める。CHRは[[チューリング完全]]だが<ref>Jon Sneyers, Tom Schrijvers, Bart Demoen: ''The computational power and complexity of constraint handling rules.'' ACM Trans. Program. Lang. Syst. 31(2): 2009.</ref>、
独立した言語としてではなく既存言語の拡張機能として、主に[[Prolog]]などのホスト言語上に実装されたライブラリとして提供される。
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.)

== 関連項目 ==
*[[論理プログラミング]]
*[[制約プログラミング]]
*[[並行制約プログラミング]]
*[[並行論理プログラミング]]
*[[形式手法]]
*[[プログラミングパラダイム]]

== 参考文献 ==
*Jaffar, J., and Maher, M.J., ''Constraint Logic Programming: A Survey''. in Journal of Logic Programming, Volume 19/20, pp.503-581, 1994.
*Frühwirth T, et al. ''Constraint Logic Programming An Informal Introduction''. Technical Report ECRC-93-5, ECRC. February 1993.
*相場 亮, ''[https://cir.nii.ac.jp/crid/1390564238039460480 制約論理プログラミングシステム]''. コンピュータソフトウェア, Vol.9, No.6 pp.461-473 1992.

== 脚注 ==
<div class="references-small">
<references/>
</div>

== 外部リンク ==
*[http://www.constraint.org/constraint_org.htm 制約プログラミングのページ]

{{プログラミング言語の関連項目}}

{{DEFAULTSORT:せいやくろんりふろくらみんく}}
[[Category:プログラミングパラダイム]]
[[Category:理論計算機科学]]
[[Category:形式手法]]
[[Category:数理論理学]]
[[Category:人工知能]]
[[Category:数学に関する記事]]
[[Category:論理プログラミング]]