区間制約処理

区間制約処理は各リテラルに、従来の真理値(true,false の二値)に替えて区間制約情報(順序付き非負整数の有限領域)を付加すること で、多値論理系の推論を実現する機構を提供するものである。

区間制約情報付きリテラル(以下、制約リテラルと略す)は、以下の形式により 表現される。

1. extraval制約　：　S = ]I,J[ = {i ∈ N | i < I or i > J}
2. interval制約　：　S = [I,J] = {i ∈ N | I<=i<=J}

制約リテラルの制約部における異なる引数はそれぞれ異なる(有限)領域を持つ と想定するので、制約処理を行うためには、プログラムが述語の制約部の 定義域を知る必要がある。したがって、ルール集合には、 以下のような述語宣言が含まれなければならない。 述語宣言は以下のような形式である。

各々の制約リテラルは、リテラル部分p(t_1,...,t_r)と制約部分 #S_1,...,S_m#の２つの部分から構成される。r,mは0の場合があり 得る。前者は制約情報付き命題の場合、後者は制約リテラルとしての宣言をし ない述語の場合である。したがって、全ての一階述語論理プログラムは 制約プログラムである。

● 拡張解釈の必要性

区間制約情報を付加したIV-MGTPの利点として、まず各種の多値論理問題に対 する記述能力が増加することが挙げられる。さらに重要な点として、前件での 連言照合操作あるいは証明の多分岐によって大きな負荷となり得る、全体とし てのモデル(候補)数を減少させることにより、速度の面から見た推論性能の向 上が図れることである。

しかし、一方で、制約付きのリテラルをモデルとしてどのように 解釈するかという問題がある。たとえば、p(1)#[1,2],[3,4]# という 制約リテラルは、制約部を通常の選言として表現した場合には、4つの 要素を持つ選言となり、通常の意味論においてはモデルとはなり得ず、 分岐を生じなければならない。しかし、制約リテラルとしては、上記のような リテラルも含めてモデルと考えたいので、ここで意味論を拡張する必要性が 生じる。

●拡張解釈による制約ルールの形式的意味論と充足可能性判定手続き

ここで、基本的なモデル生成アルゴリズムにおける解釈の概念を拡張する。 通常の一階述語論理における解釈は、 エルブラン解釈に基づくものであり、基底項から真理値 trueあるいは false への写像である。これに対し、制約リテラルに対する解釈とは、基底項から、 真理値空間(有順序の非負整数有限領域で表される)の部分集合への写像を表す。 これを拡張解釈と呼ぶ。

述語pの制約部はfunctionalなものであり、したがって制約部が同じものは 拡張解釈I(p)について真でなければならない。pの制約部が #N1,...,Nm# と宣言された場合、項の変数t_1,...,t_rそれぞれに対 し、< t_1,...,t_r,c_1,...,c_m > ∈ I(p)であるよ うな値のタプルc_1 ∈ N_1,...,c_m ∈ N_mが最低一つ存在する。

解釈の概念を拡張したのに従い、充足可能性の概念にも若干の拡張を加える。 拡張解釈Iは、I(F) ⊆ Sのとき区間制約情報Sをもつ基底 リテラル Fを(拡張)充足すると言える。

入力となる制約ルールの充足可能性は以下のように判定される。

• 基底リテラルL=p(t_1,...,t_r)#S_1,...,S_m#が解釈Iにより充足される (I ⊃ L)
  iff ∈ I(p)であるような c_1∈ S_1,...,c_m ∈ S_mが存在する。
• 基底リテラルの集合Mが充足される iff 各々のL ∈ MについてI ⊃ L
• 基底ルールがIにより充足される
  iff ルールの前件の少なくとも１つのリテラルがIにより充足されない。 あるいは後件の少なくとも１つのリテラルがIにより充足される。
• 非基底ルールrがIにより充足される iff 任意の代入 σに対しI ⊃ rσ
• 制約プログラムが充足される iff 任意のr ∈ Pに対しI ⊃ r

通常の照合機能においては、項の部分の照合(すなわち、ルールの前件部が 現在のモデル候補において充足されているか否かの判定)を行うが、 制約ルールにおいてはこの判定は必要条件に過ぎない。 すなわち、照合の処理として、項の部分の処理に加えて、 制約部の照合処理を追加しなければならない。

制約部の照合処理を以下の表に示す。

ここで、S_k は前件部に現れるリテラルの制約部、 条件中に現れる M(p)^S は、モデル候補中で管理されている 述語 p の制約部 S を表すもので、M(p)^S_min, M(p)^S_max は その(区間)制約における最小値と最大値をそれぞれ表すものである。 また、i,j は基底化された制約表現を表し、 I,J はそれぞれ変数による制約表現であることを示している。

前件リテラルL_1=p({1,2})，L_2=p([I,4])，L_3=p(]I,J[)を考える。 L_1について、{1,2}のEVリスト表現は <]3,6[>である。 <]2,2[,]5,6[> とintersectionをとると、 <]2,6[>であるので、条件は失敗する。L_2については、 M(p)^S_{max}=4 <= 4を得るので、条件は充足され、結果の代入は I <- M(p)^S_max=1となる。最後に、L_3については、二つの代 入{I <- 2,J <- 2}および {I <- 5,J <- 6}が可能である。

● 項メモリの拡張

項メモリでは、制約付きリテラルを管理しなければならないので、 項メモリの構成、処理方式にも拡張が必要である。

具体的には、以下の機能が必要である。

1. 項の構造として、制約部を追加し、制約情報を管理する。
2. 各制約部は、分岐時に書き換えられていくので、分岐時の 情報を保存しておくために、Activation cell (A-セル)情報を 項に付加された A-セル情報とは別に付加しておく必要がある。 また、書き換えられた制約情報をすべて保存しておかなければ ならない。
3. 照合時には、単に項メモリに登録されているかのみでなく、 制約部の充足可能性も判定する。
4. 登録時は、通常、項の部分を新規に登録するか、または A-セル情報を on にする処理となるが、 加えて、制約情報間の積により、新しい制約情報を生成し、 登録することが必要である。

制約プログラムに対する基本的な推論アルゴリズムはMGTPで提供される ものと相違ない。したがって、基本的な処理の流れについては、MGTP に委ねることができる。 ただし、処理の各過程における連言照合、包摂テスト、簡約化、反駁、 ならびに項メモリの管理、参照のプロセスにおいて、制約部分の処理が 追加されなければならない。 これらは項の定義に基づいて、制約部が定義されているものについては、 項の部分の処理に追加して、制約部の処理を行うものとする。

包摂テスト、簡約化、反駁の各プロセスについては、以下でその機能を まとめることとする。

● 制約間演算処理

制約間演算処理としては以下の2つが必要である。 ここで、制約間演算処理を行う2つの制約部をそれぞれ

1. 充足判定処理 C_1^i が C_2^i を充足するとは、C_2^i の表す領域が C_1^iの表す領域に包含されることをいう。 C_1のすべての制約要素がC_2^iの対応する制約要素を充足するとき、 C_1 は C_2^iを充足するという。
2. 積計算処理 C_1^i と C_2^i の積は、領域としての重なりを表す制約要素である。 これらの直積をもって、 C_1 と C_2 の積とする。

包摂検査のタスクは、現在のモデル候補にそれ以上制約を加えないような(冗 長な)拡張段階を避けるためにある。

生成された後件部の 項部分がモデル候補により包摂され、かつ制約部が対応するモデル候補の 制約部に包摂されるならば、その後件部の制約情報を新たに モデル候補として登録しない。

制約部を持つ項(後件部)の包摂判定は以下の手続きによる。

1. 生成された後件部の項部分がモデル候補により包摂されるか。 もし包摂されなければ false を返す。 すなわち、後件部を新しく項メモリに登録する。
2. 項部分がモデル候補により包摂されない場合、制約部が 対応するモデル候補の制約部に包摂されるか。 もし、包摂されなければ false を返す。 すなわち、後件部の制約部分とモデル候補の制約部分の 積をもってモデル候補の制約部分を書き換える。
3. 制約部が対応するモデル候補の制約部に包摂される場合、 その後件部は包摂されたものとし、true を返す。 すなわち、後件部はモデル候補として新たに登録されない。

制約リテラルでは、文法上負リテラルとしての記述を許していない。 負リテラルは、制約リテラルとして記述可能だからである。 従って、反駁テストは、与えられた後件部の項部分と一致する モデル候補に対して、制約部の反駁テストを行えば良いことになる。 制約部の反駁テストは、 反駁テストは制約部の積が空になるときをもって反駁されるとする。

【例】
後件部として p(1)#[1,2]# が生成され、 モデル候補に p(1)#]1,2[# がすでに登録されていたとする。 このとき、#[1,2]# と #]1,2[# の積は空であるから、後件部 p(1)#[1,2]#は反駁される。

● 簡約化

簡約化処理は、反駁手続きの選言への拡張である。 すなわち、後件部として、選言が生成され、その選言要素が モデル候補によって反駁されるならば、選言要素から削除する。同時に 各選言要素の制約部をモデル候補の対応する項の制約部との積に 置き換える。ただし、反駁による簡約化を除けば後者の処理は 処理効率上は影響を与えない。後者の処理は、モデル拡張節の選択 ヒューリスティックスとして、制約領域の最も狭いものを選択する という戦略をとる場合には有効となるが、通常は単位節として取り出された時のみ 書換えを行なえは、十分であり、これは前述した 包摂検査により実現される。

簡約化の処理手続きを以下に示す。

1. 生成された帰結部としての選言C_1,...,C_n の各要素 C_i (1 <= i) に 対して以下の処理を行う。 C_i がモデル候補により(制約リテラルとして)反駁されるか。 もし反駁されるならば、C_i を選言から取り除く。
2. もし反駁されないならば、C_i の制約部をモデル候補の 対応する項の制約部との積に書き換える。
3. この手続きをC_i (1 <= i)に対して繰り返し、選言の長さが 0 に なったときは、失敗した枝として、探索を終了する。また、選言の長さが 1 に なったときは、単位節として、登録を行い、選言バッファから削除する。