(57)【要約】【課題】スキーママッピングの合成を容易にするシステムを提供すること。【解決手段】２つのスキーマ間の制約や関数の逆など、１つまたは両方のマッピングが関数でないより広いクラスのマッピングを合成するための一般的アルゴリズムが提供される。合成コンポーネントが、異種のデータソースのスキーママッピングに合成を行い、スキーママッピングは、完全従属性、局所従属性、および２次従属性の少なくとも１つで表すことができ、２次従属性は、ソースからターゲットへの形式である必要はない。合成のアルゴリズムはさらに、合成アルゴリズムが終了するかどうかをテストする手順を含む。【選択図】図１
2006172436.tif 000002
【特許請求の範囲】
【請求項１】
データマッピングを容易にするシステムであって、
演繹手順を用いて入力スキーママッピングを合成して、合成マッピングに出現する必要があるすべての制約の有限の公理化を得る合成コンポーネント
を備えることを特徴とするシステム。
【請求項２】
前記演繹手順は、分解を含む完全な演繹手順であることを特徴とする請求項１に記載のシステム。
【請求項３】
前記演繹手順は、終了と正しい結果の生成が確認されることを特徴とする請求項１に記載のシステム。
【請求項４】
前記入力スキーママッピングは、局所従属性で表され、Ｓｋｏｌｅｍｉｚｅされて、２次従属性で表されるスキーママッピングを得ることを特徴とする請求項１に記載のシステム。
【請求項５】
前記公理化は、ｄｅＳｋｏｌｅｍｉｚｅされて１次の制約で表されるスキーママッピングを得る、有限の２次公理化を含むことを特徴とする請求項１に記載のシステム。
【請求項６】
局所従属性で表される前記入力スキーママッピングは、Ｓｋｏｌｅｍｉｚｅされて、２次従属性で表される中間スキーママッピングを得ることを特徴とする請求項１に記載のシステム。
【請求項７】
前記中間スキーママッピングを与える制約から演繹されることができる入力署名および出力署名に対するすべての制約について有限の公理化が計算されることを特徴とする請求項６に記載のシステム。
【請求項８】
確認が行われて、形式φ（ｚ），Ｒ（ｙ）→Ｒ（ｘ）の制約が、
φ（ｚ）はＳ1∪Ｓ3に対するアトムの連接であり、
｛ｘ｝⊆｛ｗ｝でφ（ｚ）にアトムＲ（ｗ）はなく、
｛ｘ｝は｛ｙ｝の部分集合でなく、かつ
ＲはスキーマＳ2の関係記号である
ように、前記有限の公理化に出現するかどうかを確認することを特徴とする請求項１に記載のシステム。
【請求項９】
前記入力スキーママッピングが第１の手順を用いて合成されるように、第１の手順が、ドメイン演算子と範囲演算子の少なくとも１つを計算することを特徴とする請求項１に記載のシステム。
【請求項１０】
前記演繹手順は、３つ以上のマッピングの連続を合成する際に、前記入力スキーママッピングに存在するすべての制約に対して実質的に同時に行われることを特徴とする請求項１に記載のシステム。
【請求項１１】
請求項１に記載のコンポーネントが記憶されたことを特徴とするコンピュータ可読媒体。
【請求項１２】
前記スキーママッピングは、完全従属性、局所従属性、および２次従属性の少なくとも１つで表され、前記２次従属性は、ソースからターゲットへの形式である必要はないことを特徴とする請求項１に記載のシステム。
【請求項１３】
データをマッピングする方法であって、
演繹手順を用いて、合成マッピングに出現する必要のあるすべての制約の有限の公理化を得ることにより、合成コンポーネントとともに入力スキーママッピングを合成すること
を備えることを特徴とする方法。
【請求項１４】
有限の２次の公理化をｄｅＳｋｏｌｅｍｉｚｅして、１次の制約で表されるスキーママッピングを得ることをさらに備えることを特徴とする請求項１３に記載の方法。
【請求項１５】
前記有限の公理化をｄｅＳｋｏｌｅｍｉｚｅする行為はさらに、２次従属性をアンネストするステップを備えることを特徴とする請求項１４に記載の方法。
【請求項１６】
前記有限の公理化をｄｅＳｋｏｌｅｍｉｚｅする行為はさらに、同じ関数記号を含むすべての項が統合されるように、制約中の変数をリネームするステップを備えることを特徴とする請求項１４に記載の方法。
【請求項１７】
すべての制約の対を考慮することにより前記変数をリネームすることをさらに備え、前記リネームは、多項式時間で行われることができることを特徴とする請求項１６に記載の方法。
【請求項１８】
前記有限の公理化をｄｅＳｋｏｌｅｍｉｚｅする行為はさらに、Ｓｋｏｌｅｍ項に結び付けられた変数を含むアトムを除去することを備えることを特徴とする請求項１４に記載の方法。
【請求項１９】
局所従属性で表される前記入力スキーママッピングをＳｋｏｌｅｍｉｚｅして、２次従属性で表される中間スキーママッピングを得る行為と、
前記中間スキーママッピングを与える制約から演繹することができる入力署名および出力署名に対するすべての制約の有限の公理化を計算する行為と、
前記有限の公理化をｄｅＳｋｏｌｅｍｉｚｅして、局所従属性で表されるスキーママッピングを得る行為と
をさらに備えることを特徴とする請求項１３に記載の方法。
【請求項２０】
データマッピングを容易にするシステムであって、
演繹手順を用いて、合成マッピングに出現する必要のあるすべての制約の有限の公理化を得ることにより、合成コンポーネントとともに入力スキーママッピングを合成する手段と、
局所従属性で表される前記入力スキーママッピングをＳｋｏｌｅｍｉｚｅして、２次従属性で表されるスキーママッピングを得る手段と、
有限の２次公理化をｄｅＳｋｏｌｅｍｉｚｅして、１次従属性で表されるスキーママッピングを得る手段と
を備えることを特徴とするシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、データベーススキーマ間の、既存のマッピングから構成されるマッピングを合成するシステムおよび方法に関する。
【背景技術】
【０００２】
インターネットなどの世界規模の通信ネットワークの到来で、多量のデータへのアクセスが容易になった。世界中に情報源があるが、多くの場合、データは、情報源ごとに異なる形で表される。今日有線および無線の制度で優勢となっている情報の自由な流れは、使用のためにデータを記憶し、解釈することに関する限りは、供給源と行き先との間に互換性があることを要求する。今日企業および個人が直面する大きな問題の１つは、あるモデル／スキーマで存在するデータに、別のモデル／スキーマを介してアクセスする必要性である。しかし、そのようなプロセスは、互いと大きく異なり、変化し続けるモデル／スキーマのセットによって阻まれている。そのような例はデータの保管に見られ、データの保管では、記憶と、他のソースからの迅速なアクセスのために、多くの異なる供給源からデータが受け取られる。あるモデルから別のモデルにデータを変換することは、時間を要し、多くのリソースを必要とするだけでなく、変換問題がからむ可能性もある。
【０００３】
スキーママッピングは、異種のデータソース間の関係を明らかにし、データの変換、データ交換、スキーマの展開、継続的な確認、および他の作業を支援するために使用される。マッピングの合成は、スキーマＡ、Ｂ、Ｃ間の２つのマッピングｍａｐABとｍａｐBC入力として受け取り、組み合わせられたマッピングｍａｐABとｍａｐBCによって与えられる、ＡとＣの間の同じ制約のセットを指定する１つのマッピングｍａｐACを生成する動作である。
【０００４】
マッピング合成の使用を具体的に説明するために、次のようなスキーマ展開シナリオを考えられたい。Ｓ1、Ｓ2、Ｓ3、Ｓ4が、ある製品の連続した発売で使用されるスキーマのバージョンであるとする。マッピングｍａｐ12を使用して、スキーマＳ1のフォーマットからスキーマＳ2のフォーマットにデータを移行する。同様に、マッピングｍａｐ23を使用して、スキーマＳ2のフォーマットからスキーマＳ3のフォーマットにデータを移行し、そして、ｍａｐ34を使用してスキーマＳ3のフォーマットからスキーマＳ4のフォーマットにデータを移行する。バージョンＳ1からバージョンＳ4にデータを移行する従来の方式は、ｍａｐ12、ｍａｐ23、ｍａｐ34を１つずつ実行するものであり、これは時間とコストがかかる。１回のステップでＳ1からＳ4にデータを移行するには、マッピング合成が必要となる。マッピングｍａｐ14は、初めにｍａｐ12およびｍａｐ23を合成し、次いで、結果得られたマッピングをｍａｐ34と合成することによって得ることができる。
【０００５】
次いで、Ｖ1がＳ1について定義されたビューであり、ｍａｐ1v1が関数であるとする。Ｓ1からＳ2にビューＶ1を移行するには、この場合も合成が用いられる。マッピングｍａｐ12の逆がｍａｐ1v1とともに合成されて、Ｓ2からＶ1へのマッピングｍａｐ2V1を得る。
【発明の開示】
【発明が解決しようとする課題】
【０００６】
マッピング合成のアルゴリズムは、各マッピングが関数である場合（すなわち、１つのデータベース状態を正確に１つのデータベース状態にマッピングし、両方のマッピングが同じ方向性を有する）についてはよく知られている。しかし、１つまたは両方のマッピングが関数でない、より広いクラスのマッピングに適したアルゴリズムに対する満たされない相当な要求（ｓｕｂｓｔａｎｔｉａｌ  ｕｎｍｅｔ  ｎｅｅｄ）がある。
【課題を解決するための手段】
【０００７】
以下に、本発明のいくつかの態様の基本的理解を提供するために、簡略化した本発明の要約を述べる。この要約は、本発明の広範囲にわたる概要ではない。この要約は、本発明の主要／不可欠な要素を明らかにするものでも、本発明の範囲を詳述するものでもない。その唯一の目的は、その後に提示されるより詳細な説明への前置きとして簡略化した形で本発明の一部の概念を提示することである。
【０００８】
本発明は、２つのスキーマ間の制約（ｃｏｎｓｔｒａｉｎｔ）や関数の逆（ｉｎｖｅｒｓｅ  ｏｆ  ｆｕｎｃｔｉｏｎ）など１つまたは両方のマッピングが関数でない、より広いクラスのマッピングを合成するのに適した一般的なアルゴリズムである。これは、２つの既存のマッピングを合成することにより、２つのデータベーススキーマ間で２つの既存のマッピングからマッピングを作成することを可能にする。この合成のアルゴリズムは、合成アルゴリズムが終了するかどうかをテストする手順を含む。
【０００９】
ここに開示され、特許権が請求される本発明は、その１つの態様で、スキーママッピングの合成を助けるシステムを備える。合成コンポーネントが、異種のデータソースの既存のスキーママッピングの合成を行い、スキーママッピングは、完全従属性（ｆｕｌｌ  ｄｅｐｅｎｄｅｎｃｙ）、局所従属性（ｅｍｂｅｄｄｅｄ  ｄｅｐｅｎｄｅｎｃｙ）、および２次従属性（ｓｅｃｏｎｄ−ｏｒｄｅｒ  ｄｅｐｅｎｄｅｎｃｙ）の少なくとも１つで表すことができ、２次従属性は、ソースからターゲットへの形式である必要はない。
【００１０】
本発明の別の態様では、２つのスキーママッピングを合成する方法論が提供され、この合成は、局所従属性で表されるスキーママッピングをＳｋｏｌｅｍｉｚｅして、２次従属性で表されるスキーママッピングを得ること、スキーママッピングを与える制約から演繹することができる入力署名および出力署名に対するすべての制約の有限の公理化を計算すること、および、有限の公理化をｄｅＳｋｏｌｅｍｉｚｅして、局所従属性で表されるスキーママッピングを得ること、による。
【００１１】
本発明のさらに別の態様では、方法論が提供され、この方法論では、有限の公理化をｄｅＳｋｏｌｅｍｉｚｅする動作はさらに、相等（ｅｑｕａｌｉｔｙ）を用いてＳｋｏｌｅｍ関数をアンネストして結論を生成すること、結論中のすべての変数が、Ｓｋｏｌｅｍ関数の可変従属性集合（ｖａｒｉａｂｌｅ  ｄｅｐｅｎｄｅｎｃｙ  ｓｅｔ）に出現することを確認すること、結論中に出現するＳｋｏｌｅｍ関数を統一することによって得られるすべての可能な文節を生成すること、各Ｓｋｏｌｅｍ項を新しい存在変数に置き換えることにより、各文節を別個にｄｅＳｋｏｌｅｍｉｚｅすることを備える。
【００１２】
前述の目的およびそれに関連する目的を達成するために、以下の説明および添付図面との関連で本発明の特定の例示的態様が記載される。しかし、それらの態様は、本発明の原理を用いることが可能な各種方式の数例に過ぎず、本発明は、そのような態様とその均等物をすべて包含するものとする。本発明の他の利点および新規の特徴は、図面と併せて以下の本発明の詳細な説明を検討することから明らかになろう。
【発明を実施するための最良の形態】
【００１３】
次いで図面を参照して本発明を説明するが、すべての図面を通じて同様の要素は同様の参照符号を使用して示す。以下の説明では、説明の目的で、本発明の完全な理解を提供するために、多数の具体的な詳細を述べる。しかし、本発明は、そのような具体的な詳細なしでも実施できることは明らかであろう。他の事例では、本発明の説明を容易にするために、よく知られる構造はブロック図で示す。
【００１４】
本願で使用される用語「コンポーネント」および「システム」は、ハードウェア、ハードウェアとソフトウェアの組合せ、ソフトウェア、実行中のソフトウェアを問わず、コンピュータに関連するエンティティを指すものとする。例えば、コンポーネントは、これらに限定しないが、プロセッサで実行されるプロセス、プロセッサ、オブジェクト、実行ファイル、実行のスレッド、プログラム、および／またはコンピュータ等である。例示として、サーバで実行されるアプリケーションとサーバの両方がコンポーネントとなることができる。プロセスおよび／または実行のスレッド中には１つまたは複数のコンポーネントが存在することができ、コンポーネントは、１つのコンピュータに局所化しても、かつ／または２つ以上のコンピュータに分散してもよい。
【００１５】
マッピングの合成（ｃｏｍｐｏｓｉｔｉｏｎ）  
本発明は、２つのスキーマの間の制約（ｍａｐ12、ｍａｐ23、ｍａｐ34など）や関数の逆（ｍａｐ12の逆など）など、いずれかまたは両方のマッピングが関数でない、より広いクラスのマッピングを合成するのに適した汎用的なアルゴリズムである。
【００１６】
図１に、本発明による、データベーススキーマ（図示せず）間の２つの既存のマッピング（１０４と１０６）の合成により得られるマッピング１０２の合成を表す図１００を示す。第１のスキーママッピング１０４（スキーママッピング12と表記）が提供され、このマッピングは、関数であっても、非関数であってもよい。同様に、第２のスキーママッピング１０６（スキーママッピング23と表記）が提供され、これも関数であっても非関数であってもよい。マッピングの合成のアルゴリズムは、各マッピングが関数である場合についてはよく知られる。そのため、本発明は、マッピングスキーマ（１０４および１０６）の１つまたは両方が非関数である事例のみを扱う。
【００１７】
点線で表すように、次のシナリオが扱われる。第１のスキーママッピング１０４が関数である時、第２のスキーママッピング１０６は非関数である。第１のスキーママッピング１０４が非関数の時、第２のスキーママッピング１０６は関数である。そして、第１のスキーママッピング１０４が非関数の時、第２のスキーママッピング１０６は非関数である。スキーママッピング（１０４および１０６）は、合成アルゴリズムコンポーネント１０８を使用して結果得られるマッピング１０２（スキーママッピング13と表記）を生成することによって合成される。合成コンポーネント１０８は、演繹的な手順を用いて、合成マッピングに出現する必要のあるすべての制約の有限の公理化（ａｘｉｏｍａｔｉｚａｔｉｏｎ）を得る。これについては、以下で詳細に説明する。
【００１８】
３つの非関数のマッピングのいずれでも、マッピングは、論理的制約あるいは文節（ｃｌａｕｓｅ）で表すことができる。図２に、本発明による論理的制約のマッピング合成を表す図２００を示す。３つのデータベーススキーマ２０２（Ｓ1、Ｓ2、およびＳ3と表記）が提供され、それらのスキーマから、第１および第２のスキーママッピング（２０４および２０６）（それぞれマッピング12およびマッピング23と表記）が導出される。
【００１９】
合成コンポーネント２０８（コンポーネント１０８と同様）は、２つのスキーママッピング（２０４と２０６）を合成して、最終的なスキーママッピング２１０（マッピング13と示す）にすることを助ける。検討される制約言語には、完全従属性（ＣＱ0=マッピング）、局所従属性（ＣＱ=マッピング）、または２次従属性（ＳＯＣＱ=マッピング。２次タプル生成従属性とも称する）が含まれる。したがって、第１および第２のマッピング（２０４および２０６）はそれぞれ、完全従属性、局所従属性、および／または２次の従属性である制約を含むことができる。必ずしも関数でない２つの有限のＣＱ0=マッピング、ＣＱ=マッピング、またはＳＯＣＱ=マッピングｍａｐ12およびｍａｐ23を与えられて、問題となるのは、ｍａｐ12とｍａｐ23の合成の最終的に得られるマッピング２１０を指定する、ＣＱ0=、ＣＱ=、またはＳＯＣＱ=マッピングを見つけることである。
【００２０】
次いで図３を参照すると、本発明による従属性の合成の方法論が示される。説明を簡潔にするために、例えばフローチャートの形で本明細書に示される１つまたは複数の方法論は、動作の連続として図示し、説明するが、一部の動作は、本発明により、ここに図示され、説明される順序とは異なる順序で、かつ／または他の動作と同時に行ってもよいので、本発明は、動作の順序によって制限されないことは理解されたい。例えば、当業者は、方法論は、代わりに状態図など相互に関連する状態または事象の連続として表すこともできることを理解されよう。さらに、本発明による方法論を実施するために、図示されるすべての動作が必要とは限らない。
【００２１】
合成は、次の３ステップで計算される。ＣＱ=マッピングがＳｋｏｌｅｍｉｚｅされて、２次従属性（ＳＯＣＱ=）マッピングを得る。本明細書において、Ｓｋｏｌｅｍｉｚａｔｉｏｎは、式から存在記号を取り除く手段（方法）（ｗａｙ）である。次いで、そのマッピングを与える制約から演繹することができる、入力署名および出力署名に対するすべての制約の有限の公理化が見つけられる。最後に、有限の公理化がｄｅＳｋｏｌｅｍｉｚｅされてＣＱ=マッピングを得る。したがって、次のように方法論が提供される。３００で、局所従属性がＳｋｏｌｅｍｉｚｅされて２次従属性を得る。３０２で、入力署名および出力署名に対するすべての制約の有限の公理化が見つけられる。公理化は、マッピングを与える制約から演繹することができる。３０４で、有限の公理化がｄｅＳｋｏｌｅｍｉｚｅされて局所従属性を得る。
【００２２】
ＣＱ0=マッピングおよびＳＯＣＱ=マッピングの場合は、図３の動作３０２のみが該当する。したがって、図４に、条件を課し、チェックを用いて合成が正しい答えで終了するかどうかを判定する、本発明による合成方法論を示す。４００で、Ｃｏｍｐｏｓｅアルゴリズムが実行される。以下のアルゴリズムｃｏｍｐｏｓｅは、入力マッピングｍａｐ12が、スキーマＳ1とＳ2の間のＣＱ0=の従属性の有限の集合Σ12で指定され、入力マッピングｍａｐ23が、Ｓ2とＳ3の間のΣ23によって指定され、出力マッピングｍａｐ13がＳ1とＳ3の間のΣ13で指定されると仮定する。（このＣＱ=マッピングおよびＳＯＣＱ=マッピングのための基本アルゴリズムの生成については、以下で述べる。）
【００２３】
【表１】
2006172436.tif 000003
【００２４】
ｃｏｍｐｏｓｅが終了した時には、このアルゴリズムが正しい答えを与えることが証明される。しかし、ｃｏｍｐｏｓｅは終了しない場合もある。４０２で、条件が課されてアルゴリズムの終了を確認する。アルゴリズムｃｏｍｐｏｓｅが終了する充足度をテストするために以下の条件を含めることができる。これらの条件は、４０４に示すように、ｃｏｍｐｏｓｅ（Σ12，Σ23）のｋ−１回の反復を実行し（ｋは、Ｓ2にある関係記号の数）、次のように形式φ（ｚ），Ｒ（ｙ）→Ｒ（ｘ）の制約がΣに出現するかどうかを調べることにより、多項式時間（ｐｏｌｙｎｏｍｉｎａｌ  ｔｉｍｅ）で調べることができる。
【００２５】
（１）ψ（ｚ）は、Ｓ1∪Ｓ3のアトムの連接（ｃｏｎｊｕｎｃｔｉｏｎ）である  
（２）｛ｘ｝は、｛ｙ｝の部分集合でない、かつ  
（３）Ｒは、Ｓ2にある関係記号である。
【００２６】
４０６で、条件が満たされると、ｃｏｍｐｏｓｅアルゴリズムは、正しい答えとともに終了する。
【００２７】
局所従属性を得るために、図３の動作３０４（ステップ３）で示すように、正しい結果を出すアルゴリズムが提供される。したがって、図５に、本発明による、有限の公理化にｄｅＳｋｏｌｅｍｉｚａｔｉｏｎを行って局所従属性を得る方法論を示す。５００で、相等を用いてＳｋｏｌｅｍ関数がアンネスト（ｕｎｎｅｓｔ）されてある結論に達する。５０２で、確認を行って、結論中のすべての変数が、各Ｓｋｏｌｅｍ関数の可変の従属性集合に現われることを保証する。５０４で、結論中のすべての変数が可変従属性に現われる場合は、流れは５０６に進み、結論中に現われるＳｋｏｌｅｍ関数を統合することによって得られるすべての可能な文節（ｃｌａｕｓｅ）を生成する。５０８で、各Ｓｋｏｌｅｍの項を新しい存在変数に置き換えることによって各文節が別個にｄｅＳｋｏｌｅｍｉｚｅされる。しかし、５０４ですべての変数が出現しない場合は、流れは５１０に進み、Ｓｋｏｌｅｍｉｚｅが失敗し、進行が終了する。
【００２８】
図６に、本発明による、４つ以上のデータソーススキーマ６０２についての複数の合成の図６００を示す。データソーススキーマ６０２（Ｓ1，Ｓ2，Ｓ3，．．．，ＳNと表す）の各対は、１次のスキーママッピング６０４（Ｍ12，Ｍ23，．．，Ｍ(N-1)(N)と表す）に関連付けられる。１次のスキーママッピング６０４の各対はさらに、合成コンポーネント（ＣNと表記）によって合成される。すなわち、１次スキーママッピングの第１の対（Ｍ12とＭ23）は、第１の合成コンポーネント６０６（Ｃ1と表記）を用いて結果得られる２次のスキーママッピングＭ１３を生成することによって合成される。結果得られた２次のマッピングＭ13が次いで、異なる合成コンポーネントＣ2（または同じ合成コンポーネントＣ1）を用いて、次の１次スキーママッピングＭ34と合成される。このプロセスは、合成すべき１次のスキーママッピング６０４がそれ以上なくなるまで継続し、結果得られたスキーママッピングＭINを出力で生成する。
【００２９】
図６のアルゴリズムに代えて、または図６のアルゴリズムに加えて、図７に、１回のアルゴリズムの呼び出しを使用して行われて出力マッピングＭINを得る、複数のマッピングの合成を容易にするシステム７００を示す。ここで、合成コンポーネント７０４は、１次スキーママッピング７０２の複数の入力（Ｍ12，Ｍ23，．．．，Ｍ(N-1)(N)と表記）を受け取り、マッピング７０２を処理し、出力で、結果得られたスキーママッピングＭINを１回のパスで生成する。
【００３０】
以下で検討するすべてのアルゴリズムと変種は、この方式で複数のマッピングに適用することができる。詳細には、図６に提示するアルゴリズムを図７のアルゴリズムに拡張することができ、下で述べるように、正しい合成を生成し、図６の段階的な手順がうまくいかない時でも終了することができる。
【００３１】
【表２】
2006172436.tif 000004
【００３２】
合成および非関数マッピングの分析  
用語「マッピング」は、データベースに関する文献では、データベース状態やＸＭＬドキュメントなどのインスタンスのバイナリ関係を指すものとして確立されている。モデル管理と称されるマッピングを管理する一般的なフレームワークは、マッピングと、モデルと称されるインスタンスのセットに対する一般的な演算子を研究する。そうした演算子には、ドメイン、範囲、合成、逆などの基本的な演算子がある。
【００３３】
マッピングが関数である場合、そのマッピングは関数（ｆｕｎｃｔｉｏｎａｌ）であると言う。非関数のマッピングは、特にデータ統合やデータ交換などの多くのコンテクストで現われる。非関数マッピングの自然な供給源は多数ある。例えば、写像でない関数マッピングの逆が、非関数マッピングになる。
【００３４】
この分野の大きな関心は、制約によって与えられるマッピングとモデルの開発、そして特に、局所従属性と完全従属性によって与えられるマッピングの開発に見出される。そのようなマッピングはそれぞれ、相等を有する連接クエリを（ＣＱ=）含めることと、相等を有する連接クエリが含まれるが存在記号を持たない（ＣＱ0=）ことから、ＣＱ=マッピングとＣＱ0=マッピングと呼ばれる。同様に、局所従属性と完全従属性によって与えられるモデルはそれぞれ、ＣＱ=モデルとＣＱ0=モデルと呼ばれる。
【００３５】
関係設定の基本的演算子についていくつかの基本的な問題が検討される。モデルおよびマッピングのための言語をＬとする。演算子
【００３６】
【数１】
2006172436.tif 000005
【００３７】
とＬモデルおよびＬマッピングを入力のために与えられて、（１）出力は常にＬモデルまたはＬマッピングか？（すなわちＬは
【００３８】
【数２】
2006172436.tif 000006
【００３９】
の下では閉じている）；（２）そうでない場合は、いつ出力がＬモデルまたはＬマッピングになるかを判定する判定手順があるか？。および（３）出力がＬモデルまたはＬマッピングである場合、その出力の表現を見つけるのはどれだけ大変か。
【００４０】
ここでの説明は、少なくとも、ＬがＣＱ0=、ＣＱ=、またはＳＯＣＱ=である事例を扱う。多くの演算子（例えば同一、交差、デカルト積など）については、（１）の答えが「ｙｅｓ」になり、（３）の答えが「非常に易しい」になることが理解できる（下記の命題３参照）。一部の他の演算子（範囲、ドメイン、合成など）については、（１）および（２）の答えが「ｎｏ」になることを示すことができる。さらに、（１）の答えが「ｙｅｓ」で（３）の答えが「容易」になる、ＣＱ0=、ＣＱ=、およびＳＯＣＱ=の大きな部分クラスが導入される。
【００４１】
ドメイン、範囲、および合成は、密接に関連し、互いに変形できることが理解することができる（下記の命題４参照）。したがって、合成と逆を研究すれば十分である。後者は、マッピングを定義する言語に対称の制約が置かれると容易である。それに対し、合成は、非常に難しいことが判明する。
【００４２】
マッピングの合成は、これまでに当技術分野で研究されている。ある研究では、ソースからターゲットへの２次のタプル生成従属性（ＳＴ  ＳＯ  ｔｇｄｓ）のクラスが取り入れられ、ＳＴ  ＳＯ  ｔｇｄｓによって与えられるマッピングのクラスは、合成の下では閉じていることが示される。さらに、より小さいマッピングのクラスは合成の下で閉じない事例を例証するいくつかの例が見つかっている。詳細には、ＣＱ=マッピングは、さらにソースからターゲットへの従属性に制約される場合でも、合成の下で閉じないことを示すことができる。
【００４３】
本発明は、従来技術の研究をいくつかの方向に拡張する。ここでは、ＳＯ  ｔｇｄｓによって与えられるマッピングをＳＯＣＱ=マッピングと称する。ＣＱ=マッピングをＳｋｏｌｅｍｉｚｅすると、ＳＯＣＱ=マッピングが得られることに気づかれたい。したがって、マッピングの主要な３つのクラスの合成が扱われ、それぞれのマッピングは、１つ前のマッピングを正しく含む。すなわち  
１．ＣＱ0=マッピング（完全従属性）  
２．ＣＱ=マッピング（局所従属性）  
３．ＳＯＣＱ=マッピング（ＳＯ  ｔｇｄｓ）
興味深い事例の１つは、局所従属性（ＣＱ=マッピング）の場合である。上記の図３で参照するように、そのようなスキーママッピングの合成を計算する方式の１つは、（１）ＣＱ=マッピングをＳｋｏｌｅｍｉｚｅしてＳＯＣＱ=マッピングを得、（２）そのマッピングを与える制約から演繹することができる入力および出力署名に対するすべての制約の有限の公理化を見つけ、そして最後に（３）有限の公理化をｄｅＳｋｏｌｅｍｉｚｅして、ＣＱ=マッピングを得る。ステップ２から３で困難が生じる。
【００４４】
本発明は、考慮される言語の制約を拡張して逆の下での閉鎖（ｃｌｏｓｕｒｅ）を得るが、これは、ソースからターゲットへの制約の逆はターゲットからソースへの制約になるので、ソースからターゲットへの制約の場合にはうまく行かない。
【００４５】
合成と逆の下で閉じ、合成の下で閉じることが分かっているＣＱ0=とＣＱ=クエリから生じる制約を理想的に含む、ＣＱ0=、ＣＱ=、およびＳＯＣＱ=の下位クラスが提供される。
【００４６】
２つのＣＱ0=マッピング（ＣＱ=、ＳＯＣＱ=）の合成をＣＱ0=マッピング（ＣＱ=、ＳＯＣＱ=）にするための、広く適用することができ、多項式時間で確認することができる、十分条件を有することが求められる。さらに、計算することが可能な必要かつ十分な条件があるかどうか、または問題が決定可能でないかどうかを知ることが好ましい。
【００４７】
ここに提供されるいくつかの態様を要約すると、ＣＱ0=マッピングは合成の下で閉じないことが示される。２つのＣＱ0=マッピングの合成がＣＱ0=マッピングであるかどうかを判定する問題は、決定不可能であることが示される。これらの結果は、ＣＱ=マッピングとＳＯＣＱ=マッピングの場合に持ち越される。加えて、合成についてのいくつかの等価の（有効でない）条件が提供される。
【００４８】
合成のための多項式時間で確認することができる十分条件が取り込まれ、これは、クエリによって与えられる制約の事例を含む。さらに、合成と逆の下で閉じ、クエリによって与えられる制約の事例を含む、ＣＱ0=、ＣＱ=、およびＳＯＣＱ=の部分集合が識別される。最後に、上記の条件を満たすＣＱ0=、ＣＱ=、およびＳＯＣＱ=マッピングの合成を計算する、多項式時間アルゴリズムが提示される。
【００４９】
予備情報  
署名σ＝｛Ｒ1，Ｒ2，．．．，ＲN｝は、関係記号の集合である。関係アトムは、Ｒ（ｔ1，．．．，ｔm）の種の式であり、ｔiは、変数または定数である。相等アトムは、ｔ1＝ｔ2のような種の式であり、ｔ1は、変数や定数などの項である。ＣＱは、連接クエリの集合、すなわち∃ｘ1，．．．，∃ｘm（ψ（ｘ1，．．．，ｘm．ｙ1，．．．，ｙn））のような種の式と定義され、ψは、関係アトムまたは相等アトムの連接であり、各自由変数ｙ1，．．．，ｙnは、何らかの関係アトムに出現する。ＣＱ0は、連接を有するが、存在記号を持たないクエリの集合である（すなわちｍ＝０のとき。ｓｅｌｅｃｔ−ｊｏｉｎクエリとも称される）。クエリクラスＬを与えられて、Ｌ=は、相等も含む対応するクエリクラスになる。
【００５０】
Ｓｋｏｌｅｍ（Ｑ）は、存在記号をＳｋｏｌｅｍ関数に置き換えることによってＱから得られる式と定義される。すなわち、Ｓｋｏｌｅｍ関数の存在を仮定し、１次の存在記号を持たない、存在２次式である。例えば、
Ｑ＝∃ｙ（Ｅｘｙ，Ｅｙｚ）→Ｅｘｚ  
の場合、  
Ｓｋｏｌｅｍ（Ｑ）＝∃ｆ（Ｅ（ｘ、ｆ（ｘｚ）），Ｅ（ｆ（ｘｚ），ｚ）→Ｅｘｚ）
となる。  
ＳｋＬ：＝｛Ｓｋｏｌｅｍ（Ｑ）：Ｑ∈Ｌ｝と設定する。署名σ1∪σ2に対する制約の集合ψを与えられると、
【００５１】
【数３】
2006172436.tif 000007
【００５２】
が、σ1にある関係記号のみを含むψの制約の集合となる。前提または結論にσ1からの関係記号を含む制約をσ1制約と称する。
【００５３】
モデルおよびマッピング。モデルは、インスタンスの集合である。モデルは、ＳＱＬ  ＤＤＬ、ＸＭＬスキーマなどの具体的言語で表すことができる。例えば、関係スキーマは、データベース状態の集合を表し、ＸＭＬスキーマは、ＸＭＬドキュメントの集合を表し、ワークフロー定義は、ワークフローインスタンスの集合を表し、プログラミングインターフェースは、そのインターフェースに準拠する実装の集合を表す。マッピングは、関係またはインスタンスである。特に指示しない限り、すべてのマッピングはバイナリ、すなわち２つのモデルの間で成立するものと想定する。マッピングは、ＳＱＬ  ＤＭＬ，ＸＳＬＴなどの具体的言語で表すことができる。
【００５４】
マッピングを指定する制約。制約は、ブールクエリである。制約の集合は、大文字のギリシャ文字を用いて表記し、個々の制約は、小文字のギリシャ文字で表す。検討される制約は、
【００５５】
【数４】
2006172436.tif 000008
【００５６】
にあり、
【００５７】
【数５】
2006172436.tif 000009
【００５８】
は、Ｑ1、
【００５９】
【数６】
2006172436.tif 000010
【００６０】
、および
【００６１】
【数７】
2006172436.tif 000011
【００６２】
中の自由変数の集合である。これらをＬに対するクエリ包含制約と称する。これらの種の制約は、Ｑ2におけるＱ1の制約を表し、ＬがＣＱ=である場合は局所従属性、ＬがＣＱ0=である場合は完全従属性と称される。
【００６３】
次の
【００６４】
【数８】
2006172436.tif 000012
【００６５】
の中の制約も検討され、
【００６６】
【数９】
2006172436.tif 000013
【００６７】
は、Ｑ1、
【００６８】
【数１０】
2006172436.tif 000014
【００６９】
の自由変数の集合であり、Ｑ1、Ｑ2は、関数記号
【００７０】
【数１１】
2006172436.tif 000015
【００７１】
から合成される項も有することができる点を除いては、ＣＱ0=クエリに似る。ＩＣ（ＳＯＣＱ）も同様に定義され、Ｑ1、Ｑ2は、ＣＱ0クエリに似る。
【００７２】
クエリ言語Ｌを与えられて、
（σ1，σ2，Σ12）  
の形式のすべての表現に関連付け、  
Σ12は、署名σ1∪σ2マッピング  
【００７３】
【数１２】
2006172436.tif 000016
【００７４】
に対するＩＣ（Ｌ）の有限の部分集合であり、σ1は、入力（あるいはソース）署名であり、σ2は、出力（あるいはターゲット）署名である。一般性を失うことなく、σ1、σ2が互いに素、または同一であると仮定する。
【００７５】
Ｅに対応するマッピングがｍである場合に、ｍが表現Ｅによって与えられるとする。さらに、Σ12がＩＣ（Ｌ）の有限の部分集合で、表現（σ1，σ2，Σ12）によってｍが与えられる場合に、ｍがＬマッピングであるとする。
【００７６】
合成。２つのマッピングｍ12およびｍ23を与えられると、合成ｍ12・ｍ23は、一意のマッピング  
｛＜Ａ，Ｃ＞：∃Ｂ（＜Ａ，Ｂ＞∈ｍ12∧＜Ｂ，Ｃ＞∈ｍ23）｝  
になる。
【００７７】
演繹およびチェース（ｃｈａｓｅ）  
以下に述べるのは、以下の項でアルゴリズムと正しさの証明を説明するために提供される追加的な予備事項である。以下では、具体的な演繹システムを固定し、├、
【００７８】
【数１３】
2006172436.tif 000017
【００７９】
、ＤＣ（＊）、およびｃｈａｓｅ（＊）の標準的な概念を定義し、定理１および２を与える。
【００８０】
ＩＣ（ＳＯＣＱ=）の制約が次の形式の規則として書かれる。
【００８１】
【数１４】
2006172436.tif 000018
【００８２】
この結果、Ｓｋｏｌｅｍ関数についての２次修飾子と、一番外側の１次の普遍的な修飾子
【００８３】
【数１５】
2006172436.tif 000019
【００８４】
が陰になる。
【００８５】
【数１６】
2006172436.tif 000020
【００８６】
を前提と称し、
【００８７】
【数１７】
2006172436.tif 000021
【００８８】
を結論と称する。前提が空の場合は、結論のみが書かれる。形式
【００８９】
【数１８】
2006172436.tif 000022
【００９０】
の規則を呼び出し、
【００９１】
【数１９】
2006172436.tif 000023
【００９２】
は、制約のタプル、すなわち事実である。
【００９３】
定義１。規則Σからの演繹は、一連の規則であり、それぞれの規則は、３つの方法の１つで得られる。  
１．Σからコピーする  
２．連続の中で先に現われる規則を拡大および／またはリネームする、または  
３．連続中で先に現われる２つの規則に分解を適用する。  
このような規則は、それぞれ、公理規則、拡張／リネーム規則、および分解規則と称される。
【００９４】
演繹手順は、演繹を用いて新しい規則を導出する手順である。演繹は、ｎ個の行からなる場合、長さｎを有する。規則ｒ’から拡張／リネームによって得られる規則ｒは、前提に追加的なアトムを有する可能性があり、任意の項に整合的に置き換えられた変数を有する可能性があり、前提の式と整合する結論中に置き換えを有する可能性がある。例えば、
Ｒ（ｘｙ），ｙ＝ｆ（ｘｙ）→Ｓ（ｘｙ）  
は、Ｒ（ｕｖ）→Ｓ（ｕｆ（ｕｖ））に拡張／リネームを適用した有効な結果である。
【００９５】
両方の公式を意味的に同じにする可変の置き換えが存在する時に、２つの公式を１つに統合することができる。分解は、１つの規則の前提のアトムを別の規則の結論のアトムと統合できる時に、２つの所与の規則から新しい規則を導出する完全な論理的推論手順である。例えば、  
Ｒ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｚ）  
は、規則  
Ｒ（ｘｙ）→Ｓ（ｘｙ）  
Ｓ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｚ）  
に分解を適用した結果である。
【００９６】
この例は、肯定式（ｍｏｄｕｓ  ｐｏｎｅｎｓ）と称される分解の特殊な例の具体例である。規則ｒ’、ｒ”に肯定式を適用することによって得られる規則ｒは、ｒ’の結論に出現しないｒ”のアトムとともに、ｒ”の結論とｒ’の前提のアトムから構成される。
【００９７】
演繹は、昇順で規則に番号をつけ、その行がどのように得られたかを示す正当化を各行に追加することによって注釈がつけられる。分解規則は２つのみの番号で、そして拡張／リネーム規則は１つの番号と変数の割り当てで正当化すれば十分である。公理規則は、他の注釈がないことを通じて示すことができる。変数の割り当ては、形式ｘ：＝ｙの項目のリストであり、ｘは変数であり、ｙは、項である。
【００９８】
（実施例１）  
Δ＝｛Ｒ（１，１）｝および  
Σ＝｛Ｒ（ｘｙ）→Ｓ（ｘｙ），Ｓ（ｚｚ）→Ｔ（ｚｚ）｝  
とすると、次が、Σ∪Δからの有効な演繹になる。  
１．Ｒ（１，１）  
２．Ｒ（ｘｙ）→Ｓ（ｘｙ）  
３．Ｒ（１，１）→Ｓ（１，１）    ［２］ｘ：＝１，ｙ：＝１  
４．Ｓ（１，１）                  ［１，３］  
５．Ｓ（ｚｚ）→Ｔ（ｚｚ）  
６．Ｓ（１，１）→Ｔ（１，１）    ［５］ｚ：＝１  
７．Ｔ（１，１）                  ［４，６］  
ここでは、規則１、２、５が公理であり、３および６が拡張／リネームであり、４および７が分解である。
【００９９】
演繹では、署名σ2のアトムを統一することによって分解が行われる場合に、分解ステップがσ2分解と呼ばれる。σ2分解で得られる規則ζは、σ2分解（ｒｅｓｏｌｖｅｎｔ）と称される。規則ζは、分解を用いずにζ’から演繹できる場合にζ’の変形になる。
【０１００】
次に述べるのは、合成アルゴリズムの正しさと決定不可能性の結果を証明する必須条件の紹介である。
【０１０１】
制約の集合Σから演繹があり、最後の行が制約ζを含む場合、ζはΣから演繹されると表され、これはΣ├ζと表記される。
【０１０２】
ΣのＬ演繹閉鎖は、  
ＤＣ（Ｌ，Σ）：＝｛ζ∈Ｌ：Σ├ζ｝  
である。文脈からＬが明らかである時にＤＣ（Σ）と書く。Σのすべての制約がＤで成立する場合は、
【０１０３】
【数２０】
2006172436.tif 000024
【０１０４】
と書く。すべてのインスタンスＤについて、
【０１０５】
【数２１】
2006172436.tif 000025
【０１０６】
が
【０１０７】
【数２２】
2006172436.tif 000026
【０１０８】
を示す場合に
【０１０９】
【数２３】
2006172436.tif 000027
【０１１０】
と書く。
【０１１１】
【数２４】
2006172436.tif 000028
【０１１２】
であれば、
【０１１３】
【数２５】
2006172436.tif 000029
【０１１４】
も成り立ち、すなわち演繹システムが健全であることを確かめることができる。演繹システムは、文の集合が満たすことができず、矛盾を導出することが保証される場合に完全と呼ばれる。演繹は、導出される規則が公理規則によって示唆されることを証明する。
【０１１５】
命題１。Δが事実の集合である場合、以下が等価となる。  
１．Σ∪Δ├φ  
２．Σ├ζおよびΔ，ζ├φとなるようにζがある。
【０１１６】
証明。（２）が成立すれば、Σ├ζおよびΔ，ζ├φを証明する演繹γおよびγ’が存在する。そして、Σ∪Δ├φを証明するγが、γにγ’を付加することによって得られる。次いで、（１）が成立し、γがΣ∪Δ├φを証明するとする。以下の置き換えを除いてγをγに設定し、以下の置き替えは、γの最初の規則から最後の規則まで規則ごとに行われる。  
１．規則ｒがΔからの公理規則である場合は、それを取り除く。  
２．規則ｒがΔからでない公理規則である場合は、そのままにする。  
３．規則ｒが規則ｉから拡張／リネームで得られる場合は、ｒ、およびｒについての変数割り当てにあるすべての制約ｃを、それに対応する変数ｖcに置き換える。  
４．規則ｒが規則ｉおよびｊからの分解で得られ、規則ｉがΔからの公理規則である場合は、ｒを、規則ｊからの自明の拡張／リネームに置き換える。  
５．規則ｒが規則ｉおよびｊからの分解によって得られ、規則ｉがｒからの公理規則でない場合は、ｒを、新しい規則ｉおよびｊに分解を適用した結果に置き換える。
【０１１７】
（実施例２）  
実施例１からの演繹γを前提とすると、γは、  
１．ブランク行  
２．Ｒ（ｘｙ）→Ｓ（ｘｙ）  
３．Ｒ（ｖ1ｖ1）→Ｓ（ｖ1ｖ1）    ［２］ｘ：＝ｖ1，ｙ：＝ｖ1 
４．Ｒ（ｖ1ｖ1）→Ｓ（ｖ1ｖ1）    ［３］  
５．Ｓ（ｚｚ）→Ｔ（ｚｚ）  
６．Ｓ（ｖ1ｖ1）→Ｔ（ｖ1ｖ1）    ［５］ｚ：＝ｖ1 
７．Ｒ（ｖ1ｖ1）→Ｔ（ｖ1ｖ1）    ［４，６］
各規則について以下の置き換えが行われている。
【０１１８】
１．Δからの公理：１によって除去される  
２．Σからの公理：２により変更なし  
３．拡張／リネーム：３により１がｖ1に置き換えられる  
４．１、３の分解：４により自明な拡張／リネーム  
５．Σからの公理：２により変化なし  
６．拡張／リネーム：３により１がｖ1に置き換えられる  
７．４，６の分解：５による分解
Δからの公理がもはや使用されず、また上記の１から５の置き換えによって規則Ｒが以前に置き換えられた規則から正しく演繹されることが保証されるので、γは、Σ├ζを証明する有効な演繹となる。また、以下のシーケンスから構成される演繹γ’によって、Δ、
【０１１９】
【数２６】
2006172436.tif 000030
【０１２０】
が証明される。  
−  γを得るためにγから取り除かれた、Δからの公理  
−  各変数ｖcをそれに対応する定数ｃにリネームすることにより、ζから得られた、ζ’が後に続くζ、および  
−  Δからの各公理を用い、ζ’で始まる分解ステップのシーケンス。
【０１２１】
定義２。インスタンスＤを与えられると、制約Σ⊆ＩＣ（ＳＯＣＱ=）およびＳｋｏｌｅｍ関数の集合ＦでＤをチェースした結果は、ｃｈａｓｅ（Ｄ，Σ，Ｆ）と略記することができ、
【０１２２】
【数２７】
2006172436.tif 000031
【０１２３】
から得られるデータベースＤ”で表記される。
【０１２４】
【数２８】
2006172436.tif 000032
【０１２５】
は制約のタプルであり、  
Δは、Ｄによって与えられる事実の集合であり、
【０１２６】
【数２９】
2006172436.tif 000033
【０１２７】
Φは、次のようにＦによって与えられる事実の集合である。
【０１２８】
【数３０】
2006172436.tif 000034
【０１２９】
Σ∪Δ∪Φ├ｃ0＝ｃ1の時かつその時に限り、ｃ0≡ｃ1と設定する。
【０１３０】
次いで、Ｄ’からＤ”を得るために、すべての相等クラスから１つの定数ｃ0を選び出し、その相等クラスのすべての制約をｃ0に置き換える。すなわち、Ｄ”：＝Ｄ’／≡になる。Ｆのすべての関数は、同じドメインを有することが必要とされる。それらが有限である場合は、ｃｈａｓｅ（Ｄ，Σ，Ｆ）が有限になる。この定義は、通常の定義の変形であり、関数Ｆは、チェースプロセス中に合成される。
【０１３１】
命題２。Ｃｈａｓｅ
【０１３２】
【数３１】
2006172436.tif 000035
【０１３３】
証明。何らかのζ∈ΣについてＤ”＝ｃｈａｓｅ
【０１３４】
【数３２】
2006172436.tif 000036
【０１３５】
と設定し、
【０１３６】
【数３３】
2006172436.tif 000037
【０１３７】
と仮定する。これは、ζの前提が成立し、結論が成立しないように、前提の変数
【０１３８】
【数３４】
2006172436.tif 000038
【０１３９】
に定数
【０１４０】
【数３５】
2006172436.tif 000039
【０１４１】
の何らかの割り当てがなければならないことを示唆する。結論が１つの関係アトム
【０１４２】
【数３６】
2006172436.tif 000040
【０１４３】
または１つの式ｙ1＝ｙ2からなり、
【０１４４】
【数３７】
2006172436.tif 000041
【０１４５】
は、
【０１４６】
【数３８】
2006172436.tif 000042
【０１４７】
に対する項のシーケンスであるとする。
【０１４８】
【数３９】
2006172436.tif 000043
【０１４９】
を、
【０１５０】
【数４０】
2006172436.tif 000044
【０１５１】
のすべての変数をそれに対応する定数
【０１５２】
【数４１】
2006172436.tif 000045
【０１５３】
に置き換えることによって
【０１５４】
【数４２】
2006172436.tif 000046
【０１５５】
から得られる項のシーケンスに設定する。前者が成立する場合は、Δ∪Φ，
【０１５６】
【数４３】
2006172436.tif 000047
【０１５７】
が成立し、
【０１５８】
【数４４】
2006172436.tif 000048
【０１５９】
は、Ｄ’にない。ζ∈Σであるので、命題１は、
【０１６０】
【数４５】
2006172436.tif 000049
【０１６１】
が成立することを示唆し、Ｄ’の定義と矛盾する。後者が成立する場合、Δ∪Φ、ζ├ｙ'1＝ｙ'2、およびｙ'1＝ｙ'2が成立する。ζ∈Ｚなので、命題１は、Σ∪Δ∪Φ├ｙ'1＝ｙ'2が成立することを示唆し、≡およびＤ”の定義と矛盾する。
【０１６２】
ＣＱ0=マッピングの合成  
以下の合成の説明は、ＣＯ0マッピングとＣＱ0=マッピングの合成を考察することから開始する。その後、それらの事例に対処するために導入された技術を拡張して、ＳＯＣＱ=マッピングとＣＱ=マッピングに対応する。２つのＣＱ0=マッピングの合成をＣＱ0=マッピングにするための必須および十分条件、そして計算不可能条件を与える（下記の定理１参照）。そして、ＣＱ0とＣＱ0=が合成の下で閉じないことが示され（下記の実施例３参照）、さらに、２つのＣＱ0=マッピングの合成がＣＱ0=マッピングであるかどうかを判定することが決定不可能であることが示される（下記の定理２参照）。合成のためのアルゴリズム（ＣＱ0=ＣＯＭＰＯＳＥ）が与えられ、このアルゴリズムは、下記の定理３の条件を満たすＣＱ0=マッピングについて正しく機能し、多項式時間で確認することができる。また、ｇｏｏｄＣＱ0=と呼ばれる、多項式時間で認識することができるＣＱ0=の部分集合が定義され、これは合成の下で閉じている（下記の定理４参照）。
【０１６３】
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられる２つのＣＱ0=マッピングの合成を、次のアルゴリズムを使用して計算することができる。
【０１６４】
【表３】
2006172436.tif 000050
【０１６５】
次のステップは、アルゴリズムの正しさを検証し、このアルゴリズムが終了する条件を研究することである。次の例が示すように、ＣＱ0とＣＱ0=は、合成の下で閉じないことに気づかれよう。
【０１６６】
（実施例３）  
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられるＣＱ0マッピングｍ12とｍ23を考えられたい。ここで、Σ12は、  
Ｒ（ｘｙ）→Ｓ（ｘｙ）  
Ｓ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｚ）  
であり、Σ23は、  
Ｓ（ｘｙ）→Ｔ（ｘｙ）  
である。
【０１６７】
そして、σ1＝｛Ｒ｝，σ2＝｛Ｓ｝、σ3＝｛Ｔ｝である。併せて、これらの制約は、Ｒ⊆Ｓ⊆Ｔであり、Ｓが推移的閉鎖（ｔｒａｎｓｉｔｉｖｅ  ｃｌｏｓｕｒｅ）の下で閉じることを示す。これは、ｔｃ（Ｒ）⊆Ｔであることを示唆し、ｔｃ（Ｒ）は、Ｒの推移的閉鎖である。ＲとＴの間で成立する唯一のＣＱ0=制約は、次の形式の制約になることが分かる  
Ｒ（ｘｖ1），Ｒ（ｖ1，ｖ2），．．．，Ｒ（ｖi-1，ｖi），Ｒ（ｖi，ｙ）→Ｔ（ｘｙ）  
が、これらの有限集合はいずれもｔｃ（Ｒ）⊆Ｔを表さない。
【０１６８】
実際、合成ｍ12・ｍ23は、ＦＯ（１次論理）ですら表すことができない。そうでない場合、
【０１６９】
【数４６】
2006172436.tif 000051
【０１７０】
のようにＦＯ文φを与えられて、ＦＯ式ψ（ｘｙ）を作成することができ、これは、φにおけるすべてのＴ（ｕｖ）の出現をｘ≠ｕ∨ｙ≠ｖに置き換えることによって得られる。そして、Ｒ⊆Ｄ2、
【０１７１】
【数４７】
2006172436.tif 000052
【０１７２】
の領域Ｄを与えられて、
【０１７３】
【数４８】
2006172436.tif 000053
【０１７４】
の時かつその時に限り、  
ｔｃ（Ｒ）⊆Ｄ2−＜ａ，ｂ＞の時かつその時に限り、  
＜ａ，ｂ＞∈ｔｃ（Ｒ）の時かつその時に限り、  
したがって、∀（ｘ，ｙ）¬ψ（ｘ，ｙ）は、Ｒが、ＦＯで表すことのできない接続グラフであることを意味する。
【０１７５】
２つのＣＱ0=マッピングの合成がＣＱ0=マッピングになるのはいつか。本明細書の定理１が、必要かつ十分条件を与える。合成をＣＱ0=マッピングにする障壁の１つは、帰納であるが、帰納は常に問題になるとは限らない。定理３では、効率的に調べることができる十分条件が提供され、定理４では、下記で定義されるＣＱ0=の部分集合であるｇｏｏｄＣＱ0=が合成の下で閉じることが示される。これらの結果はすべて、ＣＱ0について成立する。
【０１７６】
定理１。Σ123：＝Σ12∪Σ23およびσ13＝σ1∪σ3で、（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によってＣＱ0=マッピングｍ1、ｍ2が与えられる場合、以下が等価となる。
【０１７７】
（１）（σ1，σ2，Σ13）によってｍ：＝ｍ1・ｍ2が与えられるように、署名σ13に対する制約の有限の集合
【０１７８】
【数４９】
2006172436.tif 000054
【０１７９】
がある。
【０１８０】
（２）
【０１８１】
【数５０】
2006172436.tif 000055
【０１８２】
となるように、署名σ13に対する制約の有限の集合
【０１８３】
【数５１】
2006172436.tif 000056
【０１８４】
がある。
【０１８５】
（３）Σ123├ζを満たす署名σ13のすべてのζについて、多くともｍ回のσ2分解を用いたΣ123からのζの演繹があるように、ｍがある。
【０１８６】
証明。この証明では、下記の補助命題（ｌｅｍｍａ）１および２を用いる。この証明では、初めに、（１）と（２）の等価性を示し、次いで（２）と（３）の等価性を示す。
【０１８７】
（２）が成立すると仮定する。すると、＜Ａ，Ｃ＞∈ｍ1・ｍ2となる。
【０１８８】
【数５２】
2006172436.tif 000057
【０１８９】
これは、（１）が成立することを示す。
【０１９０】
逆に（１）が成立すると仮定する。すると、
【０１９１】
【数５３】
2006172436.tif 000058
【０１９２】
となる。
【０１９３】
【数５４】
2006172436.tif 000059
【０１９４】
これは（２）が成立することを示す。
【０１９５】
次いで（３）が成立すると仮定する。Σを、多くともｍ回のσ2分解を用い、他の分解は用いずに演繹することができる、
【０１９６】
【数５５】
2006172436.tif 000060
【０１９７】
のすべての制約の集合に設定する。Σのすべての制約は、有限の部分集合Σ13⊆Σから拡張／リネームによって得ることができる。（２）が成立することが示されることができる。
【０１９８】
Σ123├ζを証明する演繹γがあると仮定する。（３）が成立するので、γがｍ’回のσ2分解を有すると仮定することができる。補助定理２により、同じくｍ’回のσ2分解を有するΣ123├ζを証明する演繹γがあり、それらはすべて、他の分解より前に行われる。γの最後の行は、σ2からの記号を含まないので、γは、最後のσ2分解の後にσ2からの記号を含む行は含まないと仮定することができる。
【０１９９】
γを、最後のσ2分解までの、そして最後のσ2分解を含むγの最初の部分であるγ1と、γの残りの部分であるγ2、の２つの部分に分割する。Σの定義により、γ1にあるすべての制約ψは、Σになければならず、したがってΣ13├ψが成立する。γ2のすべての制約ψは、σ2の記号を含まず、
【０２００】
【数５６】
2006172436.tif 000061
【０２０１】
となり、これはΣ13├ψを示唆する。したがって、要求されるようにΣ13├ζとなる。
【０２０２】
逆に（２）が成立すると仮定する。Σ123からすべてのψ∈Σ13を演繹するために必要なσ2分解の総数をｍとする。Σ123├ζと仮定する。すると、Σ13├ζを証明する演繹γがある。明らかに、γは、σ2分解を持たない。γから、Σ13にあるすべての制約の演繹をγに付加し、その公理の演繹が終了する行の空の（ｖａｃｕｏｕｓ）拡張／リネームによってΣ13からの公理が用いられるすべての行を置き換えることによって、Σ123├ζを証明するγを得ることができる。明らかに、γは、要求される通り正確にｍ回のσ2分解を有する。これは、（３）が成立することを示す。
【０２０３】
補助命題１。定理１の仮定の下では、以下が等価である。
【０２０４】
１．
【０２０５】
【数５７】
2006172436.tif 000062
【０２０６】
２．
【０２０７】
【数５８】
2006172436.tif 000063
【０２０８】
証明。何らかのＢについて
【０２０９】
【数５９】
2006172436.tif 000064
【０２１０】
と仮定する。すると、（健全性により）
【０２１１】
【数６０】
2006172436.tif 000065
【０２１２】
となり、したがって、Ｂは
【０２１３】
【数６１】
2006172436.tif 000066
【０２１４】
で言及されないので
【０２１５】
【数６２】
2006172436.tif 000067
【０２１６】
となる。
【０２１７】
逆に
【０２１８】
【数６３】
2006172436.tif 000068
【０２１９】
と仮定する。
【０２２０】
【数６４】
2006172436.tif 000069
【０２２１】
と設定する。
【０２２２】
チェースが終了し、Ａ＝Ａ’、およびＣ＝Ｃ’である場合は、命題２により、
【０２２３】
【数６５】
2006172436.tif 000070
【０２２４】
となり、これは、要求される通り
【０２２５】
【数６６】
2006172436.tif 000071
【０２２６】
および
【０２２７】
【数６７】
2006172436.tif 000072
【０２２８】
になることを示唆する。
【０２２９】
取り込まれる新しい制約がないので、チェースが終了することが明らかである。次いで、矛盾を得るために、Ａ≠Ａ’、およびＣ≠Ｃ’であると仮定する。ΔACを、ＡおよびＣによって与えられる事実の集合に設定する。すると、
【０２３０】
【数６８】
2006172436.tif 000073
【０２３１】
となり、Ｒは、
【０２３２】
【数６９】
2006172436.tif 000074
【０２３３】
を含まないＡまたはＣの関係であり、または、  
Σ123∪ΔAC├ｃ0＝ｃ1 
となり、  
ｃ0、ｃ1は、ＡまたはＣの別個の制約である。
【０２３４】
前者の場合を考えられたい。後者も同様である。
【０２３５】
【数７０】
2006172436.tif 000075
【０２３６】
である場合は、命題１により、Σ123├ζおよび
【０２３７】
【数７１】
2006172436.tif 000076
【０２３８】
となるようにζが存在する。
【０２３９】
【数７２】
2006172436.tif 000077
【０２４０】
なので、これから、
【０２４１】
【数７３】
2006172436.tif 000078
【０２４２】
および
【０２４３】
【数７４】
2006172436.tif 000079
【０２４４】
であることになり、これは最初の仮定と矛盾する。
【０２４５】
補助命題２。定理１の仮定の下で、多くともｍ回のσ2分解を有するΣ123├ζを証明する演繹γがある場合、多くともｍ回のσ2分解を有するΣ123├ζを証明するγがあり、さらに、すべてのσ2分解は、すべての他の分解より前に出現する。
【０２４６】
証明。ｋ＜ｍ、およびγk,lが、次のようなΣ123├ζを証明すると仮定する。  
１．正確にｍ回のσ2分解  
２．最初のｋ個の分解がσ2分解であり、  
３．ｋ＋１番目のσ2分解または演繹の最後より前に、非σ2分解が正確にｌ個ある。
【０２４７】
証明は、ｋおよびｌに対する帰納によって進める。ｌ＞０のγk,lを前提として、証明は、γk,l-1をどのように得るかを示す。ｌ＝０の場合を証明するには、単にγk+1,l：＝γk,0と設定し、ｌ’は、上記の条件を満たす。何らかのｌ’についてγml’が得られると、γ：＝γm,l’と設定し、補助命題が証明される。
【０２４８】
例えばそれぞれαとβを含む行ｉおよびｊのγk,jの（ｋ＋１）番目のσ2分解である
【０２４９】
【数７５】
2006172436.tif 000080
【０２５０】
を含む行ｓを考えられたい。また、例えば、それぞれλ1とλ2を含む行ｒ1およびｒ2のγk,jのｌ番目の非σ2分解であるλを含む行ｒも考えられたい。
【０２５１】
次いでいくつかの事例を検討する。ｉ，ｊ＜ｒ＜ｓである場合、行ｓをｒのすぐ前に移動することにより、γk,l-1を得る。行ｉ，ｊが行ｒから得られない場合は、初めに、ｉ，ｊ＜ｒ＜ｓとなるようにγk,jからγk,jを再配列し、上記のように進行することにより、γk,l-1を得る。
【０２５２】
そうでない場合は、行ｒから、拡張／リネームを通じてαまたはβが得られている。表現を簡略にするために、両方が行ｒからの１回の拡張／リネームを通じて得られていると仮定する（他の場合も同様）。その結果、ｒ＜ｉ、ｊ＜ｓが存在することになる。必要な場合はγk,jを再配置することにより、ｉ＝ｒ＋１、ｊ＝ｒ＋２、およびｓ＝ｒ＋３であると仮定する。αとβは拡張／リネームによりｒから得ることができるので、拡張／リネームにより、それぞれｒ1、ｒ2からα1、α2、およびβ1、β2が得られ、その結果、αは、α1、α2の分解となり、βはβ1、β2の分解となる。４つの連続した行ｒ、ｉ、ｊ、ｓを次の７つの行に置き換える。  
ｒ        α1    ［ｒ1］  
ｒ＋１    α2    ［ｒ2］  
ｒ＋２    β1    ［ｒ1］  
ｒ＋３    β2    ［ｒ2］  
ｒ＋４    δ1    ［ｒ＋１、ｒ＋２］  
ｒ＋５    δ2    ［ｒ＋４］  
ｒ＋６    δ      ［ｒ＋５、ｒ＋３］
重要な点は、αとβが分解するため、α2およびβ1がσ2の関係記号を通じて分解しなければならないので、行ｒ＋４が今度はσ2分解を含むようになることである。α1、α2、β1、β2の分解の結果がαおよびβの分解の結果と同じになる（これは分解が「連想型」であるため）ので、δが行ｒ＋６に来ることに注意されたい。
【０２５３】
帰結１。定理１の仮定の下では、ＣＱ0=ＣＯＭＰＯＳＥ（Σ13，Σ23）が終了した時に、（σ，σ3，Σ13）によってｍ12・ｍ23が与えられるように、ＣＯＭＰＯＳＥはΣ13を与える。
【０２５４】
メインループがｍ回反復した後に、Σは、多くともｍ回のσ2分解ステップを使用して演繹することができるすべての制約の変形を含んでいることに気づかれよう。実施例３の制約は、定理１の（３）を満たすことができず、したがってＣＱ0=ＣＯＭＰＯＳＥ（Σ12，Σ23）は、Σ12、Σ23が入力のために実施例３のようにある時に終了しない。これに対し、ＣＱ0=ＣＯＭＰＯＳＥ（Σ12，Σ23）は、下記の実施例からのΣ12、Σ23で終了し、これは定理１の（３）を満たし、そのため再帰が常によくないという訳ではない。
【０２５５】
（実施例４）  
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられるＣＱ0マッピングｍ12およびｍ23で、Σ12が  
Ｒ（ｘｙ）→Ｓ（ｘｙ）  
Ｓ（ｘｙ），Ｓ（ｙｚ）→Ｒ（ｘｚ）  
であり、Σ23が  
Ｓ（ｘｙ）→Ｔ（ｘｙ）  
であるものを考えられたい。
【０２５６】
ここでσ1＝｛Ｒ｝、σ2＝｛Ｓ｝、およびσ3＝｛Ｔ｝である。ともに、これらの制約は、Ｒ⊆Ｓ⊆Ｔであり、ＲとＳが推移的閉鎖の下で閉じており、（この理由は制約  
Ｓ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｚ）  
Ｒ（ｘｙ）、Ｒ（ｙｚ）→Ｒ（ｘｚ）  
を上記の制約から演繹できるため）、そしてＳ（ｘｙ），Ｓ（ｙｚ）が成立すれば必ずＲ（ｘｚ）が成立することを意味する。制約  
Ｒ（ｘｙ），Ｒ（ｙｚ）→Ｒ（ｘｚ）  
Ｒ（ｘｙ）→Ｔ（ｘｙ）  
は、正確に合成ｍ1・ｍ2を表し、正確に、ＣＱ0=ＣＯＭＰＯＳＥ（Σ１２，Σ２３）によって見つけられるものになる。
【０２５７】
定理２。２つのＣＱ0マッピングの合成がＣＱ0マッピングであるかどうかの確認は、決定不能である（実際ｃｏＲＥ−ｈａｒｄである）。同じことは、ＣＱ0ではなくＣＱ0=にも当てはまる。
【０２５８】
証明。証明では、決定不能であることが知られているポストの対応問題（ＰＣＰ；Ｐｏｓｔ'ｓ  ｃｏｒｒｅｓｐｏｎｄｅｎｃｅ  ｐｒｏｂｌｅｍ）を、ｍ12とｍ23がＣＱ0マッピングである場合にｍ12・ｍ23がＣＱ0マッピングであるかどうかを判定する問題に変形する。ＰＣＰ問題を与えられて、ｍ12・ｍ23がＣＱ0マッピングでない場合にのみかつその時に限りＰＣＰ問題に解があるようにｍ23を定義する（ｍ12は、ＰＣＰ問題に依存しない）。
【０２５９】
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によってＣＱ0マッピングｍ12・ｍ23が与えられ、ここで  
・  σ1＝｛Ａ，Ｂ，Ｏ，Ｚ｝  
・  
【０２６０】
【数７６】
2006172436.tif 000081
【０２６１】
、および  
・  σ3＝｛Ｔ｝  
である。Ａ、Ｂは単項であり、他のすべての関係は二項であり、Σ12とΣ23は下記の通りである。
【０２６２】
Ｚ、Ｏ（Ｚは「ゼロ」をあらわし、Ｏは「１」を表す）を通るＡからＢの経路に対応するσ1について、アトムの集合  
Ａ（ｘ），Ｚ（ｘａ）、Ｚ（ａｂ），Ｏ（ｂｃ），Ｏ（ｃｙ）、Ｂ（ｙ）  
についてｘ００１１ｙを書く。
【０２６３】
同様に、σ2に対して、アトムの集合に
【０２６４】
【数７７】
2006172436.tif 000082
【０２６５】
【数７８】
2006172436.tif 000083
【０２６６】
を書く。  
Σ12は、制約
【０２６７】
【数７９】
2006172436.tif 000084
【０２６８】
と、すべての組合せＡＯ、ＺＺ、ＺＯ、ＯＺ、ＺＢ、ＯＢについての対応するすべての制約を含む。これらの制約は、任意の文字列Ｓから
【０２６９】
【数８０】
2006172436.tif 000085
【０２７０】
を演繹できることを示唆する。
【０２７１】
次のように、各ＰＣＰ「ドミノ」をΣ23の制約で符号化する。例えば、ドミノ００１１／０１１を制約
【０２７２】
【数８１】
2006172436.tif 000086
【０２７３】
として符号化する。
【０２７４】
最後に、Σ23に、制約
【０２７５】
【数８２】
2006172436.tif 000087
【０２７６】
を加える。
【０２７７】
次いで、ＰＣＰ問題が、｛０，１｝*に対する文字列Ｓに解を有すると仮定する。これは、形式  
ｘＳkｙ、ｘ’Ｓkｙ’→Ｔ（ｘｙ）  
の多くの制約を無限に演繹し、Ｓkは、次のようにｋ回繰り返される文字列Ｓである。これらの制約は、σ1∪σ3に対するものであり、これらの制約はいずれも他の制約から得られないことに気づかれたい。
【０２７８】
ｋ＝１について（他の場合も同様）、初めにΣ12の制約を用いて
【０２７９】
【数８３】
2006172436.tif 000088
【０２８０】
を得、次いで、Ｓを得るために必要なブロックの連続に対応するΣ23の規則を用いて、分解により、  
ｘＳｙ，ｘ’ＳｙＳ→Ａ（ｘｘ’），Ａ（ｙｙ’），Ｂ（ｙｙ’）  
を順番に得る。最後に、Σ23の最後の制約を用いて、  
ｘＳｙ，ｘ’ＳｙＳ→Ｔ（ｘ、ｙ）  
を得る。
【０２８１】
逆に、ＰＣＰ問題に解がない場合は、σ1∪σ3の前提と
【０２８２】
【数８４】
2006172436.tif 000089
【０２８３】
の結論を有する演繹は可能でない。これが、σ1∪σ3の結論と一致する唯一の前提なので、σ1∪σ3の制約の前提で演繹されるものはない。この場合、
【０２８４】
【数８５】
2006172436.tif 000090
【０２８５】
が合成ｍ12・ｍ23を与える。
【０２８６】
定理２からのｃｏＲＥ−ｈａｒｄｎｅｓｓは、アルゴリズムＣＱ0=ＣＯＭＰＯＳＥは、合成がＣＱ0=マッピングであっても終了しない場合があることを示唆する。これは、例えば次の場合に発生する。
【０２８７】
（実施例５）  
（σ1、σ2、Σ12）および（σ2、σ3、Σ23）によって与えられるＣＱ0マッピングｍ12およびｍ23を考えられたい。ここで、Σ12は、  
Ｒ（ｘｙ）→Ｓ（ｘｙ）  
Ｒ（ｘｙ），Ｒ（ｙｚ）→Ｒ（ｘｚ），Ｒ’（ｙ）  
Ｓ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｙ），Ｓ’（ｙ）  
であり、Σ23は、  
Ｓ（ｘｙ）→Ｔ（ｘｙ）  
であり、σ1＝｛Ｒ，Ｒ’｝、σ2＝｛Ｓ，Ｓ’｝、σ3＝｛Ｔ｝である。制約  
Ｒ（ｘｙ），Ｒ（ｙｚ）→Ｒ（ｘｚ），Ｒ（ｙ）  
Ｒ（ｘｙ）→Ｔ（ｘｙ）  
は、正確に合成ｍ1・ｍ2を表すが、アルゴリズムＣＱ0=ＣＯＭＰＯＳＥは、実施例３で演繹する多くの制約を無限に演繹することになるので、終了することがない。
【０２８８】
以下の条件は、アルゴリズムＣＱ0=ＣＯＭＰＯＳＥが終了するのに十分である。これらの条件は、次のように多項式時間で調べることができる。ＣＱ0=ＣＯＭＰＯＳＥ（Σ12，Σ23）をｋσ2−１回反復して実行し、ｋσ2は、σ2の関係記号の数であり、そして、下記の形式の制約がΣに出現するかどうかを調べる。
【０２８９】
定理３。定理１の仮定では、
１．
【０２９０】
【数８６】
2006172436.tif 000091
【０２９１】
がσ123に対するアトムの連接  
２．
【０２９２】
【数８７】
2006172436.tif 000092
【０２９３】
には
【０２９４】
【数８８】
2006172436.tif 000093
【０２９５】
のアトム
【０２９６】
【数８９】
2006172436.tif 000094
【０２９７】
はない  
３．
【０２９８】
【数９０】
2006172436.tif 000095
【０２９９】
、かつ  
４．Ｓはσ2にある関係記号  
であるような形式
【０３００】
【数９１】
2006172436.tif 000096
【０３０１】
の制約は、σ2統合のみを用いてΣ123から演繹されることができず（これは不良な制約と呼ばれる）、そしてＣＱ0=ＣＯＭＰＯＳＥ（Σ12，Σ23）が終了し、そのためｍ1・ｍ2はＣＱ0=マッピングになる。同じことがＣＱ0マッピングにも成り立つ。
【０３０２】
証明。この仮定が成立すると仮定する。σ2統合のみを用いるΣ123├ζを証明する演繹γで、ζが結論にσ2アトムを含むものを考えられたい。一般性を失わずに、初めにすべてのリネーム動作が行われ、その後すべての分解動作が行われるとする。また、γにあるすべての規則が、その結論に１つのアトムを含み、すべての規則が多くとも１回の分解ステップで用いられるものとする。
【０３０３】
このような演繹は、ツリーＴとして表すことができ、このツリーではすべてのノードが１つのアトムである。Ｔのすべての非葉ノードは、何らかの規則ｒの結論である。ｒの子は、規則ｒの前提にあるアトムである。ζの前提は、Ｔのすべての葉からなり、その結論は、Ｔのルートとなる。
【０３０４】
すべてのノードについて、Ｔにあるそのすべての子を含むか、子をまったく含まないＴの任意の部分ツリーＴを、Σ123├ζ’を証明する演繹γに変換できるかどうかを調べるのは容易であり、ここで、ζ’の前提は、Ｔのすべての葉からなり、その結論はＴのルートである。
【０３０５】
この仮定が成立するので、どの部分ツリーもそのルートとして
【０３０６】
【数９２】
2006172436.tif 000097
【０３０７】
を、その葉として
【０３０８】
【数９３】
2006172436.tif 000098
【０３０９】
を含むことはできず、Ｓは、σ2と
【０３１０】
【数９４】
2006172436.tif 000099
【０３１１】
の関係記号である。したがって、ノード
【０３１２】
【数９５】
2006172436.tif 000100
【０３１３】
を含むＴの葉からルートへの経路は、Ｓ個のアトムを有する多くとも２rｒ！8個の他のノードのみを含み、ｒは、Ｓのアリティー（ａｒｉｔｙ）である。これは、そのような経路はいずれも、ｋσ2２’σ2ｒσ2！を限界とする長さを持たなければならないことを意味し、ｋσ2は、σ2にある関係記号の数であり、ｒσ2は、σ2の関係記号の最大アリティーである。その結果、変形に至るまで、σ2統合を通じて得ることができるΣ123の結論は有限数しかなく、これは、ＣＱ0=ＣＯＭＰＯＳＥ（Σ12，Σ23）が終了することを意味する。
【０３１４】
定義３。ＣＱ0=マッピングは、  
１．
【０３１５】
【数９６】
2006172436.tif 000101
【０３１６】
がσ1∪σ2に対するアトムの連接
２．
【０３１７】
【数９７】
2006172436.tif 000102
【０３１８】
には
【０３１９】
【数９８】
2006172436.tif 000103
【０３２０】
のアトム
【０３２１】
【数９９】
2006172436.tif 000104
【０３２２】
はない  
３．
【０３２３】
【数１００】
2006172436.tif 000105
【０３２４】
かつ
４．ＳおよびＳ’はともにσ1またはσ2の関係記号  
であるような形式
【０３２５】
【数１０１】
2006172436.tif 000106
【０３２６】
の制約が、σ1統合のみまたはσ2統合のみを用いてΣ123から演繹できないように、（σ1，σ2，Σ12）によって与えられる場合に、ｇｏｏｄＣＱ0=マッピングとなる。ｇｏｏｄＣＱ0も同様に定義する。
【０３２７】
定理４。ｇｏｏｄＣＱ0=とｇｏｏｄＣＱ0は、合成および逆の下で閉じる。  
注１。ＣＱ0=クエリはｇｏｏｄＣＱ0=マッピングに含まれる。総合的および全射（ｓｕｒｊｅｃｔｉｖｅ）のＣＱ0=マッピングは、合成の下で閉じないことに気づかれたい。
【０３２８】
（実施例６）  
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられるＣＱ0マッピングｍ12およびｍ23を考えられたい。ここでΣ12は、  
Ｒ（ｘｙ）→Ｓ（ｘｙ）  
Ｒ（ｘｙ），Ｓ（ｙｚ）→Ｓ（ｘｚ）  
であり、Σ23は、  
Ｓ（ｘｙ）→Ｔ（ｘｙ）  
であり、  
σ1＝｛Ｒ｝、σ2＝｛Ｓ｝、σ3＝｛Ｔ｝である。ここで、ｍ12およびｍ23は、総合および全射であり、その合成は、ｔｃ（Ｒ）⊆Ｔになることを意味し、これは、実施例５に見られるようにＦＯでも表すことができない。
【０３２９】
ＳＯＣＱ=マッピングの合成  
この項で扱うのはＳＯＣＱ=マッピングの合成である。ＣＱ=マッピングの存在記号に対応するために、初めに、ＣＱ=マッピングの制約をＳｋｏｌｅｍ形式に変換し、それによりＳＯＣＱ=マッピングが得られる。下記の定理５で、ＳＯＣＱ=マッピングは、存在的に定量化された関数記号（ｅｘｉｓｔｅｎｔｉａｌｌｙ−ｑｕａｎｔｉｆｉｅｄ  ｆｕｎｃｔｉｏｎ  ｓｙｍｂｏｌ）を用いて、中間の署名σ2に関係が存在することを仮定することができるので、合成の下で閉じることが示される。
【０３３０】
次の関連する問いも非常に重要である。  
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によってＳＯＣＱ=マッピングｍ12・ｍ23が与えられる場合、Σ13⊆ＳＯＣＱ=が、Σ12∪Σ23に出現するもの以外の関数記号または制約を持たないようにｍ13＝ｍ12・ｍ23を満たす（σ1，σ3，Σ13）によって与えられるＳＯＣＱ=マッピングは存在するか？存在する場合は、ｍ12およびｍ23がコンサーバティブ（ｃｏｎｓｅｒｖａｔｉｖｅ）な合成を有すると表す。
【０３３１】
最終的には、ＣＱ=マッピングを得るためにすべての関数記号を除去する必要があり、また下記の定理５の証明で用いられるような等式で導入される関数記号をどのように除去するかは分からないので、コンサーバティブ合成は重要である。上記の項の定理１および２で、ＳＯＣＱおよびＳＯＣＱ=はコンサーバティブ合成の下では閉じず、２つのＳＯＣＱ=マッピングのコンサーバティブ合成がＳＯＣＱ=マッピングになるかどうかの判定は決定不可能であることが示される。ＣＱ0=マッピングの場合と同様に、２つのＳＯＣＱ=マッピングがコンサーバティブな合成を有するための必要かつ十分の計算不可能な条件が与えられ（下記の定理６参照）、効率的に調べることができるコンサーバティブな合成のための十分条件が与えられる。ＳＯＣＱ=マッピングに正しく機能し、上記の条件を満たす、コンサーバティブ合成のためのアルゴリズム（ＳＯＣＱ=ＣＯＭＰＯＳＥ）が与えられる。また、ＳＯＣＱ=の多項式時間の部分集合としてｇｏｏｄＳＯＣＱ=が定義され、これは、コンサーバティブな合成の下で閉じる。１つ前の項と対照的に、この場合は、等化が不可欠であり、そのためそれらの結果はＳＯＣＱには成立しないことが分かる。
【０３３２】
結果に進む前に、ＩＣ（ＳＯＣＱ=）制約のセマンティックを簡単に説明する。問題となるのは、関数が値をとることができる母集団（ｕｎｉｖｅｒｓｅ）は何か、すなわち許容される範囲は何になるかということである。直感的には、問題は、存在的に定量化された中間データベースの母集団にあるように思われる。すべてのデータベースは、有限（すなわちすべての関係が有限）であるが、陰の可算的に無限の母集団を有することを必要とされる。関数は、その範囲が有限であれば、この陰の母集団からどの値をとることも許される。これらの仮定により、下記の定理６に必要とされる、項２で紹介した演繹システムがＩＣ（ＳＯＣＱ=）について健全になることが保証される。
【０３３３】
定理５。ＳＯＣＱ=マッピングは合成の下で閉じる。  
証明。（σ1，σ2，Σ12）および（σ2，σ3，σ23）によってＳＯＣＱ=マッピングｍ12およびｍ23が与えられる場合、Σ13は、合成ｍ12・ｍ23が次のように（σ1，σ2，Σ23）によって与えられるように取得される。Σ13：＝Σ'12∪Σ'23と設定し、Σ'12およびΣ'23は、アトム
【０３３４】
【数１０２】
2006172436.tif 000107
【０３３５】
（Ｒ∈σ2）のすべての出現を
【０３３６】
【数１０３】
2006172436.tif 000108
【０３３７】
【数１０４】
2006172436.tif 000109
【０３３８】
と置き換えることによってΣ12およびΣ23から得られ、
【０３３９】
【数１０５】
2006172436.tif 000110
【０３４０】
であり、ｆ、ｇR、ｈRは、新しい関数記号である。
【０３４１】
次いで、＜Ａ，Ｃ＞∈ｍ12・ｍ23である場合は、
【０３４２】
【数１０６】
2006172436.tif 000111
【０３４３】
かつ
【０３４４】
【数１０７】
2006172436.tif 000112
【０３４５】
となるようにＢがある。設定
【０３４６】
【数１０８】
2006172436.tif 000113
【０３４７】
は、そのドメインから任意の２つの値を使用することにより、σ2のすべての関係ＲについてＢで成立する。さらに、ｃがＢのアクティブなドメインである場合にｆ（ｃ）：＝ｃ、ｆ（ｃ）；＝ｃ’と設定し、そうでない場合、ｃ’は、そのドメインの何らかの値になる。すると
【０３４８】
【数１０９】
2006172436.tif 000114
【０３４９】
となる。逆に
【０３５０】
【数１１０】
2006172436.tif 000115
【０３５１】
の場合は、σ2のすべての関係Ｒについて
【０３５２】
【数１１１】
2006172436.tif 000116
【０３５３】
と設定して、
【０３５４】
【数１１２】
2006172436.tif 000117
【０３５５】
、
【０３５６】
【数１１３】
2006172436.tif 000118
【０３５７】
となるようにＢを得る。ｆの範囲が有限なので、
【０３５８】
【数１１４】
2006172436.tif 000119
【０３５９】
は有限の賓辞（ｐｒｅｄｉｃａｔｅ）になる。したがって、Ｂにおけるすべての関係Ｒは有限となる。
【０３６０】
定理６。Σ123：＝Σ12∪Σ23かつσ13＝σ1∪σ3の（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によってＳＯＣＱ=マッピングｍ12、ｍ23が与えられる場合は、次が等価になる。  
１．ｍ：＝ｍ12・ｍ23が（σ1，σ3，Σ13）によって与えられ、Σ13が、Σ123に出現する以外の関数記号または制約を持たないように、署名σ13に対する制約の有限の集合Σ13⊆ＩＣ（ＳＯＣＱ=）がある。  
２．
【０３６１】
【数１１５】
2006172436.tif 000120
【０３６２】
となり、Σ13が、Σ123に出現する以外の関数記号または制約を持たないように、署名σ13に対する制約の有限の集合Σ13⊆ＩＣ（ＳＯＣＱ=）がある。  
３．Σ123├ζを満たすσ13に対するすべてのζについて、多くともｋ回のσ2分解を使用したΣ123からの演繹があるようにｋがある。  
証明。基本的に定理３の証明と同じであり、補助命題１の代わりに下記の補助命題３を用いる。
【０３６３】
補助命題３。定理６の仮定の下では、以下が等価である。  
１．
【０３６４】
【数１１６】
2006172436.tif 000121
【０３６５】
２．
【０３６６】
【数１１７】
2006172436.tif 000122
【０３６７】
定理６は、ＣＱ0=ＣＯＭＰＯＳＥと基本的に同じＳＯＣＱ=マッピングの合成のためのアルゴリズムを示唆し、これをＳＯＣＱ=ＣＯＭＰＯＳＥと呼ぶ。その唯一の違いは、ＳＯＣＱ=ＣＯＭＰＯＳＥはＩＣ（ＳＯＣＱ=）制約に作用するのに対して、ＣＱ0=ＣＯＭＰＯＳＥは、ＩＣ（ＣＱ0=）制約に作用することである。ＳＯＣＱ=ＣＯＭＰＯＳＥの正しさ、このアルゴリズムが終了するための十分条件、およびｇｏｏｄＳＯＣＱ=マッピングは、ＣＱ0=とまったく同じようにＳＯＣＱ=に対して定義される。
【０３６８】
ＣＱ=マッピングの合成  
この項では、ＳＯＣＱ＝マッピングを変換してＣＱ=に戻す方法を検討する。ＣＱマッピングとＣＱ=マッピングの場合を考えられたい。（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられる２つのＣＱ=マッピングｍ12、ｍ23の合成を計算するには、次のように３ステップで進行する。  
手順ＣＱ=ＣＯＭＰＯＳＥ（Σ12，Σ23）  
１．Σ'12：＝ＳＫＯＬＥＭＩＺＥ（Σ12）  
Σ'23：＝ＳＫＯＬＥＭＩＺＥ（Σ23）  
２．Σ'13：＝ＳＯＣＱ=ＣＯＭＰＯＳＥ（Σ'12，Σ'23）  
３．ＤＥＳＫＯＬＥＭＩＺＥ（Σ'13）を返す
最初のステップ、ＳＫＯＬＥＭＩＺＥは容易である。２番目のステップ、ＳＯＣＱ=ＣＯＭＰＯＳＥについては前の項で述べた。３番目のステップ、ＤＥＳＫＯＬＥＭＩＺＥについては、正しいことが示されるアルゴリズムが以下で与えられる（定理７参照）。２番目のステップが成功しても、Σ'13≡Σ13となるようにΣ13⊆ＩＣ（ＣＱ=）を見つけることが不可能である可能性がある。そのため、３番目のステップが成功するための、必要かつ十分な多項式時間で確認できる条件が識別される（命題２参照）。ＤＥＳＫＯＬＥＭＩＺＥは、その入力の大きさに指数関数的な大きさの結果を生成することができる。一般的な事例では、これは避けることができない（定理８参照）が、ＤＥＳＫＯＬＥＭＩＺＥをその入力の大きさで多項式時間で実行するための、多項式時間で確認することができる条件が提供される（命題２参照）。
【０３６９】
次に挙げる従来技術の例は、ｄｅ−Ｓｋｏｌｅｍｉｚａｔｉｏｎが常に可能とは限らないことを示す。
【０３７０】
（実施例７）  
（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられるＣＱ=マッピングｍ12およびｍ23を考えられたい。ここで、  
Σ12は    Ｅ（ｘ，ｙ）→Ｆ（ｘ，ｙ）  
Ｅ（ｘ，ｙ）→∃ｕＣ（ｘ，ｕ）  
Ｅ（ｘ，ｙ）→∃ｖＣ（ｙ、ｖ）であり  
Σ23は    Ｆ（ｘ，ｙ），Ｃ（ｘ，ｕ），Ｃ（ｖ，ｖ）→Ｄ（ｕ，ｖ）である。  
そして、σ1＝｛Ｅ｝，σ2＝｛Ｆ，Ｃ｝，σ3＝｛Ｄ｝である。ここで、ＣＱ=ＣＯＭＰＯＳＥのステップ１および２は成功するが、ｍ12・ｍ23は、当技術分野で示されるようにＣＱ=マッピングでないので、用いられるアルゴリズムに関係なくステップ３は失敗する。
【０３７１】
下記で提示するアルゴリズムＤＥＳＫＯＬＥＭＩＺＥは、├＊に依存し、これは、
【０３７２】
【数１１８】
2006172436.tif 000123
【０３７３】
の何らかの多項式時間の近似である。すなわち、Σ├＊φの場合、
【０３７４】
【数１１９】
2006172436.tif 000124
【０３７５】
となる。この逆は成立しない場合がある。同じく完全であるそのような├＊が存在する既知の事例がある（すなわち逆は成立する）。例えば、Σが階層的な証明を有する場合がある。説明を簡略にするために、├＊の実装についてのオプションについては説明しない。ＤＥＳＫＯＬＥＭＩＺＥは、上記の条件を満たすどの├＊に対しても機能し、すなわち├＊がより完全であるほど、ＤＥＳＫＯＬＥＭＩＺＥが成功する入力の集合が大きくなる。そのため、図８に、本発明によるｄｅＳｋｏｌｅｍｉｚｅの方法論を示す。
【０３７６】
手順ＤＥＳＫＯＬＥＭＩＺＥ（Σ）  
８００でアンネストプロセスが開始される。Λ１：＝｛φ’：φ∈Σ｝と設定し、φ’は、φと等価であり、項を「アンネスト」し、関係アトムと結論から項を取り除くことによって、φから得られ、その結果、φ’では、  
（ａ）関数記号が前提中の等式のみに出現する  
（ｂ）すべての項
【０３７７】
【数１２０】
2006172436.tif 000125
【０３７８】
は、１つのみのアトムに出現する  
（ｃ）すべての等式が、何らかの変数ｖ（ｆについて可変の項）、関数ｆ、および変数の連続
【０３７９】
【数１２１】
2006172436.tif 000126
【０３８０】
（定義式）については形式
【０３８１】
【数１２２】
2006172436.tif 000127
【０３８２】
、または２つの可変項ｕおよびｖ（制約式）については形式ｖ＝ｕになる  
（ｄ）結論は多くとも１つのアトムを含み、それは定義式ではない。  
変数項が出現する関係アトムは、制約アトムと称される。Ａが、ｖが出現する制約関係アトムまたは制約式であり、ｖがｆの変数項である場合、Ａは、ｆを制約するアトムと呼ばれる。制約は、その制約が前提中に制約アトムを含む場合に「制約された」と呼ばれる。
【０３８３】
８０２で、サイクルの確認が行われる。すべてのφ∈Λ1について、グラフＧφを作成し、このグラフでは、辺はφにある変数であり、形式ｖ＝ｆ（．．．ｕ．．．）の形式の等式がある時かつその時に限り辺（ｖ、ｕ）がある。Ｇφがサイクルを有する場合は、終了する。そうでない場合は、Λ2：＝Λ1に設定する。
【０３８４】
８０４で、引数の両立性（ｃｏｍｐａｔｉｂｉｌｉｔｙ）の確認が行われる。すべてのφ∈Λ2について、φが同じ関数記号を有する２つのアトムを含まないことを確認する。同じ関係記号を有する２つのアトムを含む場合は終了する。そうでない場合はΛ3：＝Λ2に設定する。
【０３８５】
８０６で、変数が位置合わせされる。Λ3の変数をリネームして次を満たすΛ4を得る。  
（ａ）Λ4にあるすべての関数記号ｆと、形式ｖ＝
【０３８６】
【数１２３】
2006172436.tif 000128
【０３８７】
および
【０３８８】
【数１２４】
2006172436.tif 000129
【０３８９】
の２つの等式について、ｖは、ｙと同じ変数であり、
【０３９０】
【数１２５】
2006172436.tif 000130
【０３９１】
は
【０３９２】
【数１２６】
2006172436.tif 000131
【０３９３】
と同じ変数の連続である。  
（ｂ）Λ4のすべての２つの異なる関数記号ｆおよびｇと、形式
【０３９４】
【数１２７】
2006172436.tif 000132
【０３９５】
および
【０３９６】
【数１２８】
2006172436.tif 000133
【０３９７】
の任意の２つの等式について、ｖとｙは異なる変数である。  
これが可能でない場合は終了する。
【０３９８】
８０８で、制約アトムが取り除かれる。Λ4における関数記号の何らかの順序付けｆ1，．．．，ｆkを選択する。Δ0＝Λ4に設定する。ｎ＝１，．．．，ｋ−１で、Δn+1：＝｛φ’：φ∈Δn｝と設定し、φ’は、次のようにφから得られる。前提から取り除かれたｆn+1個の制約アトムとともに、ψをφに設定する。Δn├＊ψである場合はφ’：＝ψに設定し、それ以外の場合はφ’：＝φに設定する。いずれの場合も、Δn+1≡Δnになる。Λ5：＝Δkに設定する。
【０３９９】
８１０で、制約アトムを有する制約が除去される。Λ6を、次のテストに従って除去することができない制約の集合φ∈Λ5に設定する。すなわち、φは、次の場合に除去することができる。  
（ａ）φが前提中にｆ制約アトムを含み、かつ  
（ｂ）結論にｆ制約アトムを持ち、前提にｆ制約アトムを持たない制約ψ∈Λ5はない、
８１２で、制約された制約の確認が行われる。Λを、Λ6の制約されない制約の集合に設定する。
【０４００】
【数１２９】
2006172436.tif 000134
【０４０１】
となるようにφ∈Λ6がある場合は終了する。それ以外の場合はΛ7：＝Λに設定する。
【０４０２】
８１４で、従属性の確認が行われる。すべてのφ∈Λ7およびφのすべての変数ｖについて、次のようにＤφ、vを定義する。ｖが変数項でない場合は、Ｄφ,v＝｛ｖ｝に設定する。ｖが変数項であり、
【０４０３】
【数１３０】
2006172436.tif 000135
【０４０４】
がφで定義式である場合は、
【０４０５】
【数１３１】
2006172436.tif 000136
【０４０６】
を設定する。直感的に、Ｄφ,vは、ｖが依存する変数の集合である。Ｖφ：＝φの結論に出現する変数の集合に設定する。Ｖφのすべての変数項ｖについて、Ｄφ,v＝∪u∈vφＤφ,vであることを確認する。これが成立しない場合は終了する。そうでない場合はΛ8：＝Λ7に設定する。
【０４０７】
８１６で従属性が組み合わせられる。
【０４０８】
【数１３２】
2006172436.tif 000137
【０４０９】
と設定し、ψΦは、次のように定義される。すべてのφ∈Φに出現する関数ｆがある場合、ψΦの前提は、Φのすべての前提にあるアトムからなり、ψΦの結論は、Φのすべての結論にあるアトムからなる（重複するアトムは除去する）。そうでない場合、ψΦは、Φにある何らかの制約になる。ψ{φ}＝φなので、Λ9⊇Λ8であることに気づかれたい。
【０４１０】
８１８で、冗長な制約が除去される。すべてのφ∈Λ9についてΛ10├φとなり、これがΛ10のどの真部分集合についても成立しないように、何らかの集合Λ10⊆Λ9を選択する。
【０４１１】
また、８１８で、∃変数を有する関数が置き換えられる。Λ11：＝｛φ’：φ∈Λ10｝と設定し、ここで、φ’の前提は、取り除かれたすべての等式を有するφの前提であり、φ’の結論は、φの結論であり、すべての変数は、存在的に定量化されたφの等式の左側に出現する。
【０４１２】
８２０で、不要な∃変数が除去される。Λ12：＝｛φ’：φ∈Λ11｝と設定し、Λ12を返し、ここで、φ’はφに似るが、結論アトムに出現しない存在的に定量化された変数は除去されている（各自の存在記号とともに）。
【０４１３】
（実施例８）  
ｉ∈｛１，２，３｝についてのアルゴリズムＤＥＳＫＯＬＥＭＩＺＥ
【０４１４】
【数１３３】
2006172436.tif 000138
【０４１５】
の３回の実行を考えられたい。
【０４１６】
【数１３４】
2006172436.tif 000139
【０４１７】
を、次の（アンネストされた）ＳＯＣＱ=従属性の集合とする。  
γ1      Ｒ1（ｖ），Ｒ2（ｘ），ｙ＝ｆ（ｘ）→Ｔ1（ｘ）  
γ2      Ｒ2（ｘ），ｙ＝ｆ（ｘ）→Ｔ2（ｙ）  
γ3      Ｒ2（ｘ），ｙ＝ｆ（ｘ）→Ｒ1（ｙ）  
完全性のために、各
【０４１８】
【数１３５】
2006172436.tif 000140
【０４１９】
は、初めに、下に示す
【０４２０】
【数１３６】
2006172436.tif 000141
【０４２１】
および
【０４２２】
【数１３７】
2006172436.tif 000142
【０４２３】
によって与えられるＣＱ=マッピングをｄｅＳｋｏｌｅｍｉｚｅし、次いでＳＯＣＱ=ＣＯＭＰＯＳＥを呼び出すことによって得られることに留意されたい。
【０４２４】
ｉ  
【０４２５】
【数１３８】
2006172436.tif 000143
【０４２６】
１．｛α1，α2｝          ｛β2｝            ｛γ1｝
２．｛α1，α2｝          ｛β1，β2｝        ｛γ1，γ2｝
３．｛α1，α2，α3｝      ｛β1，β2｝      ｛γ1，γ2，γ3｝
従属性α1、α2、α3、β1、β2は、次のように指定される。
【０４２７】
α1      Ｒ1（ｘ）→Ｓ1（ｘ）
α2      Ｒ2（ｙ）→∃ｚ（Ｓ2（ｚｙ））
α3      Ｓ2（ｚｙ）→Ｒ1（ｚ）
β1      Ｓ2（ｚｙ）→Ｔ2（ｚ）
β2      Ｓ1（ｘ），Ｓ2（ｘｙ）→Ｔ1（ｙ）
ＤＥＳＫＯＬＥＭＩＺＥ
【０４２８】
【数１３９】
2006172436.tif 000144
【０４２９】
の３回の実行すべてで、γ1、γ2、γ3はそれぞれ、サイクルがなく、同じ関数記号を有する複数のアトムを持たないので、プロセス８０２と８０４は通過する。従属性の変数名はすでに位置合わせされているので、プロセス８０６は、効果がない。残りのプロセスについては以下で説明する。
【０４３０】
実行されるＤＥＳＫＯＬＥＭＩＺＥ（｛γ1｝）で、｛γ1｝は単集合なので、プロセス８０８は効果がない。結論にｆ制約アトムを有する規則は｛γ1｝にないので、その唯一のメンバγ1は、プロセス８１０で除去される。直感的に、γ1は、その範囲がＲ1と互いに素であるｆを合成することができるので、γ1はトートロジーである。したがって、｛γ1｝は、ＩＣ（ＣＱ）に自明に存在する、制約の空集合に等しい。
【０４３１】
実行されるＤＥＳＫＯＬＥＭＩＺＥ（｛γ1，γ2｝）で、γ2は、その結論にｆ制約アトムＴ2を含む。したがって、制約される制約γ1は、プロセス８１０で除去されることができず、そのためｄｅＳｋｏｌｅｍｉｚｅはプロセス８１２で終了する。
【０４３２】
実行されるＤＥＳＫＯＬＥＭＩＺＥ（｛γ1，γ2，γ3｝）では、γ2にも関わらずｄｅＳｋｏｌｅｍｉｚｅが可能である。プロセス８０８では、Δ0＝｛γ1，γ2，γ3｝になる。唯一の関数記号ｆを考慮することにより、Δ1＝｛ψ、γ2，γ3｝≡Δ0を得、ψは、次のようにγ1の前提から制約アトムＲ1（ｙ）を除去することにより得られる。  
ψ：＝Ｒ2（ｘ），ｙ＝ｆ（ｘ）→Ｔ1（ｘ）
Δ0⊃｛γ1，γ3｝├＊ψなので、明らかにΔ0├＊ψである。Δ1は制約を加える制約を持たず、プロセス８１０は効果がなく、プロセス８１２が通過する。Δ1のすべての従属性は、その結論に、多くとも１つの変数項を有するので、プロセス８１４は、Λ8＝Λ7＝｛ψ、γ2，γ3｝で成功する。例えば、γ3についてこの計算を行うと、Ｖγ3＝｛ｘ，ｙ｝，Ｄγ3,x＝Ｄγ3,y＝∪u∈Vγ3Ｄγ3,u＝｛ｘ｝が得られる。プロセス８１６で、Φ＝Λ8についての従属性を組み合わせると、  
γ4：＝Ｒ1（ｖ），Ｒ2（ｘ），ｙ＝ｆ（ｘ）→Ｔ1（ｘ），Ｔ2（ｙ），Ｒ1（ｙ）
が得られる。
【０４３３】
（紙面を簡略化するために、Λ8の真部分集合から得られる組合せは示さない。）プロセス８１８で、それらは、γ4と前提を共有し、その結論は、γ4の結論によって包摂されるので、ψ、γ2、γ3を含む冗長な制約が除去され、その結果はΛ10＝｛γ4｝となる。最後に、８１８で、γ4の存在変数で関数ｆを置き換えることにより、  
Λ12＝｛Ｒ2（ｘ）→∃ｙ（Ｔ1（ｘ）∧Ｔ2（ｙ）∧Ｒ1（ｙ））｝  
が得られる。  
したがって、ＤＥＳＫＯＬＥＭＩＺＥ（｛γ1，γ2，γ3｝）⊆ＩＣ（ＣＱ）となる。
【０４３４】
定理７。入力Σ⊆ＩＣ（ＳＯＣＱ=）にＤＥＳＫＯＬＥＭＩＺＥ（Σ）が成功する場合、Σ’：＝ＤＥＳＫＯＬＥＭＩＺＥ（Σ）は次を満たす。  
Σ’⊆ＩＣ（ＣＱ=）かつΣ’≡Σ  
このアルゴリズムの説明から次が得られる。
【０４３５】
命題３。  
１．ＤＥＳＫＯＬＥＭＩＺＥ（Σ）は、プロセス８１６に達する場合かつその場合に限り、入力Σ⊆ＩＣ（ＳＯＣＱ=）に成功し、これは、Σの大きさで多項式時間で確認することができる。  
２．さらに、Σに依存しない何らかの制約ｌについて、Λ8のすべての関数記号について、ｆが出現するΛ8にｌより多くの規則がある場合、ＤＥＳＫＯＬＥＭＩＺＥ（Σ）は、Σの大きさの多項式時間で実行される。
【０４３６】
命題３の最初の部分から、ＳＫＯＬＥＭＩＺＥの結果の大きさは、その入力の大きさに多項式であり、また、ＳＯＣＱ=ＣＯＭＰＯＳＥ（Σ'12，Σ'23）が終了するための十分条件を多項式時間で調べることができるので、ＣＱ=ＣＯＭＰＯＳＥ（Σ12，Σ23）が成功するための十分条件は、多項式時間で調べることができることになる。
【０４３７】
ＤＥＳＫＯＬＥＭＩＺＥ（Σ）は、プロセス８１６のためにΣの大きさに指数関数的な大きさの結果を生成することができるので、ＣＱ＝ＣＯＭＰＯＳＥ（Σ12，Σ23）は、Σ12∪Σ23の大きさに指数関数的な大きさの結果を生成することができる。次の例は、一般的な事例ではこれが避けられないことを示す。しかし、命題３の２番目の部分は、ＤＥＳＫＯＬＥＭＩＺＥが成功することだけでなく、それが多項式時間で終了することも保証するより厳格な条件を効率的に調べることができることを示す。
【０４３８】
定理８。任意の準指数関数的な関数ｆについて、ｍ13：＝ｍ12・ｍ23が大きさがｆ（ｓ）未満であるΣ13について（σ1，σ3，Σ13）によって与えられないＣＱマッピングになるように、（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられる、ソースからターゲットへのＣＱマッピングｍ12およびｍ23があり、ｓは、Σ12∪Σ23の大きさである。
【０４３９】
証明。（概要）ｆ（２ｋｌ）＜２kとなり、ｌが最も長い制約の大きさとなるのに十分な大きさのｋを選択する（９は、約１８＋ｌｏｇ  ｋ文字の長さである）。ｆが準指数関数的なので、そのようなｋは必ず存在することになる。［ｋ］：＝｛１，．．．，ｋ｝と設定する。（σ1，σ2，Σ12）および（σ2，σ3，Σ23）によって与えられるＣＱ=マッピングｍ12およびｍ23を考えられたい。ここで、  
Σ12は      Ｒ0（ｘ）→∃ｙＳ0（ｘｙ）  
Ｒi（ｘ）→Ｓi（ｘ）であり  
Σ23は      Ｓ0（ｘｙ），Ｓi（ｘ）→Ｔi（ｙ）    である。  
ｉ∈［ｋ］であり、σ1＝｛Ｒi：ｉ∈｛０，．．．，ｋ｝｝、σ2＝｛Ｓi：ｉ∈｛０，．．．，ｋ｝｝であり、σ3＝｛Ｔi：ｉ∈［ｋ］｝である。合成ｍ13：＝ｍ12・ｍ13は、Ｚ⊆［ｋ］となるように、制約  
Ｒ0（ｘ），Ｒz（ｘ）→∃ｙＴz（ｙ）  
の集合Σ13によって与えられ、Ｒｚ（ｘ）：＝∧i∈zＲi（ｘ）であり、Ｔ2も同様である。一方、Σが２k−１個より少ない制約を有する場合は、ｍ13は、どの（σ1，σ3，Σ）によっても与えられない。
【０４４０】
ドメイン、範囲、および他の演算子  
合成は、入力としてモデルおよび／またはマッピングを受け取り、出力としてモデルおよび／またはマッピングを与える演算子の１つである。合成は、他の演算子の組合せを使用して行うことができ、他の演算子は、上記で概説した手法と同様の手法を用いて実施することができる。そうした他の演算子には次が含まれる。  
ドメイン    ｄｏｍ（ｍ）  
範囲        ｒｎｇ（ｍ）  
交差        Ａ∩Ｂ  
同一        ｉｄ（Ａ）  
直交積      Ａ×Ｂ  
交差        ｍ1∩ｍ2 
逆          ｍ-1
これらの演算子は次のように定義される。  
ｄｏｍ（ｍ）：＝｛Ａ：∃Ｂ＜Ａ，Ｂ＞∈ｍ｝  
ｒｎｇ（ｍ）：＝｛Ｂ：∃Ａ＜Ａ，Ｂ＞∈ｍ｝  
Ａ∩Ｂ：＝｛Ａ：Ａ∈Ａ，Ａ∈Ｂ｝  
ｉｄ（Ａ）：＝｛＜Ａ，Ａ＞：Ａ∈Ａ｝  
Ａ×Ｂ：＝｛＜Ａ，Ｂ＞：Ａ∈Ａ，Ｂ∈Ｂ｝  
ｍ1∩ｍ2：＝｛＜Ａ，Ｂ＞：＜Ａ，Ｂ＞∈ｍ1＜Ａ，Ｂ＜∈ｍ2｝  
ｍ-1：＝｛＜Ｂ，Ａ＞：＜Ａ，Ｂ＞∈ｍ｝
署名を伴う関係の事例では、すべてのモデルに署名が関連付けられ、すべてのマッピングに対する入力署名および出力署名、および上記の演算子に対する明白な署名互換性の条件が必要とされる。
【０４４１】
命題４。すべてのＬ⊇ＣＱ0は、同一、直交積、および交差の下で閉じる。  
証明。ｍ12とｍ34が（σ1，σ2，Σ12）および（σ3，σ4，Σ34）によって与えられ、ＡとＢが（σ1，Σ1）および（σ2，Σ2）によって与えられる場合、  
・  Ａ×Ｂは（σ1，σ2，Σ1∪Σ2）によって与えられる  
・  Ａ∩Ｂは（σ1，Σ1∪Σ2）によって与えられる（この場合σ1＝σ2）  
・  ｍ12∩ｍ34は（σ1，σ2，Σ12∪Σ34）によって与えられる（この場合σ1＝σ3、σ2＝σ4）
同一を表すには、σ2のすべての関係記号Ｒについて同一ａｒｉｔｙの関係記号Ｒを含む３番目の補助署名σ'2を参照し（この署名は通常は無視される）。この場合は、σ1＝σ2であり、したがってσ'2＝σ'1となる。  
・  ｉｄ（Ａ）は（σ1，σ1，σ'1，Σ1∪Σ）によって与えられ、Σは、σ1のすべてのＲについて、形式
【０４４２】
【数１４０】
2006172436.tif 000145
【０４４３】
の２つの制約からなる。
【０４４４】
命題５。合成、範囲、およびドメインの演算子はそれぞれ、どの互いの演算子にも変形されることができる。  
証明。  
・  ｍ12が（σ1，σ2，Σ12）によって与えられる  
・  ｍ23が（σ2，σ3，Σ23）によって与えられる  
と仮定する。  
・  ｍ1が（σ1∪σ3，σ2，Σ12∪Σ23）によって与えられ  
・  ｍ2が（σ2，σ1∪σ3，Σ12∪Σ23）によって与えられ  
・  ｄｏｍ（ｍ1）が（σ1∪σ3，Σ1）によって与えられ  
・  ｒｎｇ（ｍ2）が（σ1∪σ3，Σ2）によって与えられる  
とする  
すると、ｍ12およびｍ23は、（σ1，σ3，Σ1）および（σ1，σ3，Σ2）によって与えられる。  
これは、合成はドメインまたは範囲のいずれでも表すことができることを証明する。
【０４４５】
逆に、  
・  ｍ12が（σ1，σ2，Σ12）によって与えられる  
と仮定し、  
・  ｍ21が
【０４４６】
【数１４１】
2006172436.tif 000146
【０４４７】
によって与えられ  
・  ｍ12・ｍ21が（σ1，σ1，Σ1）によって与えられ  
・  ｍ21・ｍ12が（σ2，σ2，Σ2）によって与えられるとする  
すると、ｄｏｍ（ｍ12）とｒｎｇ（ｍ12）はそれぞれ  
（σ1，Σ1）と（σ2，Σ2）  
によって与えられる。  
これは、ドメインと範囲は、合成で表すことができることを証明する。
【０４４８】
考慮されるすべての言語は、命題４の前提を満たす。そのため、命題５は、合成および逆の下での閉鎖に注目することができることを意味する。Ｌマッピングｍが（σ1，σ2，Σ12）によって与えられる場合、その逆は、（σ2，σ1，Σ12）によって与えられることに気づかれたい。しかし、Ｌに対する制約は、２番目の式がもはやＬマッピングを与えないような制約である場合がある。例えば、これは、「ソースからターゲット」への式で生じる。それに対し、ＣＱ0=、ＣＱ=、およびＳＯＣＱ=マッピングは、逆の下で閉じるので、合成を研究すれば十分である。
【０４４９】
命題５は、ドメインと範囲を実施するために用いることができるアルゴリズム手順を合成を実施するために展開できることを示唆する。これは、上記で提示したアルゴリズムを呼び出すことによって直接実現するか、または、まずドメインと範囲の演算子を実行し、次いでその結果を用いて合成を得ることによって間接的に実現することができる。
【０４５０】
コンピューティング環境  
次いで図９を参照すると、ここに開示されるアーキテクチャを実行するように動作することが可能なコンピュータのブロック図が示される。本発明の各種態様の追加的コンテクストを提供するために、図９と以下の説明では、本発明の各種態様が実施されることができる適切なコンピューティング環境９００の簡単で概略的な説明を提供する。上記では、本発明について、１つまたは複数のコンピュータで実行することが可能なコンピュータ実行可能命令の一般的文脈で説明したが、当業者は、本発明は、他のプログラムモジュールと組み合わせて、かつ／またはハードウェアとソフトウェアの組合せとして実施してもよいことを認識されよう。
【０４５１】
一般に、プログラムモジュールには、特定のタスクを行うか、特定の抽象データ型を実装する、ルーチン、プログラム、コンポーネント、データ構造などが含まれる。さらに、当業者は、本発明の方法は、シングルプロセッサまたはマルチプロセッサのコンピュータシステム、ミニコンピュータ、メインフレームコンピュータ、ならびにパーソナルコンピュータ、ハンドヘルドコンピューティングデバイス、マイクロプロセッサを利用した、あるいは設定可能な家電製品などを含む他のコンピュータシステム構成で実施することができ、これらのデバイスはそれぞれ、１つまたは複数の関連付けられたデバイスに動作可能に結合できることを理解されよう。
【０４５２】
ここに例示される本発明の態様は、通信ネットワークを通じて結ばれた遠隔の処理デバイスによって一定のタスクが行われる分散コンピューティング環境で実施してもよい。分散コンピューティング環境では、プログラムモジュールは、ローカルおよびリモート両方のメモリ記憶装置に置くことができる。
【０４５３】
コンピュータは、通例各種のコンピュータ可読媒体を含む。コンピュータ可読媒体は、コンピュータによるアクセスが可能な利用可能媒体でよく、揮発性および不揮発性、取り外し可能および取り外し不能の媒体を含む。限定ではなく例として、コンピュータ可読媒体は、コンピュータ記憶媒体と通信媒体からなることができる。コンピュータ記憶媒体には、コンピュータ可読命令、データ構造、プログラムモジュール、または他のデータなどの情報を記憶するための方式または技術として実施された、揮発性および不揮発性、取り外し可能および取り外し不能の媒体が含まれる。コンピュータ記憶媒体には、これらに限定しないが、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、フラッシュメモリ、または他のメモリ技術、ＣＤ−ＲＯＭ、デジタルビデオディスク（ＤＶＤ）、または他の光ディスク記憶、磁気カセット、磁気テープ、磁気ディスク記憶、または他の磁気記憶装置、または必要な情報を記憶するために用いることができ、コンピュータからのアクセスが可能な他の媒体が含まれる。
【０４５４】
通信媒体は通例、コンピュータ可読命令、データ構造、プログラムモジュール、または他のデータを、搬送波や他の移送機構などの変調データ信号として実施し、任意の情報伝達媒体を含む。用語「変調データ信号」とは、信号中に情報を符号化するような方式で特性の１つまたは複数を設定または変化させた信号を意味する。限定ではなく例として、通信媒体には、有線ネットワークや直接配線接続などの有線媒体と、音響、ＲＦ、赤外線、他の無線媒体などの無線媒体が含まれる。上記の媒体の組合せもコンピュータ可読媒体の範囲に含める。
【０４５５】
再度図９を参照すると、コンピュータ９０２を含む、本発明の各種態様を実施する例示的環境９００が示され、コンピュータ９０２は、処理装置９０４、システムメモリ９０６、およびシステムバス９０８を含む。システムバス９０８は、これに限定しないがシステムメモリ９０６を含むシステムコンポーネントを処理装置９０４に結合する。処理装置９０４は、各種の市販プロセッサのいずれでもよい。デュアルマイクロプロセッサおよび他のマルチプロセッサアーキテクチャも処理装置９０４として用いてよい。
【０４５６】
システムバス９０８は、各種の市販のバスアーキテクチャを用いてさらにメモリバス（メモリコントローラを備える場合も備えない場合もある）、ペリフェラルバス、およびローカルバスと相互接続することができる数種のバス構造のいずれでもよい。システムメモリ９０６は、読み取り専用メモリ（ＲＯＭ）９１０とランダムアクセスメモリ（ＲＡＭ）９１２を含む。ＲＯＭ、ＥＰＲＯＭ、ＥＥＰＲＯＭなどの不揮発性メモリ９１０に基本入出力システム（ＢＩＯＳ）が記憶され、このＢＩＯＳは、起動時などにコンピュータ９０２内の要素間の情報転送を助ける基本ルーチンを含んでいる。ＲＡＭ９１２は、データをキャッシュするためのスタティックＲＡＭなどの高速ＲＡＭも含むことができる。
【０４５７】
コンピュータ９０２はさらに、外部で使用するために適切なシャーシ（図示せず）に入れて構成してもよい内部ハードディスクドライブ（ＨＤＤ）９１４（ＥＩＤＥ、ＳＡＴＡなど）、（例えば取り外し可能ディスケット９１８の読み書きを行う）磁気フロッピー（登録商標）ディスクドライブ（ＦＤＤ）９１６、および（例えばＣＤ−ＲＯＭディスク９２２を読み取る、あるいはＤＶＤなどの他の高容量光学媒体の読み書きを行う）光ディスクドライブ９２０を含む。ハードディスクドライブ９１４、磁気ディスクドライブ９１６、および光ディスクドライブ９２０は、それぞれハードディスクドライブインターフェース９２４、磁気ディスクドライブインターフェース９２６、光ドライブインターフェース９２８でシステムバス９０８に接続することができる。外部ドライブ実装のためのインターフェース９２４は、ＵＳＢ（ユニバーサルシリアルバス）とＩＥＥＥ１３９４インターフェース技術の少なくとも１つまたは両方を含む。
【０４５８】
これらのドライブとそれに関連付けられたコンピュータ可読媒体は、データ、データ構造、コンピュータ実行可能命令などの不揮発性の記憶を提供する。コンピュータ９０２のために、これらのドライブと媒体は、適切なデジタルフォーマットでのデータ記憶に対応する。上記のコンピュータ可読媒体の説明では、ＨＤＤ、取り外し可能磁気ディスケット、およびＣＤやＤＶＤなどの取り外し可能光学媒体を挙げたが、当業者には、ｚｉｐドライブ、磁気カセット、フラッシュメモリカード、カートリッジなど、コンピュータ可読の他のタイプの媒体も例示的動作環境で使用してよく、さらに、そうした媒体は、本発明の方法を行うためのコンピュータ実行可能命令を含むことができることが認識されよう。
【０４５９】
これらのドライブおよびＲＡＭ９１２には複数のプログラムモジュールを記憶することができ、これにはオペレーティングシステム９３０、１つまたは複数のアプリケーションプログラム９３２、他のプログラムモジュール９３４、およびプログラムデータ９３６が含まれる。オペレーティングシステム、アプリケーション、モジュール、および／またはデータのすべてまたは一部は、ＲＡＭ９１２にキャッシュされることもできる。本発明は、各種の市販オペレーティングシステム、またはオペレーティングシステムの組合せで実施できることが理解されよう。
【０４６０】
ユーザは、例えばキーボード９３８や、マウス９４０などのポインティングデバイスなどの１つまたは複数の有線／無線入力装置を通じて、コンピュータ９０２にコマンドと情報を入力することができる。他の入力装置（図示せず）としては、マイクロフォン、ＩＲリモートコントロール、ジョイスティック、ゲームパッド、スタイラスペン、タッチスクリーンなどが可能である。上記および他の入力装置は、多くの場合、システムバス９０８に結合された入力装置インターフェース９４２を通じて処理装置９０４に接続されるが、パラレルポート、ＩＥＥＥ１３９４シリアルポート、ゲームポート、ＵＳＢポート、ＩＲインターフェースなどの他のインターフェースで接続することができる。
【０４６１】
モニタ９４４または他のタイプの表示装置も、ビデオアダプタ９４６などのインターフェースを介してシステムバス９０８に接続される。モニタ９４４に加えて、コンピュータは通例、スピーカやプリンタなどの他の周辺出力装置（図示せず）を含む。
【０４６２】
コンピュータ９０２は、有線および／または無線通信を介した、リモートコンピュータ９４８などの１つまたは複数のリモートコンピュータとの論理接続を使用するネットワーク環境で動作することができる。リモートコンピュータ９４８は、ワークステーション、サーバコンピュータ、ルータ、パーソナルコンピュータ、携帯型コンピュータ、マイクロプロセッサを利用した娯楽機器、ピアデバイス、あるいは他の一般的なネットワークノードであり、図を簡略にするためにメモリ記憶装置９５０のみを示すが、通例は、コンピュータ９０２との関連で上述した要素の多くまたはすべてを含む。図の論理接続は、ローカルエリアネットワーク（ＬＡＮ）９５２および／または例えばワイドエリアネットワーク（ＷＡＮ）９５４などのより大きなネットワークへの有線／無線接続性を含む。このようなＬＡＮおよびＷＡＮネットワーキング環境は、オフィスや企業などで一般的であり、イントラネットなどの企業内コンピュータネットワークを容易にし、企業内ネットワークはすべて、インターネットなどの世界規模の通信ネットワークに接続することができる。
【０４６３】
ＬＡＮネットワーキング環境で使用される場合、コンピュータ９０２は、有線および／または無線の通信ネットワークインターフェースあるいはアダプタ９５６を通じてローカルネットワーク９５２に接続される。アダプタ９５６は、ＬＡＮ９５２との有線または無線通信を助けることができ、ＬＡＮは、無線アダプタ９５６と通信するための、ネットワーク内に配置された無線アクセスポイントを含むこともできる。
【０４６４】
ＷＡＮネットワーキング環境で使用される場合、コンピュータ９０２は、モデム９５８を含むか、またはＷＡＮ９５４上の通信サーバと接続されるか、または、インターネットを介するなどしてＷＡＮ９５４を通じて通信を確立するための他の手段を備える。モデム９５８は、内蔵型でも外付け型でも、有線デバイスでも無線デバイスでもよく、シリアルポートインターフェース９４２を介してシステムバス９０８に接続される。ネットワーク環境では、コンピュータ９０２との関連で図示するプログラムモジュールまたはその一部は、遠隔のメモリ／記憶装置９５０に記憶することができる。図のネットワーク接続は例示的なものであり、コンピュータ間に通信リンクを確立する他の手段を用いてよいことは理解されよう。
【０４６５】
コンピュータ９０２は、例えばプリンタ、スキャナ、デスクトップおよび／またはポータブルコンピュータ、携帯情報端末、通信衛星、無線検出可能タグに関連付けられた機器または場所（キオスク、新聞販売スタンド、洗面所など）、電話器など、無線通信に動作可能に配置された無線デバイスまたはエンティティと通信するように動作することができる。これには、Ｗｉ−ＦｉまたはＢｌｕｅｔｏｏｔｈ（商標）無線技術の少なくとも１つが含まれる。したがって、通信は、従来のネットワークのようなあらかじめ定義された構造であっても、単に、少なくとも２つのデバイス間のその場限りの通信であってもよい。
【０４６６】
Ｗｉ−ＦｉあるいはＷｉｒｅｌｅｓｓ  Ｆｉｄｅｌｉｔｙは、自宅のソファ、ホテル客室のベッド、あるいは職場の会議室から、配線なしでインターネットに接続することを可能にする。Ｗｉ−Ｆｉは、例えばコンピュータなどのデバイスが、基地局の範囲内のどの場所でも、屋内および屋外でデータの送受信を可能にする携帯電話で用いられる技術と同様の無線技術である。Ｗｉ−Ｆｉネットワークは、ＩＥＥＥ８０２．１１（ａ、ｂ、ｇなど）と称される無線技術を使用して、安全で、信頼性があり、高速の無線接続を提供する。Ｗｉ−Ｆｉネットワークを使用して、コンピュータ同士を接続する、コンピュータをインターネット、および無線ネットワーク（ＩＥＥＥ８０２．３またはイーサネット（登録商標）を使用する）に接続することができる。Ｗｉ−Ｆｉネットワークは、許可の不要な２．４および５ＧＨｚ無線帯域で、１１Ｍｂｐｓ（８０２．１１ａ）または５４Ｍｂｐｓ（８０２．１１ｂ）のデータレートで、または両方の帯域を含む製品（デュアルバンド）とともに動作し、そのため、このネットワークは、多くのオフィスで使用される１０ＢａｓｅＴ有線イーサネット（登録商標）ネットワークと同様の現実世界での性能を提供することができる。
【０４６７】
次いで図１０を参照すると、本発明による例示的コンピューティング環境１０００の概略ブロック図が示される。システム１０００は、１つまたは複数のクライアント１００２を含む。クライアント１００２は、ハードウェアおよび／またはソフトウェア（スレッド、プロセス、コンピューティングデバイスなど）である。クライアント１００２は、例えば、本発明を用いることにより、クッキーおよび／または関連付けられたコンテクスト情報を保持することができる。
【０４６８】
システム１０００は、１つまたは複数のサーバ１００４も含む。サーバ１００４もハードウェアおよび／またはソフトウェア（スレッド、プロセス、コンピューティングデバイスなど）である。サーバ１００４は、例えば、本発明を用いることにより、変換を行うスレッドを保持することができる。クライアント１００２とサーバ１００４間で可能な通信の１つは、２つ以上のコンピュータプロセス間で送信されるように適合されたデータパケットの形態である。データパケットは、例えば、クッキーおよび／または関連付けられたコンテクスト情報を含むことができる。システム１０００は、クライアント１００２とサーバ１００４間の通信を助けるために用いることができる通信フレームワーク１００６（インターネットなどの世界規模の通信ネットワーク）を含む。
【０４６９】
通信は、有線技術（光ファイバを含む）および／または無線技術を介して容易にすることができる。クライアント１００２は、クライアント１００２にとってローカルな情報（クッキーおよび／または関連付けられたコンテクスト情報など）を記憶するために用いることができる１つまたは複数のクライアントデータストア１００８に動作可能に接続される。同様に、サーバ１００４は、サーバ１００４にとってローカルな情報を記憶するために用いることができる１つまたは複数のサーバデータストア１０１０に動作可能に接続される。
【０４７０】
上記の説明は、本発明の例を含む。言うまでもなく、本発明を説明する目的で構成要素または方法論の着想可能な組合せをすべて記載することは不可能であり、当業者は、本発明のさらなる多くの組合せまたは置き換えが可能であることを認識されよう。そのため、本発明は、添付の特許請求の範囲に該当するそのような改変、変更、および変形をすべて包含するものとする。さらに、用語「〜を含む」が詳細な説明または特許請求の範囲で用いられる限りでは、この語は、用語「〜を備える」が請求項で接続語として用いられる時の解釈と同様に包含的な意味とする。
【図面の簡単な説明】
【０４７１】
【図１】本発明による、データベーススキーマ間で２つの既存のマッピングの合成を使用して結果得られるマッピングの構成を表す図である。
【図２】本発明による論理的制約のマッピング合成を表す図である。
【図３】本発明による従属性の合成の方法を示す図である。
【図４】条件を課し、確認を用いて合成が正しい答えで終了するかどうかを判定する、本発明による合成方法の図である。
【図５】本発明による、有限の公理化にｄｅＳｋｏｌｅｍｉｚｅを行って局所従属性を得る方法を示す図である。
【図６】本発明による４つ以上のデータソーススキーマに対する複数の合成の図である。
【図７】本発明による、アルゴリズムの１回の呼び出しを使用して行って出力マッピングを得ることができる複数マッピングの合成の図である。
【図８】本発明によるｄｅＳｋｏｌｅｍｉｚｅの方法論を説明する図である。
【図９】ここに開示されるアーキテクチャを実行するように動作可能なコンピュータのブロック図である。
【図１０】本発明による例示的コンピューティング環境の概略ブロック図である。
【符号の説明】
【０４７２】
１０４  スキーママッピング12（関数、非関数、非関数）
１０６  （非関数、関数、非関数）スキーママッピング23
１０８  合成コンポーネント
１０２  スキーママッピング13
２０２  データベーススキーマ（Ｓ1〜Ｓ3）
２０４  マッピング12（完全従属性、局所従属性、および／または２次従属性）
２０６  マッピング23（完全従属性、局所従属性、および／または２次従属性）
２０８  合成コンポーネント
２１０  マッピング13
７０４  合成コンポーネント
９０４  処理装置
９０６  システムメモリ
９０８  バス
９１４  内部ＨＤＤ
９１８  ディスク
９２０  光学ドライブ
９２２  ディスク
９２４  インターフェース
９２６  インターフェース
９２８  インターフェース
９３０  オペレーティングシステム
９３２  アプリケーション
９３４  モジュール
９３６  データ
９３８  キーボード
９４０  マウス
９４２  入力装置インターフェース
９４４  モニタ
９４６  ビデオアダプタ
９４８  リモートコンピュータ
９５０  メモリ／ストレージ
９５６  ネットワークアダプタ
９５８  モデム
１００２  クライアント
１００４  サーバ
１００６  通信フレームワーク
１００８  クライアントデータストア
１０１０  サーバデータストア
【図１】
2006172436.tif 000147
【図２】
2006172436.tif 000148
【図３】
2006172436.tif 000149
【図４】
2006172436.tif 000150
【図５】
2006172436.tif 000151
【図６】
2006172436.tif 000152
【図７】
2006172436.tif 000153
【図８】
2006172436.tif 000154
【図９】
2006172436.tif 000155
【図１０】
2006172436.tif 000156