数理解析研究所講究録1093 巻 1999 年 142-147

142

スキーママッチングにおける計算の複雑さ
山田敬三 (Keizo Yamada)平田耕– (Kouichi Hirata). 原尾政輝 (Masateru Harao)
九州工業大学情報工学部

要旨
.
$-$

階論理式に述語変数を許した式をスキー

マ (schema) という.

本論文では, スキーマと $-$階閉論理式のマッチングであるスキーママッチン
グ (schema matching), および, その判定問題であるスキーママッチング問題 (schema matching
スキーマは二階のproblem) について議論する変数である述語変数を含むので, スキ一ママッチ
そングは二階マッチングの特別な場合となる
スキーママッチングの手続きとし
こで, まず,て, 二階マッチングと同様に, 三つの書き換え規則, 簡単化 (simplificahon), 模倣 (imitation),
次に, スキーマ
射影 (projection) を定義する
マッチングを, 変数の型によって述語マッチン
matching) と項マッチング (termグ (predicate
matching) に分ける. そして, 述語マッチング問題
は表現長の線形時間で解けるが, 項マッチング問題
は完全になることを示す. -方, 個体自由変数を含まないスキーママッチング問題は, 多項式時間で解けることを示す. さらに, このアルゴリズムに$\mathrm{N}\mathrm{P}$

基づいたマッチング代入の抽出法について議論す
る.

1

はじめに

これまでに得られている知識や規則をスキー
マ (schema) として蓄え, このスキーマを援用して問題解決を行なう知識処理方式をスキーマ誘
導 (schema-guided) 処理という. このスキーマ誘導処理は、 プログラムの自動合成 [6], 数学の証明
問題 [3], プログラム変換 [12], 類推処理 [9] において広く適用されている. スキーマ誘導処理では, 援用するスキーマを決定するための操作として, マッ
チング (matchin9) が重要となる.
. マッチングとは, 与えられた二つの表現のうち,方の表現に代入を適用することで他方と –致させる操作, すなわち–方向の単–化 (un\mbox{\boldmath $\phi$}cahon)
このときの代入をマッチング代
入 (matcher) といい, マッチング代入が存在する二つの表現はマッチング可能 (matchable) であるという. また, 表現がマッチング可能か否かを判定する問題をマッチング問題 (matching problem) とのことであるいう. 項のマッチング問題の場合, 階数が 3 以下のマッチング問題は決定可能である [4] が, 二階マッ
チング問題でさえ NP 完全である [1]. また, 制

限つぎ二階マッチング問題の計算量の解析や二階マッチングの効率的アルゴリズムについての研究がなされている [2, 8, 10].
本論文では, スキーマ誘導処理におけるスキ一マを単純型理論 $[11, 12]$ を用いて定式化する. まず, 単純型理論の 標準形のうち, 抽象化を含まない二階の項をスキーマ項 (sChema term), 述語
変数を含む論理式をスキーマ (schema) として定義する
ここで, 論理式は, 論理型をもつスキー
マ項として扱われる. さらに, スキーマと自由変数を含まない $-$ 階論理式の組の有限集合をスキー
マ表現 (schema expression) といい, スキーマ項と$\beta$変数を含まないスキーマ項の組の有限集合を項表
現 (ter\tau n expression) という. 本論文では, スキー

マ表現のマッチングとマッチング問題すなわちス
キーママッチング (schema maiching) とスキーママッチング問題 (schema matching problem) について議論する.
スキーマの定義から, スキーママッチングは, 二階マッチング $[1, 12]$ の特別な場合となる. 二階
マッチングの手続きは, 簡単化 (simpl\mbox{\boldmath $\phi$}cati0n), 模
倣 (imitation), 射影 (projection) という三つの書き換え規則によって実現される [11,. 12, 13]. そこで,
本論文でも, スキーママッチングをこの三つの書き換え規則で実現する.
次に, スキ一ママッチングを, マッチングの述語マッチン
対象となる変数の型によって,matching) と項マッチング (termグ (predicate
maiching) の二つの段階に分ける. 述語マッチン
グは, スキーマ表現を項表現に変換する手続きである. 型の条件から, 述語マッチングは簡単化と模倣したがって, 述語の繰り返しとして実現できるマッチング問題は表現長の線形時間で解け, 解である項表現も –意に求まる. -方, 項マッチングは,項表現におけるマッチングであり, 簡単化, 模倣,

射影のすべての手続きを用いて実現される. 一般に, 二階マッチング問題は NP 完全である [1]. 本
論文では, 項マッチング問題も NP 完全になることを示す.. したがって, 一般に, スキーママッチン
完全となる.
グ問題は$\mathrm{N}\mathrm{P}$143
述語マッチングによって得られる項表現
関数変数の引数に関数変数が出現しな. そこで, 項表現
いような項表現となる
は,$E=\{\langle F(s_{1}^{i}, \cdots, s)in\dot{.}, f(t_{1’ m}^{i}\ldots, ti:)\rangle|i\in I\}$に対して, 各に模倣と射影の適用可能性の情報をラベルとして割り当てた既約判定
項 (reduced judgement terrn) を定義する. そして,
この既約判定項を用いることにより, 個体自由変数$f(t_{1}^{i}, \cdots,t_{m}^{i})i$を含まない項マッチング問題が多項式時間で解けることを示す. . さらに, この既約判定項を用いたマッチング代入の抽出法について議論する.

られる項とする. これは, ラムダ計算 $[11, 13]$ におと同等の表現である.
となる変数と項 $t_{i}(1\leq$$m)$ に対して,, tm/vm 丹を代{入 $(sub_{\mathit{8}tituti}on)$ という. スキーマ項
と代入
に対して,
を以下のように帰納的に定義する:(1) $t=_{C}$ のとき, $t\theta=c$ .
(2) $t=_{X}$ に対して, $t’/x\in\theta$ ならば $t\theta=t’$ であり, そうでなければ $t\theta=x$ である.
. (3) $t=f(t_{1},$$tn^{)}(f\in C)$ のとき, $t\theta=$
ける$(\lambda V_{1b}\ldots\ovalbox{\tt\small REJECT}|n\cdot t)(t_{1}\cdots tn^{)}$$\tau(v_{i})=\tau(t_{i})$$i$$t_{1}/v_{1},$

$t$

(4)
$t_{1}\theta,$$t$.
$F(t_{1},$ $\cdots,$ $tn^{)}$

$=$

(5)

$T_{0}$$\tau_{0}$$\tau_{1},$$\mu\in\tau_{0}$$\cdots,$$\tau_{n}\in T$

ならば $\tau_{1}\cross\cdots\cross\tau_{n}arrow\mu\in T$ .
$C$$\mathcal{V}$に対して.

$\cdots$$\theta$$(F \in \mathcal{V})$ならば$t\theta$

$=$

のとき,

$t’[v_{1}$$:=$であり, そうでなければ $t\theta=$, t。のである.

$t=Q_{X\cdot t’}(Q\in\{\forall, \exists\})$$Qy.((t’\{y/X\})\theta)$

である.

ただし,

のとき, $t\theta=$
は新しい変数$y$とする.

ラムダ計算 $[11, 13]$ と同様に, スキーマ
に対し
て
に現れる
の束縛変数の名前を系統的に付け換えることによってはが得られるとき,とと表す.
同値であるといい,$\Phi$と変互いに素である定数 (cOnstant) の集合
数 (variable) の可算無限集合 に対して, すべてのに対応する型 $\tau(d)\in T$ が存在すると仮定する. このとき, 項 (term) の集合
を以下のように帰納的に定義する:
かつ
(1)
のとき,
.
$\tau(d)=\tau_{1}\cross\cdots\cross\tau_{n}arrow\mu$となる(2) (適用)$d\in C\cup \mathcal{V}$と$\in \mathcal{T}(1\leq i\leq n)$ に対して,
であり, $\tau(d(t1, \cdots, tn))=\mu$ である.
と(3) (抽象) $\tau(t)=\mu\in\tau_{0}$ となる$\tau(v_{i})=\tau_{i}$となる $v_{i}\in \mathcal{V}(1\leq i\leq n)$ に対
して,
であり,
である.
特に上の (1), (2) だけから構成される項をスキー
マ項 (schema term) という. さらに, 項を二階に制を $\tau(v)\in\tau_{0}$ , まの型限するため, 変数
たは
かつ
と仮
定する.
$\neg\in C$
を論理型とする. また,$,$$\tau(\wedge)=\tau(\vee)=\tau(\supset)=\mathit{0}\cross\mathit{0}arrow\mathit{0}$とし,かつかであるとする. さらに,
$d\in C\cup \mathcal{V}$$\in$$\cdots.v_{nn}:=t\theta]$$F(t_{1}\theta,$

基本型 (elementvl type) の有限集合に対して,型 (type) の集合 $T$ をを含み次の操作についてかつ閉じている最小の集合とする:$\theta$$\cdots,$$f(t_{1}\theta, \cdots,tn\theta)$

準備$\cdots$$t\theta$$\lambda v_{1}\cdots v_{n}.t’/F$2$v_{i}$$\leq$$d$$\Phi$$\forall,$$\exists$$\Psi$$\Phi$$\Psi$$\Phi=_{\alpha}\Psi$$\alpha$$\mathcal{T}$$t\in C\cup \mathcal{V}$$\tau(t)\in\tau_{0}$$t\in \mathcal{T}$$t_{i}$$d(t_{1}, \cdots, t_{n})\in \mathcal{T}$$t\in \mathcal{T}$$\lambda v_{1}\cdots v_{n}.t\in \mathcal{T}$$\tau(\lambda v_{1}\cdots vn\cdot t)=$$\tau_{1}\cross\cdot.\cdot\cdot\cross\tau_{n}arrow\mu$$v\in \mathcal{V}$$\tau(v)$$\tau_{i}\in\dot{\tau}_{0}$$\tau(v)=\tau_{1}\wedge\cross\cdots\cross\tau_{n}arrow\mu$$o\in \mathcal{T}_{0}$$\wedge,$$\tau(\neg)=\mathit{0}arrow \mathit{0}$

つ $\tau(x)\in\tau_{0}$$\supset,$$\tau(\varphi)=\mathit{0}$ならば $\tau(Qx.\varphi)=o(Q\in\{\forall, \exists\})$であるとする. このとき, $\tau(t)=0$ となる項
理式 (fOrmula) という.となる変数$\tau(v)=\tau_{1}\cross\cdots\cross\tau_{n}arrow \mathit{0}$

$t$

を諭

$\cross\tau_{n}arrow\tau$$v\in \mathcal{V}$$\tau\neq \mathit{0}$$\Phi,$$\varphi,$$\psi,$$\Psi,$$\cdots$$\cdots*$$\lambda v_{1}\cdots v_{n}.t$

スキーママッチング

スキーマ表現と項表現を合わせて単に表表現
現 (expression) というを $E$ の大き$i\in I\}$ に対して,さ (size) といい, $|E|$ と表す. ただし, 項の大きさ
は, その項に出現する (補助記号を除く) 記号の数とする.
表現 $E=\{\langle\Phi_{i,\varphi i}\rangle|i\in I\}$ に対して, 任意の $i\in I$ でとなる代入 を求める操
作を, スキーママッチング (sChema matching) とを $E$ のマッチング代いう.
そのような代入入 (matcher) という. 表現 $E$ にマッチング代入が$E=\{\langle\Phi_{i\backslash }.\varphi_{i}\rangle$$|$$\Sigma_{i\in I}(|\Phi_{i}|+|\varphi_{i}|)$$\Phi_{i}\theta=_{\alpha}\varphi_{i}$$\theta$$\theta$

存在するとき, $E$ はマッチング可能 (matchable) であるという. また, 表現がマッチング可能か否かを判定する問題をスキーママッチング問題 (schema
matching problem) という.
二階マッチングの手続きは, 簡単化 (simplification), 模倣 (imitation), 射影 (projection) の三つの書き換え規則によって実現できる [ . そこで,
本論文でも, スキーママッチングの手続きを三つの書き換え規則で実現する.
スキーママッチングの簡単化では, Qx.t $(Q\in$を に書き換える. そこで, に出現するを論理束縛記号 (w,で表す) という特別な個体定数で置き換える. また, 二階マッチング[12] の模倣では, 束縛変数を模倣することはできな
い. そこで, スキーママッチングの模倣でも, 論理
束縛記号の模倣ができないように定義する. さらを後で使えるようにするたに, Qx.t の模倣では,めに, 述語変数の引数を –つ増やす.
$12_{\lrcorner}^{\rceil}$$v\in \mathcal{V}$を述語変数 (predicate variable) といい, $\tau(v)=\tau 1\cross$
$.:$
かつ
となる変数
を関数
変数 (function variable) という. 述語変数を含み,
関数変数を含まない論理式をスキーマ (schema) とい L
以後 スキーマを,-階論理式を, 述語変数を $P,$ $Q,$ $R,$ , 関数変数を$F,$ $G,$ $H,$
関数定数を $f,$ $g,$ $h,$で表す.と項となる項 $t_{i}(1\leq$$i\leq n)$ に対して, $t[v_{1} :=t1, \cdots, v_{nn}:=t]$ で,中の変数賜 をちで同時に置き換えることによって得.

3$\cdots$$\cdots$$\cdots$$\tau(v_{i})=\mathcal{T}(t_{i})$$t$$\{\forall, \exists\})$

$t$

$t$

$w_{1},$ $w_{2},$ $\cdots$

$x$

$x$

144
ただし,

1. 簡単化 (simplification):$\{\langle_{C,C}\rangle\}\cup E$$\Rightarrow E(C\in C)$,$\theta_{1}=\{\lambda v_{1^{\neg}1}.P(v_{1})/P\}$$\cup E(n\geq 1, f\in C)$,$\theta_{4}=\{\lambda v1v_{2}.v_{1}/H_{1}\}$$\cup\{\langle\Phi\{w/x\}, \varphi\{w/y\}\rangle\}$$E$$=\forall u.(P(u)\{\lambda v_{1}.\neg\forall y.p(v1, y)/P\})$

かつ $c\neq w$ のとき,

$E\{\lambda\overline{v}.f(H1(v1, \cdots,v_{n})$...,$(\forall z.P(_{Z}))\{\lambda v1^{\neg\forall y}..P(v1, y)/P\}$,$\langle F(_{S_{1},\cdots,S_{n}}), c\rangle\in E$$E\Rightarrow$,とする.
したがって, $E$ のマッチング代入は,$\{\lambda v_{1}.\neg\forall y.p(v_{1}, y)/P\}$ となる.
実際,.

に関する模倣 (imitation):の $F$$E\Rightarrow E\{\lambda\overline{v}.c/F\}$,$\theta_{5}=\{\lambda v_{1}v_{2}.v_{2}/H_{2}\}$$(Q\in\{\forall, \exists\})$$\Rightarrow(E-\{\langle Qx.\Phi, Qy.\varphi\rangle\})$2.

,$\theta_{3}=\{\lambda v1v2\cdot p(H1(v_{1}, v_{2}), H_{2}(v_{1}, v_{2}))/P_{1}’\}$$\Rightarrow\{\langle_{S_{1},t_{1}}\rangle, \cdot\cdot‘, \langle sn’ t_{n}\rangle\}$$\{\langle\dot{Q}x.\Phi, Qy.\varphi\rangle\}\cup E$,$\theta_{2}=\{\lambda v_{1\cdot y.()}\forall P1\prime v_{1}, y/P_{1}\}$$\{\langle f(s_{1}, \cdots, sn), f.(t1, \mathrm{a}\cdot\cdot,tn)\rangle\}\cup E$$=\forall u.((\neg\forall y.p(v1, y))[v_{1} :=u])$,$=\forall u.\neg\forall y.p(u, y)$$H_{m}(v_{1}, \cdots, v_{n}))/F\}$,となる. また, この例から, 限量子の模倣において引数を増やす必要があることがわかる.

$\langle F(S_{1}, \cdots, Sn), f(t1, \cdots, tm)\rangle$$\in E(n\geq 0, m\geq 1)$,

かつ $\tau(F(S1, \cdots, sn))$$=\tau(f(t_{1}, \cdots, t_{m}))$のとき,$E\Rightarrow E\mathrm{f}^{\lambda}\overline{v}.QX.P(v_{1}, \cdots, vn’ X)/F\}$,

4

スキーママッチング問題の計算量$\langle F(s_{1}, \cdots, S_{n}), Qx.\varphi\rangle\in E(Q\in\{\forall, \exists\})$

かつ $\tau(F(S1, \cdots, Sn))=\tau(QX.\varphi)$ のとき.

3.

$E$

の $F$

に関する射影 (projection):$E\Rightarrow E\{\lambda\overline{v}.v_{i}/F\}$,$\langle F(_{S_{1},\cdots,s_{n}}), t\rangle\in E(n\geq 1,1\leq i\leq n)$

かつ $\tau(S_{i})=\tau(t)(1\leq i\leq n)$ のとき.

と表す. このとき, 二階マッの推移閉包をチング [12] と同様に, 以下の定理が成り立つ:$\Rightarrow^{*}$$\Rightarrow$定理 1 表現 $E$ がマッチング可能であるごとと,となることは同値である.
$E\Rightarrow^{*}\emptyset$

本論文では, スキーママッチングを, 対象となる変数が述語変数か関数変数かの違いによって, 述語マッチングと項マッチングの二つの段階に分けて考える.
述語マッチング (predicate matching) とは, 与えられたスキーマ表現に対して, それに述語変数および述語定数が現れなくなるまで, 模倣と簡単化を適用する手続きである. 述語マッチングには, 射影が適用できない. なぜならば, スキーマ表現 $E$ に対とする. このとき,して$\tau(P(s_{1,n}\ldots, S))=\tau(\varphi)=\mathit{0}$ となるが,は項となるからである. したがって,なので以下の補題が成り立つ :$\langle P(s_{1}, \cdots, s_{n}), \varphi\rangle\in E$$s_{i}$$\tau(s_{i})\neq \mathit{0}$例 1 表現 $E=\{\langle\forall x.P(X),\forall Z^{\neg(\forall}.y.P(z, y)\rangle\}$ に対するスキーママッチングは以下のようになる:(簡単 4y$\{\langle\forall x.P(X),\forall z.\neg(\forall y.p(z, y)))\}$$\Rightarrow\{\langle P(w1), \neg\forall y.p(w1, y)\rangle\}$

(模倣
(模倣

ある.

$\theta_{2}$

)

(簡単化)

$\Rightarrow\{\langle\forall y.P_{1}l(w1, y),\forall y.p(w1,y)\rangle\}$$\Rightarrow\{\langle P_{1(}’w1,w_{2}),p(w1, w_{2})\rangle\}$)(簡単 iy$\Rightarrow\{\langle\neg P_{1}(w1), \neg\forall y.p\{w1, y)\rangle\}$$\Rightarrow\{\langle P_{1}(w_{1}),\forall y.p(w1,y)\rangle\}$$\theta_{1}$(模倣$\theta_{3}$)$\Rightarrow\{\langle p(H_{1}(w1,W2), H_{2}(w1, W2)),p(w1, W_{2})\rangle\}$$\Rightarrow\{\langle H_{1}(w_{!}, w2), w1\rangle, \langle H_{2(}w1, w2),w2\rangle\}$$\theta_{4}$スキーマ表現は, 述語マッチングによって, 論理
束縛記号を含む項表現に変換される. このようにして得られた項表現に対するマッチングが項マッ
チング (term matching) となる. 項マッチングでしたは, 簡単化と模倣以外に射影も適用されるがって, 項マッチング問題は, 関数変数の引数に関数変数は出現しないような項表現に対する二階

(簡単化)

(射影

補題 1 スキーマ表現 $E$ の述語マッチング問題は$O(|E|)$ 時間で解け, その解である項表現も –意で)マッチング問題となる. 項マッチング問題に対して, 次の定理が成り立つ :定理 2 項マッチング問題は NP 完全である.

$\Rightarrow\{\langle w_{1},w1\rangle, \langle H2(a, w\iota, w2),w2\rangle\}$.

(射影$\theta_{5}$)$\Rightarrow\{\langle w1,w_{1}\rangle, \langle w2, w_{2}\rangle\}$$\Rightarrow^{*}\emptyset$.

(簡単 4y証明項マッチング問題が NP に属することは, 二階マッチング問題の NP 完全性 [1] より明らか.
完全性は, 項マッチング問題の MONOTONE -1N33SAT からの還元による. 口
$1$

145
したがって, 一般に、 スキーママッチング問題は完全となる.

$\mathrm{N}\mathrm{P}$のラベル付き頭部 (labeled head)を以下のように定義する: $T=c^{P}$ または $T=*^{P}$ のとき$\tau=f^{P}(t1, \cdots, t_{n})$ のとき$1\mathrm{h}\mathrm{d}(T)$$1\mathrm{h}\mathrm{d}(T)=$$\mathrm{l}\mathrm{h}\mathrm{d}(\tau)=\tau\backslash ,$$f^{P}$

5.

個体自由変数を含まないスキーママッチ
定義 2 項表現

ング

に対して,
の
に関する判定項をとし,$T$ (, si) とする. このとき, {, si) $|i\in I$ } の共通判定項 (COmmon judgement( si))を次のように定義する.
(1) 任意の $i\in I$ に対して,( $T$ ( , si)) $=$は個体定数か ) ならば, ロ, $\in IT$ ( , si) $=$$=$$\mathrm{h}\mathrm{d}(s_{i})$$\{\langle s_{i}.t_{i}\rangle | i \in I\}$$F$

$t_{i}$$s_{i}.\cdot$$T(t_{i}$$t_{i}$

定理 2 では, 個体自由変数の存在が証明の本質である. そこで本節では, 個体自由変数を含まないような項表現の項マッチング問題が多項式時間で解けることを示す. ここでのアイデアは, 述語マッチン

{

.( .

$*$

$t_{i}$$i\in lic$$f(t^{i}1’\cdots,$ $t_{m}i)i\rangle|i\in I$(2) 任意の $i\in I$ に対して,の各
情報をラベルとして割り当てることにある.
$f(t_{\mathrm{J}’ m}^{i}\ldots, t^{i})i$$T(t_{i}, si)=f^{P_{i}}(t_{1}^{i}, \cdots, t_{m}^{\dot{?}})$

ならば,$\text{口_{}i\in I}T(t_{i}, si)=f^{\bigcap_{i\in Ii}}P(\text{口_{}i\in I}\tau(t_{1}^{i}, S_{i}),$

定義 1
をスキーマ項 $H(s\iota, \cdots, s_{n}),$ を変数を含まないスキーマ項とする. また, $P(t)=\{i|t=$
si $(1\leq i\leq n)\}$ とする. このとき, の に関する判定項 (judgement term) $T(.t, s)$ を, 以下のようにラベル付けられた項と定義する. ここで,は新しい個体定数とする.
が論理束縛記号 $w$ のとき, $T(w, s)$ $=$
$t$

$s$

$t$

$\text{口_{}i\in I}\tau$(3)$1\mathrm{h}\mathrm{d}(T(ti, si))=f_{i}^{P}$“$s$$\mathrm{h}\mathrm{d}(T(tj, s\cdot i))$$t$$*^{Pw)}(1)$.

(2) が佃体定数 のとき, $\tau(C, s)=c^{P(\dot{c})}$ .
の(3) $t=f.(t_{1}.\cdots, t_{m})$ であり,に関する判定項が $T_{i}(t_{i,s})(1\leq i\leq m)$ のとき, $T(t, 6)=$$c$$\cdots,$

例 2 スキーマ項
スキーマ項 ,
$t_{1}$$T_{m}(tm’ s))$$s_{1},$$t_{2},$ $t_{3}$$t^{i}m$$)$$\mathrm{h}\mathrm{d}(T(tk, s_{k}))\neq$$\Pi_{i\in I}\tau(t_{i}, si)=*^{\mathrm{n}P}i\in fi$.

例 3 例 2 の判定乱 $T$ ( , si) $(i\in\{1,2,3\})$ に対して, $\{T(t_{1}, s_{1}), \tau(t2, S2)\}$ と $\{T(t_{2}, s_{2}), T(t3, s3)\}$の共通判定\Phi( , si) と.si)はそれぞれ以下のようになる:$t_{i}$$t_{i}$$\text{口_{}i\in\{.\}}1_{\backslash }2T$$\text{口_{}i\in\{3}2,\}^{T(}t_{i}$$\text{口_{}i\in\{2}1,\}\tau(t_{i\cdot S_{i}})=f^{\emptyset}(*\{2\}, f\emptyset(*\{3\}, *\{1\}))$.

$\text{口_{}i\in^{f}\iota^{2}’ 3}\}\tau(t_{i,s}i)=f^{\emptyset 2}(*\{\}, f\emptyset(a^{\emptyset\emptyset}, *))$

および変数を含まないを以下のように定義する:$s_{2,3}s$$s_{2}=H(w_{2}, g(w_{2}, a, b), a)$

定\Leftrightar ow . 3 項表現 $E=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ に対して,とする. このとき, $E$ の既約判定
項 (reduced judgement terrn) 口 E を,
( , si)$\mathrm{h}\mathrm{d}(s_{i})=F$$\Pi_{i\in I}T$

$t_{3}=f(f(a, w_{1}),$ $f(a, w_{2}))$

このとき,

の

かっ

が存在するとき,
換える.

,

.

例4例2の

に関する判定項$\{1,2,3\})$ は以下のようになる:$t_{i}$$t’$$t_{i}$$f\emptyset(t_{1}’, \cdots, t’)m$,$t_{2}=f(g(w2, a, b), f(a, w_{2}))$$s_{i}$$t_{i}$に以下の規則を可能な限り適用して得られるラベ
ル付き項とする:$=$( , si) の部分項
に対して,

,

$s_{3}=H(w1, f(a, w1), b)(=s_{1})$ ,$t_{1}=f(f(a, w_{1}),$ $f(b,w_{1}))$,.

$\text{口_{}i\in I}T$

$s_{1}=H(w1, f(a, w1), b)$ ,,, si) .

$s$$t_{i}$$f^{P(t)}(T_{1}(t_{1}, s),$かつ($\cdots$となる $k,j\in I$ が存在するとき,

$*$

$t$

$t_{i},$$ti$$1\mathrm{h}\mathrm{d}$s)ii’}に模倣と射影の適用可能性の$\langle F(s_{1’}^{i}\ldots,$$\text{口_{}i\in I}T$$c^{\cap P}C^{P_{i}}$グで得られた項表現$E=$$ter7\gamma\iota$$T$( , si) $(i\in$$t_{i}$$t_{i}’=*\emptyset$$\lceil\urcorner_{i\in I}\tau$と$s_{i}$$\{\langle s_{1}, t_{1}\rangle, \langle s_{2},t_{2}\rangle\}$すると, 例 3 より
となる.
口 E2

,

$t’$

となる $i(1\leq i\leq m)$
$t’$
を
で置き

( , si) 中の
$ti$

に対して,

$t_{i}$$=$$E_{2}$$*\emptyset$$=$$E_{1}$$\{\langle S_{2}, t_{2}\rangle, \langle s_{3}, t_{3}\rangle\}$と$\text{口}E_{1}=f^{\emptyset}(*\{2\}, f\emptyset(*\{3\}, *\{1\}))$,$=*\emptyset$$T(t_{1,S_{1}})=.f^{\emptyset}(f^{\{}2\}(a\emptyset,\{\iota*.\}), f^{\emptyset}(b^{\{3\}\{}, *\})1)$$T(t_{2}, s_{2})=f\emptyset(g^{\{\}}(2\{*\}, a^{\{}\}, b^{\emptyset}13)$$f^{\emptyset}(a^{\{\}}, *\{1\})3)$

,

,

,

$T(t_{3}, s_{3})=f\emptyset(f\{2\}(a*\{1\})\emptyset,, f\emptyset(a*)\emptyset,\emptyset)$.

補題 2 項表現 $E=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ に対して,
このとき, ロ E は
si $=F(s_{1}^{i}, \cdots, S_{m})i$ とする$O(|E|^{2})$ 時間で構成できる.

に対して, $T(t, S)$ は( , si)
時間で構成できるので,は $O(|E|^{2})$ 時間で構成できる.
また, 定義 2 より,
となる
さら
mfin
口 i\in I $T(t_{ii}, s)|$$O(|$
( , si) からに, 定義 3 より,
は,口,\in I
$T(t_{i,s_{i}})|)$ 時間で構成できる.
したがって, ロ E は$E$ から $O(|E|^{2})$ 時間で構成できる. 口
証明 スキーマ項

判定項のラベルは, その位置において射影が適用できる引数を表しており, もしラベルが であるなら
ば, その位置には射影は適用できない.
を以下のようスキーマ項 の頭部 (head)のとき $\mathrm{h}\mathrm{d}(t)=t;t=$に定義する:$f(t_{1}, \cdots, t_{n})$ のとき. 同様に, 判定項 $T$$\emptyset$$t$$\mathrm{h}\mathrm{d}(t)$$t\in C\cup \mathcal{V}$$\mathrm{h}\mathrm{d}(t)=f$

$s$

と

$t$

$O(|s|\cross|t|)$$|$$\text{口_{}i\in I}T$$\leq$$\text{口}E$$i\in I\{|t_{i}|\}$$\text{口_{}i\in I}T$

$t_{i}$$t_{i}$

146
補題 3 項表現 $E=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ に対して,$si=F(s_{1}^{i}, \cdots, S)in$ とする.
このとき, $E$ がマッチであることは同ング可能であることと, 口 E
値である.

とする. このとき, ロ E を用いてマッ
チング代入を抽出する.

$F(s_{1}^{i}., \cdots, s_{n}^{j})$$\neq*\emptyset$

定義 4 項表現 $E=\{\langle S_{i}, t_{i}\rangle|i\in I\}$ に対して,とする. ロ Eのとき,を以下のように帰納的にの項集合 (term set)
定義する:
(1) ロ E $=*^{P}$ のとき,.
$si=F(s_{1}^{i}, \cdots, S)in$

証明 $(arrow)$ 補題の対偶に対する口 E の構造に関する帰納法による. $(arrow)$ は明らか. 口$\neq*\emptyset$$\text{口}E$$T_{\ulcorner 1E}$$\tau_{\mathrm{n}E}=\{\lambda\overline{v}.v_{j}|j\in P\}$

定理 3 個体自由変数を含まないスキーマ表現 $E$のスキーママッチング問題は $O(|E|^{2})$ 時間で解ける.

(2) ロ E $=c^{P}$ のとぎ、$\tau_{\lceil\urcorner E}=\mathrm{f}\lambda\overline{v}.c\}\cup \mathrm{t}\lambda\overline{v}.v_{j}|j\in P\}$(3) ロ E$=f^{P}(\text{口}E_{1}, \cdots, \text{口}E_{m})$

.

のとき,

$\tau_{\mathrm{n}E}=\{\lambda\overline{v}.f(t1\cdot\cdots,t_{m})|\lambda\overline{v}.t_{i}\in\tau_{\mathrm{n}E_{i}}\}$

証明 $E$ に対して, 以下のような手続き Match を考える:Procedure Mat

815 例 2$\mathrm{c}\mathrm{h}(E)$;do begin;;$\{\langle s_{1}, t_{1}\rangle\},$$E_{1}:=\mathrm{P}\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{N}\mathrm{a}\mathrm{t}(E)$whileselect$E_{1}\neq\emptyset$$\cup\{\lambda\overline{v}.v_{j}|j\in P\}$の$s_{1},$ $s_{2},$ $t_{1},$

.

に対して,
とすると, 例 2 より

$E_{2}’=\{\langle s_{2},t_{2}\rangle\}$$\text{口}E_{1}^{;}=f^{\emptyset}(f^{\{2}\}(a^{\emptyset,\{\}}, *)1,$$=$$E_{1}’$$t_{2}$,$f\emptyset(b^{\{3\}}, *\{1\}))$$\text{口}E_{2}’=f\emptyset(g2\{\}(*\{1\}, a\{3\}, b\emptyset), f\emptyset(a\{3\}, *‘ \mathrm{t}1\}))$$\langle s, t\rangle\in E_{1}$となるので,$F:=\mathrm{h}\mathrm{d}(s)$$E_{2}:=\{\langle t, s\rangle\in E_{1}|\mathrm{h}\mathrm{d}(S)=F\}$,$\tau_{\mathrm{n}E_{1}}$と, は以下のようになる.

$\tau_{\mathrm{n}E_{2}}$;$T:=\text{口}E_{2;}$

if

then
return “not matchable” and halt;$T=*\emptyset$$\}$$\tau_{\mathrm{n}E_{1}}’=\{\lambda v_{1}\lambda v\lambda v_{1}\lambda v_{1}v_{2}1vv_{2}vv_{2}2vvv_{3}3\cdot.\cdot f33.f(f(v_{2}2,ff((f(a, v_{1})v,f(f(a,v1)(v3,’, v1b,v1))f(vf(b),),3’ v_{1}’)v_{1}))),$,

enreturn “matchable”;$d$$\lambda v_{1}v_{2^{V_{3}}}.f(v2, f(v3, v_{1}))$

ここで, PredMat
ある.
は個体自由変数を含まない項
よって,
表現となる
したがって, 補題 3 より, Match $(E)$が “matchable” と返すことと, $E$ がマッチング可能であることは同値である
また, 補題 1 より,
PredMat $(E)$ の計算時間は $O(|E|)$ である. さらを構成するための計算時間は高々 $O(|E|)$に,である. $E_{2}=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ とすると,を構成するための計算時間は, 補題 2 より $O(|E_{2}|^{2})$となる.
の異なる関数変数の数をとし, そをの関数変数によってと分割$E_{1}^{j}(1\leq
j\leq
k)$
する. それぞれのが上のに対応する. したがって, Match $(E)$ の計算時間
は, $O(|E|)+\Sigma_{j=1}^{k}O(|E_{1}^{J}|^{2})’\leq O((|E_{1}^{1}|+\cdots+$$|E_{1}^{k}|)^{2})\leq O(|E|^{2})$ となる. 口
$(E)$

は

$E$

の述語マッチングで$\lambda v_{1}v_{2}v_{3}.f(v_{2}, f(a, v1))$$E_{1}$$\tau_{\mathrm{n}E_{2}’}=\{$$E_{2}$$\text{口}E_{2}$$E_{1}$,$\lambda v_{1}v_{2}v_{3\cdot f}(g(v_{1}, v3, b), f(v3, v_{1}))$$\lambda v_{1}v_{2}v_{3}.f(g(v_{1}, v3, b), f(a, v_{1}))$,$\lambda v_{1}v_{2}v_{3}.f(g(v1, a, b), f(v3, v1))$

,

また,

例4の

$E_{2}$$f^{\emptyset}(*\{2\}, f\emptyset(*\{3\}, *\{1\}))$$\{\lambda\overline{v_{3}}.f(v2, f(v3, v_{1}))\}$に対して,となるので,$\text{口}E_{2}$$\tau_{\mathrm{n}E_{2}}$となる.

$E_{1}^{1}\cup\cdots\cup E_{1}^{k}$$E_{2}$

定理 4 項表現 $E=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ に対して,なとする. このとき, ロ E
らば, 代入 $\theta\in\{\{t/F\}|t\in\tau_{\mathrm{n}E}\}$ は $E$ のマッチ
ング代入となる.

$s_{i}=F(s_{1}^{i}, \cdots, S)in$$\neq*\emptyset$

定理 4 を用いることにより, 以下のような

6,$(\lambda v_{1}v_{2}v3\cdot f(g(v1, a, b), f(a, v_{1}))$$k$$E_{1}$,

マッチング代入の抽出

前節では, 与えられたスキーマ表現にマッチング代
入が存在するか\searrow というスキーママッチング問題を考察した. -方, 二階マッチングおよび本論文のス
キーママッチングでは, マッチング代入が存在しても, それが–意とは限らない [12]. そこで本節では, 個体自由変数を含まないスキーマ表現におけるマッチング代入の抽出法について議論する.
手続き Match と同様に, 述語マッチングで得られた項表現を関数変数によって分割して考える.
項表現 $E=\{\langle s_{i}, t_{i}\rangle|i\in I\}$ に対して, si
$=$

の

$E$

マッチング代入の抽出法を与えることができる: 項
表現 $E=\{\langle s_{i}, t_{i}\rangle |i\in I\}$ に対して, si $=$とする.
$E$の模倣優先 (imiiation-first) マッチング代
入は, 以下のように定義される単 $-$ 要素項集合に対して, $\{t/F\}$ となるマッチング代
入である:$F(s_{1,\prime}^{i}\ldots\backslash S^{\tilde{\iota}})n$$T_{\lceil\urcorner E}^{I}=\{t\}$(1) ロ E $=*^{P}$ のとき,$\tau_{\Pi E}^{I}=\{\lambda\overline{v}.v_{j}|j=\min\{k|k\in P\}.\}$

(2)
のとき,
.
(3) ロ E $=f^{P}$ (, ロ Em) のとき,$\text{口}E=c^{P}$.

$\tau_{\Pi E}^{I}=\{\lambda\overline{v}.c\}$$\text{口}E_{1},$$\cdots$$T_{\mathrm{n}E}^{I}=\{\lambda\overline{v}.f(t_{1}, \cdots, t_{m})|\lambda\overline{v}.t_{i}\in\tau_{\mathrm{n}E_{i}}^{I}\}$

.

147
$E$
の最左射影優先 (lefl-most p 吻 ection-fiirst)
マッチング代入は, 以下のように定義される単–要素項集合に対して、 $\{t/F\}$ となるマッ
チング代入である:(1) $\text{口}E=*^{P}$ のとき,

[3] Donat. M. R. and Wallen, L. A.: Learning andapplying generalized solutions using higher orderresolution, Proc. 9th International Conference
on Automated Deduction, LNCS 310, 41-60,$T_{\mathrm{n}E}^{L}\mathrm{p}=\{t\}$$T_{\cap E}^{LP}= \{\lambda\overline{v}.v_{j}|j=\min\{k|k\in P\}\}$(2) それ以外のとき,$P\neq\emptyset$,[5] Farmer, W. M.: Simple second-order languages
for which unification is undecidable, TheoreticalComputer Science 87, 25-41, 1991.
[6] Flener, P.: Logic program synthesisf.rom incomplete information, Kluwer Academic Press,
1995.
[7] Garey, M. R. and Johnson, D. S.: Computers
and intractability: A guide to the theory of NPcompleteness, W. H. Freeman and Company,

ならば

(a)
(b) 口 E$\text{口}E=c^{P}$.

[4] Dowek, G.: Third order matching is decidable,
Proc. 7th Annual IEEE Symposium on Logic in
Computer Science, 2-10, 1992.

.

ならば$T_{\cap E}^{LP}=\{\lambda\overline{v}.v_{j}|j=\mathrm{m}\mathrm{i}11\{k|k\in P\}\}$$P=\emptyset$

1988.

のとき,

,
のとき,

$T_{\mathrm{n}E}^{LP}=\{\lambda\overline{v}.c\}$$=f^{P}(^{\text{口}E_{1}}, \cdots, \text{口}E_{m})$$T_{\cap E}^{L}\mathrm{p}\{=\lambda\overline{v}.f(t1\cdot\cdots, t_{m})|\lambda\overline{v}.t_{i}\in\tau_{\lceil\urcorner}^{L}\mathrm{p}_{i}\}E$

.

例6例5の
に対する模倣優先マッチング
代入はそれぞれ $\{\lambda\overline{v_{3}}.f(f(a, v_{1}), f(b, v_{1}))/H\}$ ,$E_{1}’,$ $E_{2}’$$\mathrm{f}^{\lambda\overline{v_{3}}}\cdot f(g(v_{1}, a, b), f(a, v_{1}))/H\}$, となる .

$-$ 方

1979.

,

[8] 原尾, 岩沼 : 高階ユニフィケーションアルゴリズムの複雑さについて, 日本ソフトウェア科学会論文誌
8, 41-53, 1991.

’ の最左射影マッチング代入は共に$E_{1}’,$ $E_{2}$$\{\lambda\overline{v_{3}}.f(v2, f(v_{3}, v_{1}))/H\}$

7

となる.

[9] Harao, M.: Proof discovery in $LK$ system byanalogy, Proc. 3rd Asian Computing Science
Conference, LNCS 1345, 197-211, 1997.

おわりに

本論文では, スキーマと 階閉論理式マッチングであるスキーママッチングについて考察した. まず,スキーママッチングの手続きを, 簡単化, 模倣, 射影という三つの書き換え規則で実現した. そして,スキーママッチング問題が–般に NP 完全になる
ことを示した. さらに, 個体自由変数を含まない
スキーママッチング問題は, スキーマ表現 $E$ に対
して $O(|E|^{2})$ 時間で解けることを示した. さらに,
このスキーママッチングにおけるマッチング代入の抽出についても議論した.
本論文の結果は, スキーマ誘導知識処理 [6], 特に
類推 [9] におけるマッチングが多項式時間で解けることを示唆している. 本論文の手法を用いて, 類推システムを構築することは今後の課題である. また, どのようなマッチング代入を抽出すべきか, という問題も今後の課題である.
スキーママッチングにおいて, 複数存在するマッ
チング代入のうち, どのマッチング代入を利用するかの基準を導入することも今後の課題である. さらに, マッチング代入が–意に存在する, もしくは,すべてのマッチング代入が多項式時間で求まるよ–

うなスキーマの特徴づけも今後の課題である.
謝辞 本研究の–部は, 文部省科学研究補助金萌芽的研究 10878055, 基盤 (C) 07680405, および柏森情報科学振興財団の助成金によるものである.
参考文献[1] Baxter, L. D.: The complexity of unification,
Doctoral Thesis, Department of Computer Science, University of Waterloo, 1977.
[2] Curien, R., Qian, Z. and Shi, H.: Efficientsecond-order matching, Proc. of the 7th International Conference on Rewriting Techniques andApplications, LNCS 1103, 317-331, 1996.

[$10_{\rfloor}^{\rceil}$

Hirata, K., Yamada, K. and Harao, M.:
Tractable and intractable second-order matchingproblems, 情報基礎理論ワークショップ予稿集 16, 1998.

[11] Huet, G. P.: A unification algorithm for typed-calculus, Theoretical Computer Science 1, 27$\lambda$

57, 1975.

[12] Huet, G. P. and Lang, B.: Proving and applying program transformations expressed withsecond-order patterns, Acta Informatica 11, 3155, 1978.
[13] Snyder, W. and Gallier, J.: Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation 8, 101140, 1989.