技術的概要：等号を含む第一階および第二階の依存関係における目標指向クエリ応答

1. 問題定義

データベースにおける依存関係は、整合性制約の表現、データの不完全性の処理、スキーマ変換の指定に用いられる。第一階の依存関係（タプル生成依存関係（TGDs）や等号生成依存関係（EGDs）など）は標準的であるが、特定のスキーママッピングのクラスを合成して表現するためには、第二階（SO）依存関係が必要となる。等号原子を後件に追加することで、SO 依存関係は表現力の高いスキーママッピングの合成を表現可能にする。

このような依存関係に対するクエリ応答の標準的なアプローチは、chase アルゴリズムの変種を用いて普遍モデルを計算することである。しかし、このアプローチには重大な限界がある：

1. 非効率性：完全な普遍モデルの計算は、特定のクエリとは無関係な推論を大量に生成することが多い。
2. スケーラビリティ：データが頻繁に変化する場合、完全な chase の再計算は実質的に不可能なほど高コストとなる。
3. 等号の複雑性：既存の目標指向技術（Magic Sets など）は、等号や関数変数を含む依存関係に直面すると困難に陥る。等号を明示的に公理化する（合同性と関数反射性公理を使用する）単純なアプローチは、冗長な推論の増殖により非効率的な推論と非終端の不動点計算を引き起こす。

本論文は、不要な推論を回避しつつ、正しさと終端性を保証する、等号を含む第一階および第二階の依存関係に対する効率的な目標指向クエリ応答技術の開発という未解決の問題に取り組む。

2. 手法

著者は、入力依存関係を変換し、その後の chase 計算がクエリに応答しながら無関係な推論を最小化するアプローチを提案する。この技術は、7 つの主要なステップからなるパイプライン（アルゴリズム 1）として実装されている。

2.1 第二階量化の除去

入力 SO 依存関係 $\Sigma$ は、第二階量化子を削除し、関数変数を関数記号に変換することで、第一階（FO）式集合（$\Sigma_1$）に変換される。この変換はクエリ応答を保存するため、後続のステップは関数記号を伴うものの、第一階論理の枠組み内で動作できる。

2.2 単一化（Singularisation）

完全な合同公理のオーバーヘッドなしに等号を効率的に処理するため、著者は Marnette の研究を拡張した単一化の新しい変種を適用する。

• メカニズム：この技術は依存関係の本体を修正して冗長な推論を「剪定」する。等号を持つ項間で事実をコピーするために合同公理を使用する代わりに、依存関係を書き換えて等号を介して原子を明示的に結合させる。
• 先行研究の修正：著者は、ten Cate らによる先行する定式化における関数反射性（$a \approx b$ ならば $f(a) \approx f(b)$ という性質）に関する不完全性を特定した。完全な関数反射性公理を単純に追加すると非終端を引き起こす。
• 解決策：著者はD 制限付き関数反射性公理を導入する。これらの公理は、関係的事実（領域述語 $D$ によって追跡される）に現れる項に対してのみ等号を導出する。これにより、すべての関連するクエリ応答を保存しつつ、普遍モデルが有限に保たれることが保証される。

2.3 スコレーム化

FO 依存関係は、存在量化子をスコレーム関数記号に置き換えることで論理プログラム（$P_3$）に変換される。重要なのは、元の SO 依存関係からの「真の」関数記号とスコレーム記号との区別を維持することである。関数反射性公理は真の関数記号にのみ適用され、スコレーム項に対する無限の導出を防ぐ。

2.4 関連性分析

後方連鎖技術を用いて、明らかにクエリ応答に寄与しないルール全体を排除する。

• 抽象化：基本インスタンスは、各述語に対して代表定数を含むより小さな「クリティカルインスタンス」に抽象化される。
• 分析：この抽象インスタンス上のプログラムの不動点が計算される。抽象インスタンスで発火できないルールは無関係とみなされ、除去される。
• 最適化：アルゴリズムは、等号原子が関係原子や領域ルールから導出されることが多いという事実を利用し、すべての潜在的な一致に対して反射性ルールを考慮する必要を回避する。

2.5 Magic Sets 変換

残りのルールに対して、Magic Setsアルゴリズムの変種を適用し、無関係なルールインスタンス（ルール全体ではなく）を剪定する。

• 装飾：述語は、横方向の情報伝達をシミュレートするために、「束縛（bound, b）」または「自由（free, f）」のマーカで装飾される。
• 等号の処理：この変換は、等号述語を対称的に扱い、さもなければすべての述語をトリガーする反射性ルールの処理を回避することで、等号に対して最適化されている。
• 終端性：著者は、元の chase が終端する場合、魔法述語の導入にもかかわらず、変換されたプログラムの不動点も終端することを証明する。

2.6 本体における定数と関数記号の除去

Magic Sets 変換は、標準的な chase 変種が処理できない関数項をルール本体に導入する可能性がある。著者は、本体の定数と関数項を新しい変数と補助述語（$F_f$）に置き換える変換（defun）を適用し、本体に項を埋め込むことなく関数適用を公理化する。

2.7 単一化の解除

最後に、単一化中に導入された等号は、変数をその等しい項に置換することでルール本体から除去される。これにより、本体に等号、定数、関数記号を含まない「安全な」論理プログラム（$P_7$）が生成され、効率的な評価に備える。

2.8 最終評価

最終プログラム $P_7$ は、等号を「真の」等号として扱う（関数適用を追跡するために $V_f$ 述語を使用する）chase 変種を用いて評価されるが、スコレーム記号に対して関数反射性を強制しない。これにより、最終段階は効率的となり、明示的な等号公理化のオーバーヘッドに悩まされない。

3. 主要な貢献

1. 等号を含む SO 依存関係に対する最初の目標指向技術：本論文は、等号を含む一般化された第二階依存関係に対する目標指向クエリ応答を可能にする最初の技術を提示する。
2. 改訂された単一化：関数変数を処理し、非終端を引き起こさずに関数反射性に対処することで完全性を保証する、修正および拡張された単一化技術。
3. 等号のための関連性分析：普遍モデルの抽象化を計算することで無関係な依存関係を特定する新しい分析技術。等号が存在する場合でもクエリ応答に寄与できないルールを効果的にフィルタリングする。
4. 最適化された Magic Sets：対称性を活用し、通常オーバーヘッドの源となる反射性ルールの処理を回避することで、等号を効率的に処理する Magic Sets の変種。
5. ベンチマーク生成：この分野の既存のベンチマークの欠如に対処し、非自明な推論を示すことが保証された合成第二階依存関係とデータセットを生成する新しい技術。
6. 実装と評価：等号を含む第二階依存関係に対する chase の最初の実装と、広範な実証的評価。

4. 実験結果

著者は、Java でプロトタイプを実装し、不動点計算に RDFox システムを利用した。アプローチは以下のベンチマークで評価された：

• 第一階ベンチマーク：Benedikt らからの標準データセット（LUBM、Deep、Ont）。
• 第二階ベンチマーク：同ツールによって生成された新しい合成データセット（Gen-26、Gen-27、Gen-28）。

主要な知見：

• パフォーマンス向上：目標指向クエリ応答は、完全な普遍モデルを計算するよりも桁違いに高速である場合がある。いくつかのケース（例：Deep300 シナリオ）では、完全な chase は時間制限内で終端しなかったが、目標指向アプローチはすべてのクエリに正常に応答した。
• 技術比較：
  • 関連性分析は、派生事実の数を大幅に削減することが多く、パフォーマンス向上の主要な要因として特定された。
  • Magic Setsは、特に関連性分析と組み合わせた場合に追加の利益を提供したが、いくつかのケース（例：Ont-256）では、魔法ルールのオーバーヘッドが利益を上回ることがあった。
  • 第二階のオーバーヘッド：第二階依存関係の場合、関数適用のための事実生成（$F_f$ 述語を介して）のオーバーヘッドは顕著であった。関連性分析は、これらの事実を生成する必要がある項の数を削減するため、特に効果的であった。
• 事実の削減：これらの技術は、完全な chase と比較して、「有用な」派生事実の数を、多くの場合桁単位で大幅に削減した。

5. 意義と主張

本論文は、マッピングの合成が等号を含む複雑な第二階依存関係をもたらすことが多いデータ統合およびスキーママッピング合成における重要なボトルネックを解決すると主張する。目標指向技術がこの複雑な設定に適応可能であることを実証することで、著者は以下の点を示している：

• 完全な普遍モデルの計算に伴う「次元の呪い」を回避することが可能である。
• 単一化、関連性分析、Magic Sets の組み合わせは、等号と関数変数の特定の課題を処理するための堅牢な枠組みを提供する。
• 従来の手法が失敗する大規模な合成ベンチマークを正常に処理できたという事実は、このアプローチが実用的であることを示している。

著者は将来の作業について慎重であり、終端しない chase シナリオ（ガード付き依存関係など）へのこれらの技術の拡張や、補助事実（$D$ や $F_f$ 述語など）のオーバーヘッドのさらなる削減が、依然として未解決の課題であると指摘している。