用于对依存关系所给出的映射关系进行合成的系统和方法

摘要

一种便于对模式映射关系进行合成的系统。提供一种用于合成一类宽泛的映射关系的一般算法，其中两个映射关系之一或两者不是函数，而是诸如两种模式之间的约束和函数之逆等的约束。一种合成组件对若干异类数据源的模式映射关系进行合成，这些模式映射关系可由完全、嵌入和二阶依存关系中的至少一种来表达，其中二阶依存关系无须是源到目标的形式。此用于合成的算法还包括测试该合成算法是否将终止的过程。

说明书

技术领域

本发明涉及在数据库模式之间构造映射关系的系统和方法，其中所述映射是从若干现有映射合成的。

背景技术

诸如因特网等全球通信网络的出现方便人们访问大量的数据。世界充斥着各种信息源，在许多情况中，数据在不同数据源之间被以不同形式表示。如今在有线和无线领域中盛行的自由信息流要求在存储和解释数据以供使用的范围内源和目的是兼容的。如今公司和个人所面对的一个主要问题是存在于一种模型/模式的数据需要经由另一种不同的模型/模式被访问。但是，此类过程被很大程度上异类的并且不停改变的模型/模式集合所牵制。在数据仓库式处理中可找到这样一个例子，其中从许多不同的源接收数据，用于存储和从其它各种源进行快速访问。将数据从一种模型转换为另一种模型不仅耗费时间而且是占有大量资源的，但却伴随着各种转换问题。

模式映射关系指定异类数据库源之间的关系，并被用于支持数据转换、数据交换、模式进化、约束检查、以及其它任务。映射关系合成是一种操作，它取模式A、B、C之间的两个映射关系map_AB和map_BC作为输入，并产生由合成的映射关系map_AB和map_BC所给出的、指定A和C之间同一组约束的单个映射关系map_AC。

为说明映射关系合成的用途，考虑以下模式进化情形。假定S₁、S₂、S₃、S₄是一个产品逐次发布中使用的模式的版本。映射关系map₁₂用来将数据从模式S₁的格式转移到模式S₂的格式。类似地，映射关系map₂₃用来将数据从模式S₂的格式转移到模式S₃的格式，最后，映射关系map₃₄用来将数据从模式S₃的格式转移到模式S₄的格式。将数据从版本S₁的格式转移到版本S₄的常规方法是通过依此执行map₁₂、map₂₃、map₃₄，这是耗费时间并且成本高昂的。为了将数据从S₁单步转移到S₄，则需要映射关系合成。映射关系map₁₄可通过首先合成map₁₂和map₂₃，然后与map₃₄合成最终映射关系。

现在假定V₁是S₁上所定义的视图，且map_1V1是一个函数。为将视图V₁从S₁转移到S₂，再次使用合成。将映射关系map₁₂的逆与map_1V1合成以获得从S₂到V₁的映射关系map_2V1。

对于每个映射关系都是一个函数(即，将一个数据库状态精确映射到另一数据库状态，且两个映射关系都具有相同的方向性)的情况而言，用于进行映射关系合成的各种算法是公知的。但是，对于适用于其中两个映射关系之一或两者都不是函数的一类较宽泛的映射关系的算法仍有极大的未被满足的需求。

发明内容

以下给出本发明的简化的概述，以提供对本发明的一些方面的基本理解。此概述不是本发明的详尽综览。它不试图标识本发明的关键性/决定性元素，或界定本发明的范围。它唯一的目的是以简化形式给出本发明的一些概念，作为对稍后给出的更详细的描述的序言。

本发明是适用于合成一类较宽泛的映射关系的一种普遍算法，其中两个映射关系之一或者两者都不是函数，而是诸如两种模式之间的约束和函数之逆等。这允许通过合成两个现有映射关系，来从其构造两个数据库模式之间的映射关系。此用于合成的算法包括测试该合成算法是否将终止的程序。

在本文中所揭示和要求保护的本发明的一个方面包括一种便于对模式映射关系进行合成的系统。合成组件对若干异类数据源的现有模式映射关系进行合成，这些模式映射关系可由完全、嵌入、和二阶依存关系中的至少一种来表达，其中二阶依存关系无须是源到目标的形式。

在本发明的另一个方面，提供一种方法，用于通过以下动作来提供两种模式映射关系的合成：将由嵌入依存关系表达的模式映射关系斯柯伦化(Skolemize)以获得由二阶依存关系表达的模式映射关系；计算输入和输出签名上所有约束的有穷公理，该公理可从给出这些模式映射关系的约束来推导；以及将有穷公理解除斯柯伦化(de-Skolemize)以获得由嵌入依存关系表达的模式映射关系。

在本发明的又一个方面，提供一种方法，其中将有穷公理去斯柯伦化的动作还包括通过以下动作来将斯柯伦(Skolem)函数解嵌套以生成结论：检查结论中的所有变量是否都出现在斯柯伦函数的变量依存关系集合中；生成可通过统一在结论中出现的斯柯伦函数获得的所有可能的子句；以及通过用新的存在变量代换每个斯柯伦项将每个子句单独去斯柯伦化。

为实现前述及有关目的，本文中结合以下描述和附图描述本发明的某些示例性方面。但是，这些方面仅仅示意可使用本发明原理的各种方法中的若干种，并且本发明旨在包括所有这些方面及其等效技术方案。当结合附图考虑时，从以下对本发明的详细描述，本发明的其它优点和新颖特征将变得显而易见。

附图说明

图1示出根据本发明通过合成数据库模式之间两个现有映射关系来构造结果映射关系的示意图。

图2示出根据本发明给出的逻辑约束映射关系合成的示意图。

图3示出根据本发明的一种合成依存关系的方法。

图4示出根据本发明的一种合成方法，该方法强加条件并使用检查来确定合成是否终止于正确的答案。

图5示出根据本发明一种方法，该方法执行对有穷公理进行解除斯柯伦化以获得嵌入依存关系。

图6示出根据本发明的三个以上数据源模式上的多重合成的示意图。

图7示出根据本发明可通过使用算法的单次调用来执行的多重映射关系的合成，以获得输出映射关系。

图8示出根据本发明的一种用于解除斯柯伦化的方法。

图9示出可用于执行所揭示体系结构的计算机的框图。

图10示出根据本发明的一种示例性计算环境的示意性框图。

具体实施方式

现在参考附图描述本发明，贯穿所有附图使用相同的标号来指相同的元素。在以下描述中，为解释目的，阐述许多具体细节以提供对本发明的详尽理解。但是，显然无需这些具体细节也可实施本发明。在其它实例中，公知的结构和设备以框图形式示出以便于描述本发明。

如本申请中所使用，术语“组件”和“系统”意指计算机有关的实体，无论是硬件、硬件和软件的结合、软件、或执行中的软件。例如组件可以是，但不限于，处理器上运行的进程、处理器、对象、可执行代码、执行的线程、程序、和/或计算机。作为示例，服务器上运行的应用程序和该服务器都可以是组件。一个或多个组件可驻留在进程和/或执行线程的内部，且一个组件可局限在一个计算机上和/或分布在两个或多个计算机之间。

映射关系的合成

本发明是一种适用于对一类较宽泛的映射关系进行合成的普遍算法，其中两个映射关系之一或两者都不是函数，而是诸如两种模式之间的约束(诸如map₁₂、map₂₃、map₃₄等)和函数之逆(诸如map₁₂的逆等)等。

图1示出根据本发明通过合成数据库模式(未示出)之间两个现有映射关系(104和106)来构造结果映射关系102的示意图100。提供第一模式映射关系104(记为模式映射关系₁₂)，它可以是函数或非函数。类似地，提供第二模式映射关系106(记为模式映射关系₂₃)，它可以是函数或非函数。对于每个映射关系都是函数的情形而言，用于映射关系合成的各种算法是公知的。因此，本发明仅解决两个映射关系模式(104和106)之一或两者是非函数的实例。

如虚线所示，解决以下情形：当第一模式映射关系104是函数，第二模式映射关系106是非函数的时候；当第一模式映射关系104是非函数，第二模式映射关系106是函数的时候；以及，当第一模式映射关系104是非函数，第二模式映射关系106是非函数的时候。使用合成算法组件108来合成模式映射关系(104和106)，以生成结果映射关系102(记为模式映射关系₁₃)。合成组件108使用一种推论程序来获得所有需要在合成映射关系中出现的约束的有穷公理。这在下文详细描述。

在这三种非函数映射关系的任何一种中，映射关系可由逻辑约束或子句来表示。图2示出根据本发明的逻辑约束映射关系合成的示意图。图中提供三种数据库模式202(记为S₁、S₂和S₃)，从这三种模式可推导出第一和第二模式映射关系(204和206)(分别记为映射关系₁₂和映射关系₂₃)。

合成组件208(类似于组件108)便于将两个模式映射关系(204和206)合成为结果模式映射关系210(记为映射关系₁₃)。所考虑的约束语言包括完全依存关系(CQ₀^＝映射关系)、嵌入依存关系(CQ^＝映射关系)、或二阶依存关系(SOCQ^＝映射关系，也称为二阶元组生成依存关系)。因此，第一和第二映射关系(204和206)中的每一个都可包括完全、嵌入和/或二阶依存关系的约束。给定两个不一定是函数的有穷CQ₀^＝、CQ^＝或SOCQ^＝映射关系map₁₂和map₂₃，难题是找到指定map₁₂和map₂₃合成的结果映射关系210的CQ₀^＝、CQ^＝或SOCQ^＝映射关系。

现在参考图3，图中示出根据本发明的一种合成依存关系的方法。尽管出于解释简单的目的，本文中例如以流程图的形式示出的一种或多种方法是作为一系列动作来示出和描述的，但是要理解并意识到，本发明不受动作顺序的限制，因为根据本发明，一些动作可按不同次序发生和/或与本文中所示出和描述的其它动作同时发生。例如，本领域技术人员将理解并意识到，一个方法可被替换地表示为诸如状态图中的一系列相互关联的状态或事件。此外，不是所有示出的动作都是实现根据本发明的方法所必须的。

合成以三个步骤来计算：将CQ₀^＝映射关系斯柯伦化以取得二阶依存关系(SOCQ^＝)映射关系。斯柯伦化是从公式中移除存在量词的一种方法。接下来，找到输入和输出签名上的所有约束的有穷公理，该有穷公理可从给出映射关系的约束推导出来。最后，将有穷公理解除斯柯伦化以取得CQ^＝映射关系。据此，提供一种方法，以使在300，嵌入的依存关系被斯柯伦化以获得二阶依存关系。在302，输入和输出签名上的所有约束的有穷公理被找到。该公理可从给出映射关系的约束推导出来。在304，有穷公理被解除斯柯伦化以获得嵌入依存关系。

在CQ₀^＝映射关系和SOCQ^＝映射关系的实例中，仅图3的动作302适用。据此，图4示出根据本发明的一种合成方法，该方法强加条件并使用检查来确定合成是否终止于正确的答案。在400，运行“合成”算法。以下算法“合成”假定，输入映射关系map₁₂由模式S₁和S₂之间的有穷组CQ₀^＝依存关系∑₁₂指定，输入映射关系map₂₃由模式S₂和S₃之间的∑₂₃指定，而输出映射关系map₁₃由模式S₁和S₃之间的∑₁₃给出。(用于CQ₀^＝和SOCQ^＝映射关系的这一基本算法的概括在下文给出)。算法合成(∑₁₂，∑₂₃)：

设∑：＝∑₁₂∪∑₂₃

重复

    设∑′：＝

    对于∑中的每一对子句，ψ

        如果存在，ψ的σ₂-消解式x_i

            并且∑中没有x_i的变体

        则设∑′：＝∑′∪{x_i}

        设∑：＝∑∪∑′

直至∑′＝

返回∑₁₃：＝∑中仅引用S₁，S₃的符号的约束

当“合成”终止时，证明该算法给出正确答案。但是，“合成”可能不终止。在402，强加条件来检查该算法的终止。以下条件可被包括，来测试算法“合成”终止的充分性。如在404所示，通过运行合成(∑₁₂，∑₂₃)的k-1次迭代，然后检查∑中是否出现(z)，R(y)→R(x)形式的约束，可在多项式时间检查这些条件，其中k是S₂中关系符号的个数：

(1)(z)是S₁∪S₃上原子的“逻辑乘”；

(2){x}不是{y}的子集；并且

(3)R是S₂中的关系符号。

在406，一旦满足了这些条件，合成算法即带着正确答案终止。

为了获得嵌入依存关系，如图3的动作304(步骤3)所示，提供一种给出正确结果的算法。据此，图5示出根据本发明的一种方法，该方法对有穷公理进行解除斯柯伦化以获得嵌入依存关系。在500，使用“等同”对斯柯伦函数进行解嵌套来得出结论。在502，进行检查以确保结论中的所有变量都在每个斯柯伦函数的变量依存关系集合中出现。在504，如果结论中的所有变量都在变量依存关系中出现，则流程流向506，生成可通过统一结论中出现的斯柯伦函数获得的所有可能的子句。在508，通过用新的存在变量代换每个斯柯伦项将每个子句单独去斯柯伦化。但是，在504，如果不是所有的变量都出现，则流程流向510，斯柯伦化失败，进程结束。

图6示出根据本发明的三个以上数据源模式602上的多重合成的示意图600。每对数据源模式602(记为S₁、S₂、S₃、……、S_N)都与一个一阶模式映射关系604(记为M₁₂、M₂₃、……M_(N-1)(N))相关联。每对一阶模式映射关系604进而由合成组件(记为C_N)合成。即，使用第一合成组件606(记为C₁)合成第一对一阶模式映射关系(M₁₂和M₂₃)以生成结果二阶模式映射关系M₁₃。然后使用一不同的合成组件C₂(或相同合成组件C₁)将结果二阶模式映射关系M₁₃与下一个一阶模式映射关系M₃₄合成。该过程继续直至没有其它一阶模式映射关系604可用来合成，并在输出处生成结果模式映射关系M_1N。

替换地，或者作为对图6的算法的补充，图7示出便于通过使用算法的单次调用来执行的多重映射关系的合成以获得输出映射关系M_1N的系统700。此处，合成组件704接收多个一阶模式映射关系702(记为M₁₂、M₂₃、……M_(N-1)(N))的输入，处理这些映射关系702，并在输出处一次性生成结果模式映射关系M_1N。

以此方式，下文所考虑的所有算法及其变体可适用于多重映射关系。具体而言，图6中给出的算法可被扩展成图7的算法，并且如下所示，甚至在图6的逐步程序失败时，仍能产生正确的合成并终止。

算法合成(∑₁₂，∑₂₃，...，∑_(n-1)n)：

设∑：＝∑₁₂∪∑₂₃∪...∪∑_(n-1)n

重复

设∑′：＝

对于∑中的每一对子句，ψ

    如果存在，ψ的σ₂-消解式x_i其中2≤k＜n

        并且∑中没有x_i的变体

    则设∑′：＝∑′∪{x_i}

    设∑：＝∑∪∑′

直至∑′＝

返回∑₁₃：＝∑中仅引用S₁，S_n的符号的约束

合成和非函数映射关系的分析

术语“映射关系”已在数据库文献中确立，它指诸如数据库状态或XML文档等实例上的二元关系。一种称为模型管理、用于管理映射关系的一般框架研究映射关系上，以及称为摸型的实例集合上的一般算子。在这些算子之间，有诸如域、范围、合成、求逆等基本算子。

如果映射关系是函数，则称其为函数性的。非函数性的映射关系在许多上下文中出现，特别是在数据集成和数据交换中。有许多非函数性映射关系的自然源。例如，非单射的函数性映射关系的逆是非函数性的映射关系。

对约束所给出的映射关系和模型，特别是嵌入依存关系所给出的、以及完全依存关系所给出的映射关系的开发在本领域中引起了极大关注。这些映射关系分别被称为CQ^＝-映射关系和CQ₀^＝-映射关系，因为它们是由具有等同的逻辑乘查询(CQ^＝)的蕴含和具有等同、但没有存在量化的逻辑乘查询(CQ₀^＝)的蕴含给出的。类似地，由嵌入依存关系和完全依存关系给出的模型分别称为CQ^＝-模型和CQ₀^＝-模型的。

对于关系型设置中的基本算子，考察若干基本问题。令Λ为模型和映射关系所用的语言。给定算子O以及Λ-模型和Λ-映射关系作为输入：(1)输出总是Λ-模型或Δ-映射吗？(即，Λ在O下是闭合的)；(2)如果不是，则有决策程序来确定何时输出是Δ-模型或Λ-映射？；以及(3)在输出是Δ-模型或Δ-映射的情形中，找到输出的表达式的困难程度如何？

此描述至少解决Δ是CQ₀^＝、CQ^＝或SOCQ^＝时的情形。对于许多算子(例如，恒等、交、和笛卡尔积)而言，可以看到(1)的答案为‘是’，并且(3)的答案为‘非常简单’(见下文命题3)。对于一些其它算子(例如，范围、域、和合成)而言，可示出(1)和(2)的答案为‘否’。此外，引入CQ₀^＝、CQ^＝和SOCQ^＝的大子类，对其而言，(1)的答案为‘是’，(3)的答案为‘简单’。

可以看出，域、范围和合成是密切相关的，并且可相互归约(见以下命题4)。因此，研究合成和求逆就足够了。如果对定义映射关系的语言设置对称约束则后者是很简单的。另一方面，合成证明是很困难的。

本领域中已经研究了映射关系的合成。在一项研究中，引入一类源到目标二阶元组生成依存关系(ST SO tgds)，并显示ST SO tgds所给出的映射关系类在合成下是闭合的。此外，找到若干示例，示出若干较小的映射关系类在合成下不是闭合的实例。特别地，可显示甚至在进一步限制于源到目标依存关系时，CQ^＝映射关系在合成下也不是闭合的。

本发明在若干方向扩展了现有技术的成果。本文中，SO tgds给出的映射关系称为SOCQ^＝-映射关系。注意，斯柯伦化的CQ^＝-映射关系给出SOCQ^＝-映射关系。因此，解决了三大类映射关系的合成，其中每一类都恰当地包含先前的类：

1.CQ₀^＝-映射关系(完全依存关系)

2.CQ^＝-映射关系(嵌入依存关系)

3.SOCQ^＝-映射关系(SO tgds)

所关注的一种情形是嵌入依存关系(CQ^＝-映射关系)的情况。计算此类模式映射关系的合成的一种方法，如上文在图3中所引用，是(1)将CQ^＝-映射关系斯柯伦化以取得SOCQ^＝-映射关系，(2)找到输入和输出签名上的所有约束的有穷公理，该公理可从给出这些映射关系的约束推导出来，以及最后(3)将有穷公理解除斯柯伦化以取得CQ^＝-映射关系。困难来自步骤2和3。

本发明扩展为在求逆下获得闭合所考虑的语言约束，在源到目标的约束的情形中，求逆下不能获得闭合，因为源到目标的约束的逆是目标到源的约束。

提供CQ₀^＝、CQ^＝和SOCQ^＝的子类，它们在合成和求逆下是闭合的，并且理想情况下包括从CQ₀^＝和CQ^＝查询引起的约束，已知它们在合成下是闭合的。

希望具有可广泛适用的、多项式时间可检查的、充分的条件，以使两个CQ₀^＝-映射关系(CQ^＝、SOCQ^＝)的合成成为CQ₀^＝-映射关系(CQ^＝、SOCQ^＝)。此外，较佳的是知道是否有可计算的必要性和充分的条件，或问题是否是不可判定的。

概括本文中所提供的一些方面，示出CQ₀^＝-映射关系在合成下不是闭合的。确定两个CQ₀^＝-映射关系的合成是否是CQ₀^＝-映射关系的问题示出是不可判定的。这些结果转入CQ^＝-映射关系和SOCQ^＝-映射关系的情况。此外，提供合成的若干等效(无效)条件。

引入合成的多项式-时间-可检查充分条件，它包括约束由查询给出的情形。此外，标识出CQ₀^＝、CQ^＝和SOCQ^＝的子类，它们在合成和求逆下是闭合的，且它们包括约束由查询给出的情形。最后，给出一种多项式-时间算法，用于计算满足以上条件的CQ₀^＝、CQ^＝和SOCQ^＝映射关系的合成。

预备信息

签名σ＝{R₁，R₂，...，R_N}是一组关系符号。关系型原子是R(t₁，...，t_m)类型的公式，其中t_i是变量或常量。等同原子是t₁＝t₂类型的公式，其中t_i是诸如变量或常量等项。CQ定义为逻辑乘查询集合，即类型的公式，

其中是逻辑乘关系型或等同原子的逻辑乘，且自由变量y₁，...，y_n中的每一个都发生在某个关系型原子中。CQ₀是具有逻辑乘、但没有存在量词的查询集合(即，当m＝0时，也称为选择-连结查询)。给定查询类Λ，Λ^＝是还包括等同的对应查询类。

Skolem(Q)定义为通过用斯柯伦函数代换存在量词从Q获得的公式；它是声明斯柯伦函数的存在、并且不具有一阶存在量词的存在二阶公式。例如，如果

$>>Q>=>\exists >y>>(>Exy>,>Eyz>)>>\to >Exz>>>$

则

$>>Skolem>>(>Q>)>>=>\exists >f>>(>E>>(>x>,>f>>(>xz>)>>)>>,>E>>(>f>>(>xz>)>>,>z>)>>\to >Exz>)>>.>>>$

设SkΛ：＝{Skolem(Q)：Q∈Λ}。给定签名σ₁∪σ₂上的约束的集合ψ，ψ|_σ1是ψ中仅包含σ₁中的关系符号的约束的集合。在前提或结论中包含来自σ₁的关系符号的约束称为σ₁-约束。

模型和映射关系。模型是实例集合。模型可用诸如SQL、DDL、XML模式等具体语言表达。例如，关系型模式表示数据库状态的集合；XML模式表示XML文档的集合；工作流定义表示工作流实例的集合；编程接口表示与接口一致的实现的集合。映射关系是实例上的关系。除非另有声明，否则假定所有映射关系都是二元的，即，它们在两个模型之间有效。映射关系可用诸如SQL、DML、XSLT等具体语言表达。

用于指定映射关系的约束。约束是布尔查询。约束的集合用大写希腊字母表示，单个约束用小写希腊字母表示。要考虑的约束在下式中：

IC(Λ)：＝{x(Q₁(x)→Q₂(y))：Q₁，Q₂∈Λ}其中{x)是Q₁中的自由变量集合，{y){x}，且这些称为Λ上的查询蕴含约束。这些类型的约束表达Q₁被包含在Q₂中，并且在Λ是CQ^＝的情形中被称为嵌入依存关系，在Λ是CQ₀^＝的情形中被称为完全依存关系。还考虑下式中的约束：

$>>IC>>(>SOC>>Q>=>>)>>:>=>\exists ver>>f>->>\{>\forall ver>>x>->>>(>>Q>1>>>(ver>>x>->>)>>\to >>Q>2>>>(ver>>y>->>)>>)>>\}>>>$

其中{x}是Q₁中的自由变量集合，{y}{x})，且Q₁、Q₂是类似CQ₀^＝查询，不同之处是它们还可有从函数符号f构造的项。类似地定义了IC(SOCQ)，其中Q₁、Q₂是类似CQ₀查询。

给定查询语言Λ，映射关系

与每个以下形式的表达式相关联：

(σ₁，σ₂，∑₁₂)

其中∑₁₂是签名σ₁∪σ₂上的IC(Λ)的有穷子集。σ₁是输入(或源)签名，σ₂是输出(或目标)签名。不失一般性，假定σ₁，σ₂是不相交的或完全相同的。

如果对应于E的映射关系是m，则可以说m是由表达式E绐绐定的。此外，如果m是由表达式(σ₁，σ₂，∑₁₂)给定的，且∑₁₂是IC(Λ)的有穷子集，则m是Λ-映射关系。

合成。给定两个映射关系m₁₂和m₂₃，合成m₁₂·m₂₃是唯一映射关系：

推论和跟踪

以下提供附加预备信息以解释以下各部分中的算法和正确性证明。以下确定一种具体的推论系统，定义、DC(·)和chase(·)的标准记号，并给出命题1和2。

IC(SOCQ^＝)中的约束被写为以下形式的规则：

Q₁(x)→Q₂(x)

使斯柯伦函数上的二阶量词和最外面的一阶通用量词x被隐式包含。称Q₁(x)为前提Q₂(x)为结论。如果前提为空，则仅写结论。称Q₂(c)形式的规则为论据，其中c是约束元组。

定义1.从∑出发的推论是一规则序列，其中每个规则都是用以下三种方法中的一种获得：

1.通过从∑复制，

2.通过扩展和/或重命名先前在序列中出现的规则，或者

3.通过对先前在序列中出现的两个规则上应用消解。

这些规则分别被称为公理规则，扩展/重命名规则和消解规则。

推导程序是使用推论来推导新规则的程序。如果推论由n行组成，则该推论有长度n。从规则r′扩展/重命名所获得的规则r在前提中可能具有额外的原子，其变量可能被任意项一致代换，并且在结论中可能有与前提中的等式一致的代换。例如，

R(xy)，y＝f(xy)→S(xy)

是对R(uv)→S(uf(uv))应用扩展/重命名的有效结果。

当存在使两个公式句法上完全相同的变量代换时，这两个公式可被统一。消解是一种完全逻辑推论程序，当一个规则的前提的一个原子可与另一个规则的结论中的一个原子统一时，该程序从两个给定规则推导出新规则。例如，

R(xy)，S(yz)→S(xz)

是对以下规则应用消解的结果：

R(xy)→S(xy)

S(xy)，S(yz)→S(xz)

此例说明一种称为肯定前件式假言推理(modus pones)的消解的特殊情形。通过将肯定前件式假言推理应用于规则r′获得规则r，r″包含r″中的结论和r′中的前提原子，以及r″中那些未出现在r′的结论中的前提原子。

通过按升序对规则进行编号，并通过向每一行添加表示如何获得该行的理由来对推论进行注释。仅用两个编号便足以证明消解规则正确，用单个编号和一个变量赋值便足以证明扩展/重命名规则正确。公理规则可通过缺少任何其它注释来表示。变量赋值是一个x：＝y形式的项的列表，其中x是一个变量，而y是一个项。

示例1.给定

Δ＝{R(1，1)}且

∑＝{R(xy)→S(xy)，S(zz)→T(zz)}，

以下是从∑∪Δ的有效推论：

1.R(1，1)

2.R(xy)→S(xy)

3.R(1，1)→S(1，1)[2]x：＝1，y：＝1

4.S(1，1)         [1，3]

5.S(zz)→T(zz)

6.S(1，1)→T(1，1)[5]z：＝1

7.T(1，1)         [4，6]

此处，规则1、2和5是公理，3和6是扩展/重命名，而4和7是消解。

在推论之内，如果消解是通过统一来自签名σ₂的原子来执行的，则该消解步骤称为σ₂-消解。通过σ₂-消解获得的规则ξ′称为σ₂-消解式。如果不使用消解即可从ξ′推导出规则ξ，则ξ是ξ′的变体。

以下是对证明合成算法和不可判定性结果的正确性的先决条件的介绍。

如果有来自一约束集合∑的推论，其中最后一行包含约束ξ，则可以说ξ是从∑推导出来的，写成∑ξ。∑的Λ-推论闭合是

DC(Λ，∑)：＝{ξ∈Λ：∑ξ}。

当Δ从上下文中消去时写成DC(∑)。如果∑中的所有约束在D中均为真，则写成如果对于所有实例，隐含则写成可以检查得出，如果则还有即，该推论系统是健全的。如果一推论系统确保如果一个句子的集合是不可满足的，那么它将导出矛盾的话，则该推论系统被称为完整的。推论证明，所推导出的规则是由公理规则隐含的。

命题1.如果Δ是一个论据集合，那么以下是等价的：

    1.∑∪Δφ。

    2.存在ξ使∑ξ且Δ，ξφ。

证明.如果(2)成立，则存在推论和证明γ′和γ″证明∑ξ且Δ，ξφ。那么通过将γ″拼接到γ′，获得证明∑∪Δφ的γ。现在假定(1)成立，且γ证明∑∪Δφ。除了以下替换以外，设γ′为γ，以下替换由从γ中的第一个规则到最后一个规则做成的规则：

1.如果规则r是来自Δ的公理规则，则将其移除。

2.如果规则r不是来自Δ的公理规则，则按原样将其保留。

3.如果规则r是通过从规则i扩展/重命名而获得，则用对应的变量v_c替换r中和r的变量赋值中的每个常量c。

4.如果规则r是通过从规则i和j消解而获得，且规则i是来自Δ的公理规则，则用来自规则j的一般扩展/重命名取代r。

5.如果规则r是通过从规则i和j消解而获得，且规则i不是来自r的公理规则，则用将消解应用于新规则i和j所得的结果替换r。

示例2.给定从示例1的推论γ。γ′为：

1.<空行>

2.R(xy)→S(xy)

3.R(v₁v₁)→S(v₁v₁)   [2]x：＝v₁ y：＝v₁

4.R(v₁v₁)→S(v₁v₁)[3]

5.S(zz)→T(zz)

6.S(v₁v₁)→T(v₁v₁)[5]z：＝v₁

7.R(v₁v₁)→T(v₁v₁)[4，6]

为每个规则进行以下替换：

1.来自Δ的公理：根据1移除。

2.来自∑的公理：根据2不改变。

3.扩展重命名：根据3用v₁替换1。

4.对1、3的消解：根据4一般的扩展/重命名。

5.来自∑的公理：根据2不改变。

6.扩展重命名：根据3用v₁替换1。

7.对4、6的消解：根据5消解。

因为来自Δ的公理不再被使用，并且以上的替换1到5确保从先前替换的规则正确推导出规则R，所以γ′是证明∑ξ的有效推论。此外，Δ、ξR(c)由推论γ″证明，推论γ″由以下序列组成，

-来自Δ、被从γ移除以获得γ′的那些公理，

-ξ紧接着ξ′，其中ξ′是通过将每个变量v_c重命名为对应常量c而从ξ获得的。

-使用每个来自Δ的公理，并以ξ′开始的一系列消解步骤。

定义2.给定实例D，用约束∑IC(SOCQ^＝)和斯柯伦函数F的组来跟踪D的结果简写为chase(D，Σ，F)，并由从下式获得的数据库D″来表示：

D′：＝{R_i(c)：∑∪Δ∪ΦR_i(c)}

其中

c是常量元组，

Δ是D所给定的论据集合：

且Φ是F所给定的论据集合：

Φ：＝{f(c)＝a：f∈F，f(c)＝a}如下。当且仅当∑∪Δ∪Φc₀＝c₁，定义c₀≡c₁。

现在要从D′获得D″，从每个等价类中选择一个常量c₀，并用c₀替换该等价类中的每一个常量。即，D″：＝D′/≡。要求F中的所有函数都具有相同的域。如果它们是有穷的，则chase(D，∑，F)是有穷的。此定义是常规定义的变体，在其中，函数F是在跟踪过程中构造的。

命题2.

证明.设且假定对于某个ξ∈∑，这意味着在前提中必定有对变量x的某个常量c的赋值使得ξ中的前提成立，而结论不成立。假定结论由单个关系型原子R(y)或单个等式y₁＝y₂组成，其中y是一系列x上的项。通过用对应常量c替换x中的每个变量，将y′设成从y获得的一系列项。如果前者成立，则Δ∪Φ，ξR(y′)成立，且R(y′)不在D′中。因为ξ∈∑，所以命题1隐含∑∪Δ∪ΦR(y′)成立，这与D′中的定义矛盾。如果后者成立，则Δ∪Φ，ξy′₁＝y′₂和y′₁＝y′₂成立。因为ξ∈∑，所以命题1隐含∑∪Δ∪Φy′₁＝y′₂成立，这与≡和D″的定义矛盾。

CQ0＝映射关系合成

通过研究CQ₀-映射关系和CQ₀^＝-映射关系的合成，开始以下对合成的描述。稍后，所介绍的处理这些实例的技术将扩展至处理SOCQ^＝和CQ^＝-映射关系。给出将两个CQ₀^＝-映射关系合成为一个CQ₀^＝-映射关系的充要的、不可计算的条件(见以下定理1)。然后，示出CQ₀和CQ₀^＝在合成下不是闭合的(见以下示例3)，此外，确定两个CQ₀^＝-映射关系的合成是否是CQ₀^＝-映射关系是不可确定的(见以下定理2)。给出一种用于合成的(CQ₀^＝合成)算法，它在满足下面定理3的条件的CQ₀^＝映射关系上正确工作，它可在多项式时间被检查。同样，定义在多项式时间可识别的CQ₀^＝子集，称为好CQ₀^＝，该子集在合成下闭合(见以下定理4)。

(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的两个CQ₀^＝-映射关系的合成可使用以下算法来计算：

算法CQ₀^＝合成(∑₁₂，∑₂₃)：

设∑：＝∑₁₂∪∑₂₃

重复

          设∑：＝

          对于每一对φ，ψ∈∑

                 如果存在φ，ψ的σ₂-消解ξ

                     且∑中没有ξ的变体

                     则设∑′：＝∑∪{ξ}

          设∑：＝∑∪∑′

 直至∑′＝

返回∑₁₃：＝∑|σ₁₃

下一个步骤是验证该算法的正确性，以及研究该算法终止的条件。注意CQ₀和CQ₀^＝在合成下不是闭合的，如下例所示。

示例3.考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的CQ₀-映射关系m₁₂和m₂₃，其中∑₁₂是：

R(xy)→S(xy)

S(xy)，S(yz)→S(xz)

且∑₂₃是：

S(xy)→T(xy)

并且其中σ₁，＝{R}，σ₂，＝{S}，且σ₃，＝{T}。总之，这些约束说明RST以及S在传递闭包下是闭合的。这隐含tc(R)T，其中tc(R)表示R的传递闭包。可以看到，只有在R和T之间成立的CQ₀^＝-映射关系才是以下形式的约束：

R(X，v₁)，R(v₁，v₂)，...，R(v_i-1，v_i)，R(v_i，y)→T(xy)但其任何有穷集合都不表达tc(R)T。

实际上，合成m₁₂·m₂₃甚至在FO(一阶逻辑)中都是不可表达的。否则，给定FO语句φ以使：

当且仅当时，<R，T>∈m₁₂·m₂₃可创建FO公式ψ(xy)，它是通过用x≠u ∨y≠v替换φ中的每一个出现的T(uv)来获取的。然后给定带有RD²的域D：

当且仅当

当且仅当tc(R)D²-<a，b>

当且仅当<a，b>∈tc(R)有因此，(x，y)﹁ψ（x，y)说明R是连通图，它不能在FO中被表达。

两个CQ₀^＝-映射关系的合成何时是CQ₀^＝-映射关系？本文中的定理1给出充要条件。合成要成为CQ₀^＝-映射关系的一个障碍可能是递归，但是递归不总是问题。在定理3中，提供可被有效检查的充分条件，在定理4中，示出好CQ₀^＝，即以下定义的CQ₀^＝的子集，在合成下是闭合的。所有这些结果对CQ₀也成立。

定理1.如果CQ₀^＝-映射关系m₁、m₂是由(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给出的，且有∑₁₂₃：＝∑₁₂∪∑₂₃和σ₁₃＝σ₁∪σ₃，则以下是等价的：

(1)存在签名σ₁₃上的有穷约束集合 $>>>\Sigma >13>>\subseteq >IC>>(>Csup>>Q>0>=sup>>)>>,>>>使m：＝m$₁·m₂由(σ₁，σ₃，∑₁₃)给定。

(2)存在签名σ₁₃上的有穷约束集合 $>>>\Sigma >13>>\subseteq >IC>>(>Csup>>Q>0>=sup>>)>>,>>>使$

$>>DC>>(>Csup>>Q>0>=sup>>,>>\Sigma >123>>)>>>|>>\sigma >13>>>=>DC>>(sup>>CQ>0>=sup>>,>>\Sigma >13>>)>>.>>>$

(3)存在m，使对于签名σ₁₃上满足∑₁₂₃ξ的每个ξ，都有最多使用m个σ₂-消解的来自∑₁₂₃的ξ的推论。

证明.证明使用以下引理1和2。证明首先示出(1)和(2)的等价，然后示出(2)和(3)的等价。

假定(2)成立。则

当且仅当(根据·的定义)

当且仅当(根据引理1)

当且仅当(因为(1)成立)

当且仅当(根据DC的健全性)

<A，C>∈m₁·m₂。这显示(1)成立。

反过来，假定(1)成立。则

当且仅当(根据引理1)

当且仅当<A，B>∈m₁·m₂                   (根据·的定义)

当且仅当(因为(2)成立)

当且仅当(根据DC的健全性)

这显示(2)成立。

现在假定(3)成立。设∑为DC(CQ₀^＝，∑₁₂₃₎|_σ13中所有约束的集合，这可最多使用m个σ₂-消解而无需其它任何消解来导出。∑中的每个约束可通过从有穷子集∑₁₃∑扩展/重命名来获得。可以显示(2)成立。

假定有推论γ证明∑₁₂₃ξ。因为(3)成立，所以可以假定γ有m′个σ₂-消解。根据引理2，存在也带有m′个σ₂-消解的证明z₁₂₃ξ的推论γ，且它们全部都在任何其它消解之前出现。因为γ的最后一行不包含任何来自σ₂的符号，所以可以假定在最后一个σ₂-消解以后，γ不包含任何包含来自σ₂的符号的行。

将γ′分成两部分：γ′₁是到并包括最后一个σ₂-消解的γ的起始部分；而γ′₂是γ′的其余部分。根据∑的定义，γ₁中的每个约束ψ都必须在∑中，因此∑₁₃ψ成立。γ′₂中的每个约束ψ都不包含任何来自σ₂的符号和 $>>>\Sigma >123>>>|>>\sigma >13>>>\subseteq >>\Sigma >13>>,>>>这隐含\sum$₁₃ψ。因此，如所期望有E₁₃ξ。

反过来，假定(2)成立。取m为从∑₁₂₃推导每个ψ∈∑₁₃所需σ₂-消解的总数。假定∑₁₂₃ξ。则存在推论γ证明∑₁₃ξ。很明显，γ没有σ₂-消解。从γ，通过将∑₁₃中的每个约束的推论拼接到γ，并用一来自∑₁₃的公理的推论结束处的行的空扩展/重命名来替换使用该公理处的每一行，可获得证明∑₁₂₃ξ的γ′。这示出(3)成立。

引理1.在定理1的假设之下，以下是等效的：

1.

2.

证明.假定对于某个B有则(根据健全性)，因此因为在DC(CQ₀＝，∑₁₂₃)|_σ13中B未被提及。

反过来，假定设(A′，B′，C′)：＝chase((A，，C)，∑₁₂₃)。如果跟踪终止，且有A＝A′和C＝C′，则根据命题2有这蕴含和如所期望。

很明显跟踪终止，因为没有新的常量被引入。为得到矛盾，现在假定A≠A′且C≠C′。设Δ_AC为A和C所给定的论据集合。则，

∑₁₂₃∪Δ_ACR(c)其中R是不包含c的A或C的关系，或者

∑₁₂₃∪Δ_ACc₀＝c₁其中c₀、c₁是A或C中不同的常量。

考虑前一种情况，后一种情况是类似的。如果∑₁₂₃∪Δ_ACR(c)则根据命题1存在ξ使∑₁₂₃ξ且Δ_AC，ξR(c)。因为所以得出且 $>>\xi >\in >DC>>(>Csup>>Q>0>=sup>>,>>\Sigma >123>>)>>>|>>\sigma >13>>>,>>>这与初始假定矛盾。$

引理2.在定理1的假设之下，如果有推论γ最多用m个σ₂-消解证明∑₁₂₃ξ，则存在γ′最多用m个σ₂-消解证明∑₁₂₃ξ，并且所有σ₂-消解都在所有其它消解之前出现。

证明.假定k＜m且γ_k，l用以下各项证明∑₁₂₃ξ：

1.恰好m个σ₂-消解，

2.其中前k个消解是σ₂-消解，且

3.其中在第k+1个σ₂-消解之前或该推论结束处恰好有l个非σ₂-消解。

该证明接下来对k和l和进行归纳。给定γ_k.l且有l＞0，该证明示出如何获得γ_k，l-1。为了证明l＝0的情形，简单地设γ_k+1，l′：＝γ_k，0，其中l′满足以上条件。一旦为某个l′获得γ_m，l′，即设γ′：＝γ_m，l′，该引理得证。

考虑第s行包含δ，例如第i和j行的γ_k，l中的第(k+1)个σ₂-消解分别包含α和β。还考虑第r行包含λ，例如第r₁和r₂行的γ_k，l中的第l个σ₂-消解分别包含λ₁和λ₂。

现在考虑若干情形。如果i，j＜r＜s，则通过将第s行恰好移到r之前来获得γ_k，l-1。如果第i、j行不是从第r行导出，则通过首先重新排列γ_k，l到γ′_k，l以使i，j＜r＜s，然后如上进行来获得γ_k，l-1。

否则，或者α或者β是通过从第r行的扩展/重命名获得的。为简化表示，假定两者都是通过从第r行的单次扩展/重命名获得的(另一种情形是类似的)。现在存在r＜i，j＜s。通过在需要的情况下重新排列γ_k，l，假定i＝r+1，j＝r+2且s＝r+3。因为α和β可通过扩展/重命名从r获得，α₁、α₂和β₁、β₂通过扩展和重命名分别从r₁、r₂获得，使得α为α₁、α₂的消解，而β为β₁、β₂的消解。用以下7行替换4个相连行r、i、j、s。

r      α₁[r₁]

r+1    α₂[r₂]

r+2    β₁[r₁]

r+3    β₂[r₂]

r+4    δ₁[r+1，r+2]

r+5    δ₂[r+4]

r+6    δ[r+5，r+3]

很重要的一点是，因为α和β必需通过σ₂酌关系符号消解所以α₂和β₁也必须如此，因此第r+4行如今包含一个σ₂-消解。注意δ在第r+6行上，因为α₁、α₂、β₁和β₂上消解的结果与α和β上消解的结果是相同的(这是因为消解是“相关的”)。

推定1.在定理1的假设之下，无论CQ₀^＝合成(∑₁₂，∑₂₃)何时终止，它都产生∑₁₃以使m₁₂·m₂₃由(σ₁，σ₃，∑₁₃)给定。

注意在主循环的第m次迭代以后，∑将包含能最多使用m个σ₂-消解步骤来推导的每个约束的变体。示例3的约束未能满足定理1的(3)，因此，当如示例3中的∑₁₂和∑₂₃作为输入时，CQ₀^＝合成(∑₁₂，∑₂₃)将不会终止。相反，从以下的确满足定理1的(3)的示例，CQ₀^＝合成(Σ₁₂，∑₂₃)将会在∑₁₂、∑₂₃上终止，因此递归不总是坏的。

示例4.考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的CQ₀-映射关系m₁₂和m₂₃，其中∑₁₂是：

R(xy)→S(xy)

S(xy)，S(yz)→R(xz)，而∑₂₃是：

S(xy)→T(xy)，并且其中σ₁＝{R}，σ₂＝{S}，且σ₃＝{T)。总之，这些约束说明RST，R和S在传递闭包下是闭合的(因为以下约束：

S(xy)，S(yz)→S(xz)

R(xy)，R(yz)→R(xz)可从以上约束中导出)，且只要S(xy)、S(yz)成立，R(xz)就成立。以下约束：

R(xy)，R(yz)→R(xz)

R(xy)→T(xy)准确地表达合成m₁·m₂，且恰好是CQ₀^＝合成(∑₁₂，∑₂₃)所找到的。

定理2.检查两个CQ₀-映射关系的合成是否是CQ₀-映射关系是不可确定的(实际上是coRE-hard)。用CQ₀^＝替换CQ₀后仍成立。

证明.该证明将Post的对应问题(PCP)——已知为不可确定的——归纳为确定m₁₂·m₂₃是否是CQ₀-映射关系的问题，其中m₁₂和m₂₃是CQ₀-映射关系。给定一PCP问题，定义m₂₃以使当且仅当m₁₂·m₂₃不是CQ₀-映射关系时，该PCP问题有解(m₁₂不依赖于PCP问题)。

该CQ₀-映射关系m₁₂·m₂₃由(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给定，其中

·σ₁＝{A，B，O，Z}，

$>>·>>\sigma >2>>=>\{ver>>A>^>>,ver>>B>^>>,ver>>O>^>>,ver>>Z>^>>\}>,>>>且$

·σ₃＝{T}

其中A、B是一元的，所有其它关系都是二元的，且∑₁₂和∑₂₃如下所述。为σ₁上的以下原子集写成x0011y：

A(x)，Z(xa)，Z(ab)，O(bc)，O(cy)，B(y)，它对应于从A经Z、O到B的路径(Z表示“0”，O表示“1”)。类似地，σ₂上的原子集

$>ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>Z>^>>>(>xa>)>>,ver>>Z>^>>>(>ab>)>>,ver>>O>^>>>(>bc>)>>,ver>>O>^>>>(>cy>)>>,ver>>Z>^>>>(>>x>\prime >>>a>\prime >>)>>,ver>>Z>^>>>(>>a>\prime >>>b>\prime >>)>>,ver>>O>^>>>(>>b>\prime >>>c>\prime >>)>>,ver>>O>^>>>(>>c>\prime >>>y>\prime >>)>>,ver>>B>^>>>(>y>>y>\prime >>)>>>>写成\sum$₁₂包含以下约束：

A(x)，Z(xy)，A(x′)， $>>Z>>(>>x>\prime >>>y>\prime >>)>>\to ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>Z>^>>>(>xy>)>>,ver>>Z>^>>>(>>x>\prime >>>y>\prime >>)>>>>以及对于所有组合AO、ZZ、ZO、OZ、OO、ZB、OB的所有对应约束。这些约束隐含可为任意串S导出$

根据∑₂₃中约束对每个PCP“多米诺(domino)”进行编码如下。例如，将多米诺0011/011编码为以下约束：

$>ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>Z>^>>>(>xa>)>>,ver>>Z>^>>>(>ab>)>>,ver>>O>^>>>(>bc>)>>,ver>>O>^>>>(>cy>)>>,ver>>Z>^>>>(>>x>\prime >>>a>\prime >>)>>,ver>>O>^>>>(>>a>\prime >>>b>\prime >>)>>,ver>>O>^>>>(>>b>\prime >>>y>\prime >>)>>\to ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>A>^>>>(>y>>y>\prime >>)>>>>$

最后，将以下约束添加到∑₂₃中：

$>ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>A>^>>>(>y>>y>\prime >>)>>,ver>>B>^>>>(>y>>y>\prime >>)>>\to >T>>(>xy>)>>.>>>$

现在假定PCP问题对{0，1}*上的串S有解。然后推导出无穷多个以下形式的约束：

xS^ky，x′S^ky′→T(xy)其中，S^k是串S如下重复k次。注意这些约束是在σ₁∪σ₃上，且其中没有哪一个能从任何其它约束获得。

对于k＝1(其它情形是类似的)，首先通过使用∑₁₂中的约束获得：

然后按序使用∑₂₃中对应于获得S所需的块序列的规则，通过消解获得：

xSy，x′SyS→A(xx′)，A(yy′)，B(yy′)。

最后使用∑₂₃中的最后约束获得：

xSy，x′SyS→T(x，y)

反过来，如果PCP问题在无解，在σ₁∪σ₃中的前提无推论，则以下结论是可能的：

$>ver>>A>^>>>(>x>>x>\prime >>)>>,ver>>A>^>>>(>y>>y>\prime >>)>>,ver>>B>^>>>(>y>\prime >y>)>>.>>>$

因为这是匹配σ₁∪σ₃中的结论的唯一前提，所以没有导出σ₁∪σ₃中的任何约束。在此情形中，∑₁₃＝给出合成m₁₂·m₂₃。

来自定理2的coRE-hardness隐含即使当合成是CQ₀^＝-映射关系时，算法CQ₀^＝合成也可能不终止。例如在以下实例中发生此情况。

示例5.考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给出的CQ₀-映射关系m₁₂和m₂₃，其中∑₁₂是：

R(xy)→S(xy)

R(xy)，R(yz)→R(xz)，R′(y)

S(xy)，S(yz)→S(xz)，S′(y)

而∑₂₃是：

S(xy)→T(xy)

并且其中σ₁，＝{R，R′}，σ₂＝{S，S′}，且σ₃＝{T}。以下约束：

R(xy)，R(yz)→R(xz)，R(y)

R(xy)→T(xy)准确地表达合成m₁·m₂，但算法CQ₀^＝合成将永不终止，因为它将推导出无穷多个其在示例3中所推导出的约束。

以下是算法CQ₀^＝合成终止的充分条件。如下，这些条件可在多项式时间检查。运行CQ₀^＝合成(∑₁₂，∑₂₃)的k_σ2-1次迭代，并检查∑中是否出现以下所给出形式的约束，其中k_σ2是σ₂中关系符号的个数。

定理3.在定理1的假设之下，如果仅使用σ₂-统一不能从∑₁₂₃推导出φ(z)，S(y)→S(x)形式的约束(这被称为坏约束)，其中：

1.φ(z)是σ₁₂₃上原子的逻辑乘，

2.φ(z)中没有满足{x}{w}的原子S(w)，

3.并且

4.S是σ₂中的关系符号，则CQ₀^＝合成(∑₁₂，∑₂₃)终止，因此m₁·m₂是CQ₀^＝-映射关系。对于CQ₀-映射关系同样成立。

证明.假定假设成立。考虑任何仅使用σ₂-统一证明∑₁₂₃ξ的推论γ，其中ξ在结论中包含一σ₂原子。不失一般性，假定首先执行所有重命名操作，接下来进行所有消解操作。还假定γ中的每个规则在其结论中包含单个原子，且每个规则至多在一个消解步骤中使用。

这一推论能以树T来表示，其中每个节点都是一个原子。T中每个非叶节点都是某个规则r的结论。r的子节点是规则r的前提中的原子。ξ的前提由T的所有叶节点和组成，且其结论是T的根节点。

为每个节点检查T的任何子树T(包含T中其所有子节点或不包含任何子节点)是否能被转换成证明∑₁₂₃ξ′的推论γ′是很简单的，其中ξ的前提由T的所有叶节点组成，且其结论为T′的根节点。

因为该假设成立，所以没有这样的子树可包含S(x)为其根节点，并包含S(y)为叶节点，其中S是σ₂中的关系符号且因此，T中从叶节点到根节点的、包含节点S(y)的任何路径至多仅可能包含具有S个原子的2^rr！⁸个其它节点，其中r是S的数量(arity)。这意味着任何此类路径必须具有由k_σ22^r_σ2r_σ2！界定的长度，其中k_σ2是σ₂中关系符号的个数，而r_σ2是σ₂中关系符号的最大数量。结果是，取决于变体数，通过σ₂-统一仅可获得有穷个数的∑₁₂₃的结论，且这隐含CQ₀^＝合成(∑₁₂，∑₂₃)终止。

定义3.如果CQ₀^＝-映射关系由(σ₁， σ₂，∑₁₂)给定且仅使用σ₁-统一或仅使用σ₂-统一不能从∑₁₂₃推导出任何满足以下各项的φ(z)，S(y)→S(x)形式的约束：

1.φ(z)是σ₁∪σ₂上原子的逻辑乘，

2.φ(z)中没有满足{x}{w}的原子S(w)，

3.并且

4.S和S＝″均为σ₁中的关系符号，或均为σ₂中的关系符号。则CQ₀^＝-映射关系是好CQ₀^＝-映射关系。类似地定义好CQ₀。

定理4.好CQ₀^＝和好CQ₀在合成和求逆下都是闭合的。

注释1.CQ₀^＝查询包括在好CQ₀^＝-映射关系中。注意总的和满射的CQ₀^＝-映射关系在合成下不是闭合的。

示例6.考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的CQ₀-映射关系m₁₂和m₂₃，其中∑₁₂是：

R(xy)→S(xy)

R(xy)，S(yz)→S(xz)而∑₂₃是：

S(xy)→T(xy)并且其中σ₁＝{R}，σ₂＝{S}，且σ₃＝{T}。此处m₁₂和m₂₃是总的和满射的，且其合成说明示例5中可见的tc(R)T甚至不能在FO中表达。

SOCQ^＝映射关系的合成

这部分的焦点是SOCQ^＝映射关系的合成。为了处理CQ^＝-映射关系中的存在量词，首先将CQ^＝-映射关系约束转换为斯柯伦形式，这产生SOCQ^＝映射关系。以下定理5示出，SOCQ^＝映射关系在合成下是闭合的，因为它能使用存在量化的函数符号来声明中间签名σ₂中关系的存在。

以下有关问题也很重要：

如果SOCQ^＝映射关系m₁₂、m₂₃由(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给定，是否有(σ₁，σ₃，∑₁₃)所给定的SOCQ^＝映射关系m₁₃满足m₁₃＝m₁₂·m₂₃以使∑₁₃SOCQ^＝除了∑₁₂∪∑₂₃中所出现的那些函数符号或常量以外，没有其它函数符号或常量。如果是，则说m₁₂和m₂₃具有保守合成。

保守合成是很重要的，因为最终需要消除所有函数符号以获取CQ^＝-映射关系，并且如何消除在等同中引入的函数符号(诸如以下定理5的证明中所使用的函数符号等)是未知的。以上部分的定理1和2示出，SOCQ和SOCQ^＝在保守合成下不是闭合的，且确定两个SOCQ^＝-映射关系的保守合成是否为SOCQ^＝-映射关系是不可决定的。如在CQ₀^＝-映射关系的情况，对具有保守合成的两个SOCQ^＝-映射关系给出充要的不可计算的条件，并给出可有效检查的保守合成的充分条件。给出一种保守合成的算法(SOCQ^＝合成)，它在SOCQ^＝-映射关系上正确工作，从而满足这些条件。此外，定义好SOCQ^＝为SOCQ^＝的多项式时间子集，它在保守合成下是闭合的。与前一部分相反，在此情况中证明，等式是必不可少的，因此这些结果对于SOCQ是不成立的。

在前进至结果以前，简要描述IC(SOCQ^＝)约束的语义。问题是，函数可取值的域是什么，即，它们所允许的范围什么？直观地，此问题是关于存在量化的中间数据库的域。所有数据库都被要求是有穷的(即，所有关系都是有穷的)，但具有隐式的可数无穷域。函数被允许从此隐式域中取任何值，只要它们的范围是有穷的。这些假定确保第2部分中所介绍的推论系统对于IC(SOCQ^＝)而言是健全的，这是以下定理6所需要的。

定理5.SOCQ^＝-映射关系在合成下是闭合的。

证明.如果SOCQ^＝-映射关系m₁₂和m₂₃由(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给定，获得∑₁₃以使合成m₁₂·m₂₃由(σ₁，σ₂，∑₂₃)如下给定。设∑₁₃：＝∑′₁₂∪∑′₂₃，其中∑′₁₂和∑′₂₃是通过用fin(x)，g_R(x)＝h_R(x)替换原子R(x)的每个出现而获得的，其中R∈σ₂，fin(x)，g_R(x)＝h_R(x)，其中fin(x)：＝_Λ_x∈{x}x＝f(x)，且f，g_R，h_R是新函数符号。

然后，如果<A，C>∈m₁₂·m₂₃，则存在B使当且仅当通过使用来自该域的任意两个值，对于σ₂中的每个关系R都有R(c)在B中成立，则设g_R(c)＝h_R(c)。此外，如果c在B的有效域中则设f(c)：＝c，否则设f(c)：＝c′，其中c′是来自该域的某个值。从而反过来，如果则为σ₂中的每个关系R设R：＝{c：fin(c)，g_R(c)＝h_R(c)}以获得B，以使fin(x)是有穷谓词，因为f的范围是有穷的。因此，B中的每个关系R都是有穷的。

定理6.如果SOCQ^＝-映射关系m₁₂和m₂₃由(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给定，并且有∑₁₂₃：＝∑₁₂∪∑₂₃和σ₁₃＝σ₁∪σ₃，则以下是等价的：

1.签名σ₁₃上存在有穷约束集合E₁₃IC(SOCQ^＝)使m：＝m₁₂·m₂₃由(σ₁，σ₃，∑₁₃)给定，其中除了∑₁₂₃中所出现的那些函数符号或常量以外，∑₁₃没有其它任何函数符号或常量。

2.签名σ₁₃上存在有穷约束集合∑₁₃IC(SOCQ^＝)使 $>>DC>>(>SOC>>Q>=>>,>>\Sigma >123>>)>>>|>>\sigma >13>>>=>>>$ >>DC>>(>SOC>>Q>=>>,>>\Sigma >13>>)>>,>>>其中除了\sum $$₁₂₃中所出现的那些函数符号或常量以外，∑₁₃没有其它任何函数符号或常量。

3.存在k使得对于σ₁₃上满足∑₁₂₃ξ的每一个ξ，都有最多使用k个σ₂-消解从∑₁₂₃的ξ的推论。

证明.本质上和定理3的证明一样，使用以下引论3代替引论1。

引论3.在定理6的假设之下，以下是等价的：

1.

2.

定理6提出本质上和CQ₀^＝-合成相同的SOCQ^＝-映射关系合成算法，称为SOCQ^＝合成。它们之间仅有的区别是SOCQ^＝合成对IC(SOCQ^＝)约束进行操作，而CQ₀^＝-合成对IC(CQ₀^＝)约束进行操作。如同为CQ₀^＝一样，为SOCQ^＝定义SOCQ^＝合成的正确性、其终止的充分条件、以及好SOCQ^＝-映射关系。

CO^＝-映射关系的合成

这部分考虑如何将SOCQ^＝-映射关系转换回CQ^＝-映射关系。考虑CQ-映射关系和CQ^＝-映射关系的情形。为了计算(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的两个CQ^＝-映射关系m₁₂、m₂₃的合成，进程由如下三个步骤组成。

过程CQ^＝合成(∑₁₂，∑₂₃)

    1.∑′₁₂：＝斯柯伦化(∑₁₂)          ∑′₂₃：＝斯柯伦化(∑₂₃)

    2.∑′₁₃：＝SOCQ^＝合成(∑′₁₂，∑′₂₃)

    3.返回 解除斯柯伦化(∑′₁₃)

第一步斯柯伦化，是很简单的。第二步SOCQ^＝合成，已在前面部分讨论过。对于第三步解除斯柯伦化，以下给出一种示出为正确的(见定理7)算法。事实表明，即使第二步成功，也可能找不到∑₁₃IC(CQ^＝)以使∑′₁₃≡E₁₃(见示例4)。因此，标识第三步成功的充要多项式时间可检查的条件(见命题2)。解除斯柯伦化可能产生与其输入的大小成指数比例的大小的结果。事实表明，在一般情况中，这是不可避免的(见定理8)，但提供多项式时间可检查的条件，以供解除斯柯伦化在多项式时间内以其输入的大小运行(见命题2)。

以下来自现有技术的示例表明，解除斯柯伦化不总是可能的。

示例7.考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的CQ^＝-映射关系m₁₂和m₂₃，其中：

∑₁₂是    E(x，y)→F(x，y)

$>>E>>(>x>,>y>)>>\to >\exists >uC>>(>x>,>u>)>>>>$

$>>E>>(>x>,>y>)>>\to >\exists >vC>>(>y>,>v>)>>>>$

∑₂₃是    F(x，y)，C(x，u)，C(y，v)→D(u，v)

并且其中σ₁＝{E}，σ₂＝{F，C}，且σ₃＝{D}。此处，CQ^＝合成的步骤1和2成功，但无论对其使用什么算法，步骤3都失败，因为m₁₂·m₂₃不是CQ^＝-映射关系，如

现有技术中所示。

以下给出的算法解除斯柯伦化依赖于^*，它是的某种多项式时间近似。即，如果∑^*φ，则反过来可能不成立。有已知的实例，其中存在此类^*并且还是完整的(即，反过来也成立)。例如，当∑具有分层证明时即为一例。为简单起见，不描述实现^*的选择。解除斯柯伦化对于满足以上条件的任何^*有效：更完全的^*是解除斯柯伦化成功的较大输入集合。由此，图8示出根据本发明的一种去斯柯伦化的方法。

过程解除斯柯伦化(∑)

在800，启动解嵌套的过程。设Λ₁：＝{φ′：φ∈∑}，其中φ′等价于φ，并且是通过“解嵌套”和消除来自关系型原子和来自结论的项从φ中获得的，以使在′中：

(a)函数符号仅在前提中的等式中出现。

(b)每个项f(u)仅在一个原子中出现。

(c)每个等式都是关于某个变量v(f的一项变量)、函数f、以及变量序列u(定义等式)或是两项变量u和v的v＝u的形式(限制等式)。

(d)结论至多包含一个原子，该原子不是定义等式。

其中发生项变量的关系型原子称为限制原子。如果A是其中发生v的限制关系型原子或限制等式，其中v是的项变量，则被称为f-限制原子。如果约束在前提中有限制原子，则称该约束为受限制的。

在802，进行环路的检查。对于每个φ∈Λ₁，构造图G_φ，其中边是φ中的变量，并且当且仅当有v＝f(...u...)形式的等式时，存在边(v，u)。如果G_φ有环路，则中止。否则设Δ₂：＝Λ₁。

在804，进行自变量兼容性的检查。对于每个φ∈Δ₂，检查是否φ不包含两个具有相同函数符号的原子。如果有，则中止。否则设Δ₃：＝Λ₂。

在806，将变量对齐。重命名Λ₃中的变量以获得Λ₄满足：

(a)对于Λ₄中的每一个函数符号f以及任意两个v＝f(u)和y＝f(x)形式的等式，v是和y相同的变量，且u是和x相同的变量序列。

(b)对于每两个不同的函数符号f和g，以及Δ₄中任意两个v＝f(u)和y＝g(x)形式的等式，v和y是不同的变量。

如果这不可能，则中止。

在808，消除限制原子。选择Λ₄中函数符号的某种排序：f₁，...，f_k。设Δ₀＝Λ₄。对于n＝1，...，k-1，设Δ_n+1：＝{φ′：φ∈Δ_n}，其中φ′是如下从φ获得。设ψ为从前提中移除f_n+1-限制原子后的φ。如果Δ_n^*ψ，设φ′：＝ψ；否则设φ′：＝φ。无论在哪种情形中，都有Δ_n+1≡Δ_n。设Λ₅：＝Δ_k。

在801，消除具有限制原子的约束。设Δ₆为根据以下测试不能被消除的约束集合φ∈Λ₅：如果

(a)φ在前提中包含f-限制原子，并且

(b)不存在结论中有f-限制原子且在前提中没有f-限制原子的约束ψ∈Λ₅，则φ能被消除。

在812，进行受限制约束的检查。设Λ为Λ₆中不受限制的约束集合。如果存在任何φ∈Λ₆使则中止。否则设Λ₇：＝Λ。

在814，进行依存关系的检查。对于每个φ∈Λ₇和φ中每个变量v，定义D_φ，v如下。如果v不是项变量，则设D_φ，v＝{v}。如果v是项变量且v＝f(u)是其在φ中的定义等式，则设D_φ，v：＝∪u∈{u}D_φ， u。直观地，D_φ，v是v所依赖的变量集合。设V_φ：＝在φ的结论中出现的变量集合。对于V_φ中每个项变量v，检查是否D_φ，v＝∪_u∈VφD_φ，u。如果此检查失败，则中止。否则设Λ₈：＝Λ₇。

在816，合并依存关系。设Λ₉：＝{ψ_Φ：≠ΦΛ₈}，其中ψ_Φ定义如下。如果存在出现在每个∈Φ中的函数f，则ψ_Φ的前提由Φ中所有前提中的原子组成，且ψ_Φ的结论由Φ的所有结论中的原子组成(移除重复的原子)。否则，ψ_Φ是Φ中的某个约束。注意Λ₉Λ₈，因为ψ_{φ}＝φ。

在818，移除冗余约束。选择某个集合Λ₁₀Λ₉使对于每个φ∈Λ₉都有Λ₁₀φ，并使此对Λ₁₀的任意本征子集不成立。

此外，在818，具有变量的函数被替换。设Λ₁₁：＝{φ′：φ∈Λ₁₀}，其中φ′的前提是移除其中所有等式后的的φ前提，且φ′的结论是φ中的等同的左边所出现的所有变量被存在地量化后的φ的结论。

在802，消除非必要的变量。设Λ₁₂：＝{φ′：φ∈Λ₁₁)，并返回Λ₁₂，其中φ′类似于φ，但其中未在结论原子中出现的被存在地量化的变量(以及其对应的存在量词)已被移除。

示例8.考虑算法解除斯柯伦化(∑₁₃ⁱ)对于i∈{1，2，3)的三次运行。令 $>sup>>\Sigma >13>isup>>=>\{>>\gamma >1>>,>.>.>.>,>>\gamma >i>>\}>>>为以下(已解嵌套的)SOCQ＝-依存关系集合：$

γ₁    R₁(y)，R₂(x)，y＝f(x)→T₁(x)

γ₂    R₂(x)，y＝f(x)→T₂(y)

γ₃    R₂(x)，y＝f(x)→R₁(y)

为完整性起见，注意每个∑₁₃ⁱ是通过首先解除斯柯伦化由∑₁₂ⁱ和∑₂₃ⁱ所给定的如下所示的CQ^＝-映射关系，然后调用SOCQ^＝合成：

i∑₁₂ⁱ∑₂₃ⁱ ∑₁₃ⁱ1.2.3.{α₁，α₂}{α₁，a₂}{α₁，α₂，α₃}{β₂}{β₁，β₂}{β₁，β₂}{γ₁}{γ₁，γ₂}{γ₁，γ₂，γ₃}

依存关系α₁、α₂、α₃、β₁、β₂被指定为：

α₁    R₁(x)→S₁(x)

α₂ $>>>R>2>>>(>y>)>>\to >\exists >z>>(>>S>2>>>(>zy>)>>)>>>>$

α₃    S₂(zy)→R₁(z)

β₁    S₂(zy)→T₂(z)

β₂    S₁(x)，S₂(xy)→T₁(y)

在解除斯柯伦化(∑₁₃ⁱ)的所有三次运行中，过程802和804通过，因为γ₁、γ₂、γ₃中的每一个都是无环路的，并且没有多个具有同一函数符号的原子。过程806没有效果，因为依存关系的变量名已被对齐。其余过程在以下解释。

在解除斯柯伦化({γ₁})的运行中，过程808没有效果，因为{γ₁}是单元素集合。其唯一的成员γ₁在过程810中被消除，因为{γ₁}中没有在结论中具有f-限制原子的规则。直观地，γ₁是重言式的，因为可构建其范围与R₁不相交的f。因此，{γ₁}等价于空约束集合，这在IC(CQ)中是平凡的。

在解除斯柯伦化({γ₁，γ₂})的运行中，γ₂在其结论中包含f-限制原子T₂。因此，受限制的约束γ₁不能在过程810中被消除，因此解除斯柯伦化在过程812中止。

在解除斯柯伦化({γ₁，γ₂，γ₃})的运行中，尽管有γ₂，解除斯柯伦化仍是可能的。在过程808，Δ₀＝{γ₁，γ₂，γ₃}。通过考虑唯一函数符号f，取Δ₁{ψ，γ₂，γ₃}≡Δ₀，其中ψ是通过从γ₁的前提中如下消除限制原子R₁(y)来获得的：

ψ：＝R₂(x)，y＝f(x)→T₁(x)。

很明显，Δ₀^*ψ，因为Δ₀{γ₁，γ₃}^*ψ。Δ₁没有限制约束，所以过程810没有效果，且过程812通过。过程814成功，并有Λ₈＝Λ₇＝{ψ，γ₂，γ₃}，因为Δ₁中的每个依存关系在其结论中至多有一个项变量y。例如，对γ₃进行计算产生V_γ3＝{x，y}，D_γ3，x＝D_γ3，y＝∪_u∈Vγ3 D_γ3，u＝{x}。在过程816中，为Φ＝Λ₈合并依存关系产生

γ₄：＝R₁(y)，R₂(x)，y＝f(x)→T₁(x)，T₂(y)，R₁(y)(合并由Λ₈的本征子集产生，为简化起见未示出。)在过程818中，包括ψ、γ₂、γ₃的冗余约束被移除，因为它们和γ₄有相同的前提，且它们的结论为γ₄的结论所包含；结果是Λ₁₀＝{γ₄}。最后，在818，用γ₄中的存在变量替换函数f产生

因此，解除斯柯伦化({γ₁，γ₂，γ₃})IC(CQ)

定理7.如果解除斯柯伦化(∑)在输入∑IC(SOCQ^＝)上成功，则Σ′：＝解除斯柯伦化(∑)满足

∑′IC(CQ^＝)且∑′≡∑。

以下从该算法的描述推出。

命题3.

1.当且仅当解除斯柯伦化(∑)到达过程816时，它在输入∑IC(SOCQ^＝)上成功，这可在大小为∑的多项式时间中检查。

2.此外，如果对于某个独立于∑的变量l，对于Λ₈中的每个函数符号，f至多在Λ₈中的l个规则中发生，则解除斯柯伦化(∑)在大小为∑的多项式时间中运行。

从命题3的第一部分，推出CQ^＝合成(∑₁₂，∑₂₃)能在多项式时间中被成功检查的充分条件，因为斯柯伦化的结果的大小与其输入的大小是多项式关系，还因为可在多项式时间为SOCQ^＝合成(∑′₁₂，∑′₂₃)的中止检查充分条件。

因为解除斯柯伦化(∑)由于过程816而可能产生和∑的大小成指数比例的大小的结果，所以CQ^＝合成(∑₁₂，∑₂₃)可能产生和∑₁₂∪∑₂₃的大小成指数比例的大小的结果。以下示例示出在一般情形这是不可避免的。但是，命题3的第二部分示出，我们能够有效检查不但确保解除斯柯伦化成功，还确保其在多项式时间内中止的更具限制性的条件。

定理8.对于任何亚指数函数f，都有(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)给定的源到目标的CQ-映射关系m₁₂和m₂₃，使得对于任何大小小于f(s)的∑₁₃，m₁₃：＝m₁₂·m₂₃是并非由(σ₁，σ₃，∑₁₃)给定的CQ-映射关系，其中s是∑₁₂∪∑₂₃的大小。

证明.(概述)选择足够大的k，使f(2kl)＜2^k，其中l是以下最长约束的大小(其中9的长度大约是18+logk个字符)。这一k必定存在，因为f是亚指数的。设[k]：＝{1，...，k)。考虑(σ₁，σ₂，∑₁₂)和(σ₂，σ₃，∑₂₃)所给定的CQ^＝-映射关系m₁₂和m₂₃，其中：

∑₁₂是 $>>>R>0>>>(>x>)>>\to >\exists >y>>S>0>>>(>xy>)>>>>$

          R_i(x)→S_i(x)

∑₂₃是    S₀(xy)，S_i(x)→T_i(y)i∈[k]，并且其中σ₁＝{R_i：i∈{0，...，k}}、σ₂＝{S_i：i∈{0，...，k}}、且σ₃＝{T_i：i∈[k]}。合成m₁₃：＝m₁₂·m₁₃是由以下约束的集合∑₁₃所给定：

$>>>R>0>>>(>x>)>>,>>R>Z>>>(>x>)>>\to >\exists >y\; >>T>Z>>>(>y>)>>>>$

以使Z[k]，其中R_Z(x)：＝_i∈ZR_i(x)，对于T_Z也是类似的。另一方面，m₁₃不是由任何(σ₁，σ₃，∑)所给定的，其中∑有少于2^k-1个约束。

域、范围和其它算子

合成是取模型和/或映射关系作为输入，并给出模型和/或映射关系作为输出的算子之一。合成可使用组合或其它算子来执行，这些算子进而可使用如上简述的类似技术来实现。这些其它算子包括：

域      dom(m)

范围    rng(m)

交集    A∩B

恒等    id(A)

叉乘    A×B

交      m₁∩m₂

逆      m^-1

这些算子定义如下。

A∩B：＝{A：A∈A，A∈B}。

id(A)：＝{<A，A>：A∈A}。

A×B：＝{<A，B>：A∈A，B∈B}。

m₁∩m₂：＝{<A，B>：<A，B>∈m₁<A，B>∈m₂}。

m^-1：＝{<B，A>：(A，B>∈m}。

在具有签名的关系型情形中，签名与每个模型相关联，且输入和输出签名与每个映射关系相关联，并且这些算子上的明显签名兼容性是必须的。

命题4.每个ΛCQ₀在恒等、叉乘和交集下是闭合的。

证明.如果m₁₂和m₃₄是由(σ₁，σ₂，∑₁₂)和(σ₃，σ₄，∑₃₄)给定的，且A和B是由(σ₁，∑₁)和(σ₂，∑₂)给定的，则

·A×B由(σ₁，σ₂，∑₁∪∑₂)给定。

·A∩B由(σ₁，∑₁∪∑₂)给定(此处σ₁＝σ₂)。

·m₁₂∩m₃₄由(σ₁，σ₂，∑₁₂∪∑x)给定(此处σ₁＝σ₃，且σ₂＝σ₄)。

为表达恒等，参考第三辅助签名σ₂′(通常被忽略)，对于σ₂中的每个关系符号R，它包含相同元数的关系符号。在此实例中，σ₁＝σ₂，因此 $>sup>>\sigma >2>\prime sup>>=sup>>\sigma >1>\prime sup>>.>>>$

·id(A)由(σ₁，σ₁，σ₁′，∑₁∪∑)给定，其中对于σ₁中的每个R，∑由以下形式的两个约束组成：

(x)(Rx→R′x)

(x)(R′x→Rx)

命题5.算子、合成、范围和域的每一个都能被相互约简。

证明.假设

·m₁₂由(σ₁，σ₂，∑₁₂)给定，

·m₂₃由(σ₂，σ₃，∑₂₃)给定，

令

·m₁由(σ₁ ∪σ₃，σ₂，∑₁₂∪∑₂₃)给定，

·m₂由(σ₂，σ₁∪σ₃，∑₁₂∪∑₂₃)给定，

·dom(m₁)由(σ₁∪σ₃，∑₁)给定，且

·rng(m₂)由(σ₁∪σ₃，∑₂)给定，

则m₁₂·m₂₃由(σ₁，σ₃，∑₁)并由(σ₁，σ₃，∑₂)给定。

这证明合成可由域或范围来表达。

反过来，假设

·m₁₂由(σ₁，σ₂，∑₁₂)给定。

令

·m₂₁由(σ₂，σ₁，)给定

·m₁₂·m₂₁由(σ₁，σ₁，∑₁)给定，且

·m₂₁·m₁₂由(σ₂，σ₂，∑₂)给定，

则dom(m₁₂)和rng(m₁₂)分别由以下两者给定：

   (σ₁，∑₁)和(σ₂，∑₂)

这证明域和范围可由合成表达。

所考虑的所有语言都满足命题4的前提。因此，命题5表明在合成和求逆下，注意力可集中在闭合上。注意，如果Λ-映射关系m由(σ₁，σ₂，∑₁₂)给定，则其逆由(σ₂，σ₁，∑₁₂)给定。但是，Λ上的约束可能使第二表达式不再给出Λ-映射。例如，“源到目标”表达式出现这种情况。相反，CQ0^＝、CQ^＝和SOCQ^＝映射关系在求逆下是闭合的，所以研究组合就足够了。

命题5隐含可用来实现域和范围的任何算法过程可被用来实现合成。这可以通过调用以上给出的算法来直接实现，或通过首先执行域和范围算子，然后使用其结果获得合成来间接实现。

计算环境

现在参考图9，图示出可用于执行所揭示的体系结构的计算机的框图。为了给本发明的各个方面提供其它上下文，图9和以下讨论旨在提供可在其中实现本发明的各个方面的合适的计算环境900的简要的一般描述。尽管以上在可在一个或多个计算机上运行的计算机可执行指令的通用上下文中描述了本发明，但是本领域技术人员可以认识到，本发明还可结合其它程序模块，和/或作为硬件和软件的结合来实现。

一般而言，程序模块包括执行特定任务或实现特定抽象数据类型的例程、程序、组件、数据结构、等等。此外，本领域技术人员将会理解，本发明方法可用其它计算机系统配置来实施，包括单处理器或多处理器计算机系统、小型计算机、大型计算机、以及个人计算机、手持式计算设备、基于微处理器的或可编程的消费者电子设备、等等，其中每一个操作上都可被耦合到一个或多个相关联的设备。

所示出的本发明的方面还可在分布式计算环境中实施，其中某些任务是由通过通信网络连结的远程处理设备来执行的。在分布式计算环境中，程序模块可位于本地和远程记忆存储设备中。

计算机通常包括各种计算机可读介质。计算机可读介质可以是能由计算机访问的任何可用介质，包括易失性和非易失性介质、可移动和不可移动介质。作为示例，而非限制，计算机可读介质可包括计算机存储介质和通信介质。计算机存储介质包括以用于存储诸如计算机可读指令、数据结构、程序模块或其它数据等信息的任何方法或技术实现的易失性和非易失性、可移动和不可移动介质。计算机存储介质包括，但不限于，RAM、ROM、EEPROM、闪存或其它存储器技术，CD-ROM、数字视频盘(DVD)或其它光盘存储，磁带盒、磁带、磁盘存储或其它磁存储设备，或可用来存储所需信息并可由计算机访问的任何其它介质。

通信介质通常具体化为诸如载波或其它传输机制等已调制数据信号中的计算机可读指令、数据结构、程序模块或其它数据，并包括任何信息传递介质。术语“已调制信号”指以在信号中对信息编码的方式设置或改变其一个或多个特征的信号。作为示例而非限制，通信介质包括诸如有线网络或直接连线连接等有线介质，及诸如声学、RF、红外及其它无线介质等无线介质。以上的任意组合也应被包括在计算机可读介质的范畴内。

再次参考图9，图示出包括计算机902的用于实现本发明的各个方面的示例性环境900，计算机902包括处理单元904、系统存储器906和系统总线908。系统总线908将包括，但不限于，系统存储器906在内的系统组件耦合到处理单元904。处理单元904可以是各种市场上可购买的处理器中的任何一种。双微处理器和其它多处理器体系结构也可作为处理单元904使用。

系统总线908可以是若干类型的总线结构中的任何一种，该总线结构还可被互连到存储器总线(带或不带存储器控制器)、外围总线、和使用各种市场上可购买的总线体系结构中的任何一种的局部总线。系统存储器906包括只读存储器(ROM)910和随机存取存储器(RAM)912。基本输入/输出系统(BIOS)存储在诸如ROM、EPROM、EEPROM等非易失性存储器910中，BIOS包含诸如在启动期间帮助在计算机902内部各元件之间传递信息的基本例程。RAM 912还可包括诸如用于高速缓存数据的静态RAM等高速RAM。

计算机902还包括内置硬盘驱动器(HDD)914(例如，EIDE、SATA)(内置硬盘驱动器914还可被配置成在合适的机箱(未示出)中的外置使用)、软磁盘驱动器(FDD)916(例如，读或写可移动磁盘918)和光盘驱动器920(例如，读CD-ROM盘922，或者读或写诸如DVD等其它高容量光介质)。硬盘驱动器914、磁盘驱动器916和光盘驱动器920可分别由硬盘驱动器接口924、磁盘驱动器接口926和光盘驱动器接口928连接到系统总线908。供外置驱动器实现使用的接口924包括通用串行总线(USB)和IEEE 1394接口技术中的至少一种或两种。

各驱动器及其相关联的计算机可读介质提供数据、数据结构、计算机可执行指令等的非易失性存储。对于计算机902而言，各驱动器及介质容纳适当数字格式的任何数据的存储。尽管以上对计算机可读介质的描述指HDD、可移动软盘、和诸如CD或DVD等可移动光盘，但是本领域技术人员应当理解，计算机可读的其它类型的介质，诸如zip驱动器、磁带、闪存卡、卡式磁带盒等，也可在示例性操作环境中使用，此外，任何此类介质可包含用于执行本发明的方法的计算机可执行指令。

若干程序模块可被存储在各驱动器和RAM 912中，包括操作系统930、一个或多个应用程序932、其它程序模块934和程序数据936。操作系统、应用程序、模块、和/或数据的全部或部分可被高速缓存在RAM 912中。应理解，本发明可用各种市场上可购买的操作系统或若干种操作系统的组合来实现。

用户可通过例如键盘938和诸如鼠标940等定位设备等一个或多个有线/无线输入设备，将命令和信息输入到计算机902中。其它输入设备(未示出)可包括话筒、IR遥控、操纵杆、游戏垫、记录笔、触摸屏、等等。这些及其它输入设备常常通过耦合到系统总线908的输入设备接口942连接到处理单元904，但也可通过诸如并行接口、IEEE 1394串行端口、游戏端口、USB端口、IR接口等其它接口连接。

监视器944或其它类型的显示设备也经由诸如视频适配器946等接口连接到系统总线908。除了监视器944以外，计算机通常包括诸如扬声器、打印机等其它外围输出设备(未示出)。

计算机902可使用经由有线和/或无线通信到诸如远程计算机948等一个或多个远程计算机的逻辑连接，在联网环境中工作。远程计算机948可以是工作站、服务器计算机、路由器、个人计算机、便携式计算机、基于微处理器的娱乐装置、对等设备或其它普通网络节点，并通常包括以上相对于计算机902所描述的许多或所有元件，尽管出于简化目的，仅示出一记忆存储设备950。所示逻辑连接包括到局域网(LAN)952或例如广域网(WAN)954等较大网络的有线/无线连接。此类LAN和WAN网络环境常见于办公室和公司，并便于实现诸如内联网等企业范围的计算机网络，所有这些网络可连接到例如因特网等全球通信网络。

当在LAN网络环境中使用时，计算机902通过有线和/或无线通信网络接口或适配器956连接到局域网952。适配器956可便于到LAN 952的有线或无线通信，LAN 952还可包括布置在其上的无线接入点，用于与无线适配器956进行通信。

当在WAN网络环境中使用时，计算机902可包括调制解调器958，或者被连接到WAN 954上的通信服务器，或具有通过WAN 954建立通信的其它装置，诸如通过因特网。可以是内置的或外置的、有线或无线设备的调制解调器958经由串行端口接口942连接到系统总线908。在联网环境中，相对于计算机902所描述的程序模块或其部分可存储在远程存储器/存储设备950中。可以理解，所示网络连接是示例性的，且可使用在计算机之间建立通信链路的其它装置。

计算机902可用于与操作上布置在无线通信中的任何无线设备或实体通信，例如，打印机、扫描仪、台式和/或便携式计算机、便携式数据助理、通信卫星、与无线可检测标签相关联的任何设备或位置(例如，电话亭、报摊、休息室)、以及电话。这至少包括Wi-Fi和Bluetooth^TM(蓝牙)无线技术。因此，通信可以是如常规网络等预定义的结果，或仅仅是至少两个设备之间的特定通信。

Wi-Fi，或称无线保真，允许从家里的靠椅、酒店房间的床、工作处的会议室到因特网的无线连接。Wi-Fi类似于蜂窝电话中所使用的无线技术，它所使用的无线技术使例如计算机等设备在基站范围内的任何地方在室内或室外发送和接收数据。Wi-Fi网络使用称为IEEE 802.11(a、b、g等)无线电技术来提供安全、可靠、快速的无线连接。Wi-Fi网络可用于将计算机连接到其它计算机、因特网和有线网络(使用IEEE 802.3的有线网络或以太网)。Wi-Fi网络以例如11Mbps(802.11a)或54Mbps(802.11b)的数据率在未注册的2.4和5GHz无线电波段工作，或用包含两个波段(双波段)的产品工作，因此该网络能提供类似于在许多办公室中使用的10BaseT有线以太网的实际性能。

现在参考图10，图示出根据本发明的示例性计算环境1000的示意性框图。系统1000包括一个或多个客户机1002。客户机1002可以是硬件和/或软件(例如，线程、进程、计算设备)。客户机1002可通过使用本发明来容纳例如cookie和/或相关联的上下文信息。

系统1000还包括一个或多个服务器1004。服务器1004也可以是硬件和/或软件(例如，线程、进程、计算设备)。例如，服务器1004可通过使用本发明来容纳执行转换的线程。客户机1002和服务器1004之间一种可能的通信可以是适用于在两个或多个计算机进程之间被发送的数据分组的形式。数据分组可包括例如cookie和/或相关联的上下文信息。系统1000包括通信框架1006(例如，诸如因特网等全球通信网络)，该通信框架1006可用来便于在客户机1002和服务器1004之间的通信。

经由有线(包括光纤)和/或无线技术，可促进通信。客户机1002操作上连接到一个或多个客户机数据存储1008，它们可用来将信息本地存储到客户机1002中(例如，cookie和/或相关联的上下文信息)。类似地，服务器1004操作上连接到一个或多个服务器数据存储1010，它们可用来将信息本地存储到服务器1004。

以上所述包括本发明的若干示例。当然，出于描述本发明的目的，要描述组件和方法的每一种可构想的组合是不可能的，但是本领域普通技术人员可以认识到，本发明的许多其它组合和变更是可能的。因此，本发明旨在包括所有这些落入所附权利要求书范围之内的替换、修改和变体。此外，在详细描述或权利要求书中使用术语“包括”的意义上，此类术语意图如术语“包含”那样为包含性的，如“包含”在权利要求书中用作过渡词所解释的。