# Patent

## Title
System and method for composition of mappings given by dependencies

## Abstract

A system that facilitates composition of schema mappings. A general algorithm is provided for composing a broad class of mappings, where one or both mappings are not functions, such as constraints between two schemas and the inverse of functions. A composition component performs composition on schema mappings of disparate data sources, which schema mappings can be expressed by at least one of full, embedded, and second-order dependencies, wherein the second-order dependencies need not be in source-to-target form. The algorithm for composition further includes a procedure that tests whether the composition algorithm will terminate.

## Background
TECHNICAL FIELD
This invention is related to systems and methods of constructing a mapping between database schemas, which mapping is composed from existing mappings.
BACKGROUND OF THE INVENTION
The advent of global communications networks such as the Internet has facilitated access to enormous amounts of data. The world is populated with information sources where in many cases the data is represented differently from source to source. The free flow of information prevalent today in wired and wireless regimes demands that the source and destination be compatible insofar as storing and interpreting the data for use. A major problem facing companies and individuals today is that the data existing in one model/schema needs to be accessed via a different model/schema. However, such processes are being hampered by a largely disparate and ever-changing set of models/schemas. Such an example can be found in data warehousing where data is received from many different sources for storage and quick access from other sources. Converting data from one model to another model is not only time-consuming and resource intensive, but can be fraught with conversion problems.
Schema mappings specify the relationships between heterogeneous database sources and are used to support data transformation, data exchange, schema evolution, constraint checking, and other tasks. Mapping composition is an operation that takes as input two mappings mapAB and mapBC between schemas A, B, C and produces a single mapping mapAC that specifies the same set of constraints between A and C that is given by the combined mappings mapAB and mapBC.
To illustrate the use of mapping composition, consider the following schema evolution scenario. Assume that S1, S2, S3, S4 are versions of a schema used in successive releases of a product. The mapping map12 is used to migrate data from schema S1's format to schema S2's format. Similarly, mapping map23 is used to migrate data from schema S2's format to schema S3's format, and finally, map34 is used to migrate data from schema S3's format to schema S4's format. A conventional way of migrating the data from version S1 to version S4 is by executing map12, map23, map34 one by one, which is time-consuming and costly. To migrate the data from S1 to S4 in a single step, mapping composition is required. The mapping map14 can be obtained by first composing map12 and map23, and then composing the resulting mapping with map34.
Now suppose V1 is a view defined on S1 and map1V1 is a function. To migrate view V1 from S1 to S2, composition is again used. The inverse of mapping map12 is composed with map1V1 to obtain a mapping map2V1 from S2 to V1.
Algorithms for mapping composition are well-known for the case where each mapping is a function (i.e., maps one database state to exactly one database state, and both mappings have the same directionality). However, there is a substantial unmet need for an algorithm which is suitable for a broader class of mappings where one or both mappings are not functions.
SUMMARY OF THE INVENTION
The following presents a simplified summary of the invention in order to provide a basic understanding of some aspects of the invention. This summary is not an extensive overview of the invention. It is not intended to identify key/critical elements of the invention or to delineate the scope of the invention. Its sole purpose is to present some concepts of the invention in a simplified form as a prelude to the more detailed description that is presented later.
The invention is a general algorithm that is suitable for composing a broader class of mappings, where one or both mappings are not functions, such as constraints between two schemas and the inverse of functions. This enables construction of a mapping between database schemas from two existing mappings by composing them. The algorithm for composition includes a procedure that tests whether the composition algorithm will terminate.
The invention disclosed and claimed herein, in one aspect thereof, comprises a system that facilitates composition of schema mappings. A composition component performs composition on existing schema mappings of disparate data sources, which schema mappings can be expressed by at least one of full, embedded, and second-order dependencies, wherein the second-order dependencies need not be in source-to-target form.
In another aspect of the subject invention, a methodology is provided for composing two schema mappings by Skolemizing the schema mappings expressed by the embedded dependencies to obtain schema mappings expressed by the second-order dependencies; computing a finite axiomatization of all constraints over input and output signatures which can be deduced from the constraints that give the schema mappings; and de-Skolemizing a finite axiomatization to obtain a schema mapping expressed by an embedded dependency.
In still another aspect thereof, a methodology is provided where the act of de-Skolemizing the finite axiomatization further comprises unnesting Skolem functions using equality to generate a conclusion; checking that all variables in the conclusion appear in a variable dependency set of the Skolem functions; generating all possible clauses that can be obtained by unifying Skolem functions that appear in the conclusion; and de-Skolemizing each clause separately by substituting each Skolem term by a new existential variable.
To the accomplishment of the foregoing and related ends, certain illustrative aspects of the invention are described herein in connection with the following description and the annexed drawings. These aspects are indicative, however, of but a few of the various ways in which the principles of the invention can be employed and the subject invention is intended to include all such aspects and their equivalents. Other advantages and novel features of the invention will become apparent from the following detailed description of the invention when considered in conjunction with the drawings.



BRIEF DESCRIPTION OF THE DRAWINGS
FIG. 1 illustrates a diagram that represents construction of a resulting mapping by composition of two existing mappings between database schemas in accordance with the subject invention.
FIG. 2 illustrates a diagram that represents mapping composition of logical constraints in accordance with the invention.
FIG. 3 illustrates a methodology of composition of dependencies in accordance with the invention.
FIG. 4 illustrates a composition methodology in accordance with the invention that imposes conditions and employs checks to determine if composition terminates to a correct answer.
FIG. 5 illustrates a methodology of performing de-Skolemization on a finite axiomatization to obtain an embedded dependency in accordance with the invention.
FIG. 6 illustrates a diagram of multiple compositions on more than three data source schemas in accordance with the invention.
FIG. 7 illustrates composition of multiple mappings that can be performed using a single invocation of the algorithm to obtain the output mapping, in accordance with the invention.
FIG. 8 illustrates a methodology for de-Skolemization in accordance with the subject invention.
FIG. 9 illustrates a block diagram of a computer operable to execute the disclosed architecture.
FIG. 10 illustrates a schematic block diagram of an exemplary computing environment in accordance with the subject invention.



DETAILED DESCRIPTION OF THE INVENTION
The invention is now described with reference to the drawings, wherein like reference numerals are used to refer to like elements throughout. In the following description, for purposes of explanation, numerous specific details are set forth in order to provide a thorough understanding of the subject invention. It may be evident, however, that the invention can be practiced without these specific details. In other instances, well-known structures and devices are shown in block diagram form in order to facilitate describing the invention.
As used in this application, the terms “component” and “system” are intended to refer to a computer-related entity, either hardware, a combination of hardware and software, software, or software in execution. For example, a component can be, but is not limited to being, a process running on a processor, a processor, an object, an executable, a thread of execution, a program, and/or a computer. By way of illustration, both an application running on a server and the server can be a component. One or more components can reside within a process and/or thread of execution, and a component can be localized on one computer and/or distributed between two or more computers.
Composition of Mappings
The subject invention is a general algorithm that is suitable for composing a broader class of mappings, where one or both mappings are not functions, such as constraints between two schemas (such as map12, map23, and map34) and the inverse of functions (such as the inverse of map12).
FIG. 1 illustrates a diagram 100 that represents construction of a resulting mapping 102 by composition of two existing mappings (104 and 106) between database schemas (not shown) in accordance with the subject invention. A first schema mapping 104 (denoted SCHEMA MAPPING12) is provided and which can be a function or a non-function. Similarly, a second schema mapping 106 (denoted SCHEMA MAPPING23) is provided and can be a function or a non-function. Algorithms for mapping composition are well-known for the case where each mapping is a function. Thus, the invention addresses instances only where one or both of the mapping schemas (104 and 106) is a non-function.
As illustrated by the dashed lines, the following scenarios are addressed: when the first schema mapping 104 is a function, the second schema mapping 106 is a non-function; when the first schema mapping 104 is a non-function, the second schema mapping 106 is a function; and, when the first schema mapping 104 is a non-function, the second schema mapping 106 is a non-function. The schema mappings (104 and 106) are composed using a composition algorithm component 108 to generate the resulting mapping 102 (denoted SCHEMA MAPPING13). The composition component 108 employs a deductive procedure to obtain a finite axiomatization of all constraints that need to appear in the composition mapping. This is described in detail infra.
In any of the three non-function mappings, the mappings can be represented by logical constraints, or clauses. FIG. 2 illustrates a diagram 200 that represents mapping composition of logical constraints in accordance with the invention. There are provided three data base schemas 202 (denoted S1, S2, and S3) from which first and second schema mappings (204 and 206) (denoted respectively as MAPPING12 and MAPPING23) are derived.
A compose component 208 (similar to component 108) facilitates composition of the two schema mappings (204 and 206) into a resulting schema mapping 210 (denoted MAPPING13). The considered constraint languages include full dependencies (CQ0= mappings), embedded dependencies (CQ= mappings), or second-order dependencies (SOCQ= mappings, also called second-order tuple-generating dependencies). Thus, each of the first and second mappings (204 and 206) can include constraints which are full, embedded and/or second-order dependencies. Given two finite CQ0=, CQ=, or SOCQ= mappings map12 and map23 that are not necessarily functional, the challenge is to find a CQ0=, CQ=, or SOCQ= mapping that specifies the resulting mapping 210 of the composition of map12 and map23.
Referring now to FIG. 3, there is illustrated a methodology of composition of dependencies in accordance with the invention. While, for purposes of simplicity of explanation, the one or more methodologies shown herein, e.g., in the form of a flow chart, are shown and described as a series of acts, it is to be understood and appreciated that the subject invention is not limited by the order of acts, as some acts may, in accordance with the invention, occur in a different order and/or concurrently with other acts from that shown and described herein. For example, those skilled in the art will understand and appreciate that a methodology could alternatively be represented as a series of interrelated states or events, such as in a state diagram. Moreover, not all illustrated acts may be required to implement a methodology in accordance with the invention.
The composition is computed in three steps: the CQ= mappings are Skolemized to get the second-order dependencies (SOCQ=) mappings. Skolemization is a way to remove existential quantifiers from a formula. Next, a finite axiomatization of all constraints over the input and output signatures is found that can be deduced from the constraints that give the mappings. Finally, the finite axiomatization is de-Skolemized to get a CQ= mapping. Accordingly there is provided a methodology, such that, at 300, the embedded dependencies are Skolemized to obtain the second-order dependencies. At 302, a finite axiomatization of all constraints over input and output signatures is found. The axiomatizations can be deduced from constraints that give the mappings. At 304, the finite axiomatization is de-Skolemized to obtain the embedded dependencies.
In the case of CQ0= mappings and SOCQ= mappings, only act 302 of FIG. 3 applies. Accordingly, FIG. 4 illustrates a composition methodology in accordance with the invention that imposes conditions and employs checks to determine if composition terminates to a correct answer. At 400, the compose algorithm is run. The following algorithm compose assumes that the input mapping map12 is specified by finite sets of CQ0= dependencies Σ12 between schemas S1 and S2, the input mapping map23 is specified by Σ23 between S2 and S3, and the output mapping map13 is given by Σ13 between S1 and S3. (Generalization of this basic algorithm for CQ= and SOCQ= mappings is presented infra.)
Algorithm compose (Σ12, Σ23):















Set Σ := Σ12 ∪ Σ23



Repeat



 Set Σ′ := Ø



 For every pair of clauses φ, ψ in Σ



  If there exists a σ2-resolvent χi of φ, ψ



   and there is no variant of χi in Σ



  then set Σ′ := Σ′ ∪ {χi}



  Set Σ := Σ ∪ Σ′



Until Σ′ = Ø



Return Σ13 := constraints in Σ that refer only to symbols of S1, S3










When compose terminates, it is proven that the algorithm gives the correct answer. However, compose may not terminate. At 402, conditions are imposed to check termination of the algorithm. The following conditions can be included to test the sufficiency for algorithm compose to terminate. These conditions can be checked in polynomial time, as indicated at 404, by running k−1 iterations of compose(Σ12, Σ23), where k is the number of relation symbols in S2 and then checking whether a constraint of the form φ(z),R(y)→R(x) appears in Σ, such that,

    
    
        (1) φ(z) is a conjunction of atoms over S1 ∪ S3;
        (2) {x} is not a subset of {y}; and
        (3) R is a relation symbol in S2.

At 406, once the conditions are satisfied, the compose algorithm terminates with the correct answer.

    
    


In order to obtain the embedded dependency, as indicated by act 304 (Step 3) of FIG. 3, an algorithm is provided that gives the correct results. Accordingly, FIG. 5 illustrates a methodology of performing de-Skolemization on a finite axiomatization to obtain an embedded dependency in accordance with the invention. At 500, Skolem functions are unnested using equality to reach a conclusion. At 502, a check is made to ensure that all variables in the conclusion appear in the variable dependency set of each Skolem function. At 504, if all variables in the conclusion appear in the variable dependency, flow is to 506, generate all possible clauses that can be obtained by unifying Skolem functions that appear in the conclusion. At 508, each clause is de-Skolemized separately by substituting each Skolem term with a new existential variable. However, at 504, if all variables do not appear, flow is to 510, where Skolemization fails, and progress ends.
FIG. 6 illustrates a diagram 600 of multiple compositions on more than three data source schemas 602 in accordance with the invention. Each pair of data source schemas 602 (denoted S1, S2, S3, . . . , SN) is associated with a first-order schema mapping 604 (denoted M12, M23, . . . M(N−1)(N)). Each pair of first-order schema mappings 604 is further composed by a composition component (denoted CN). That is, the first pair of first-order schema mappings (M12 and M23) is composed using a first composition component 606 (denoted C1) to generate a resulting second-order schema mapping M13. The resulting second-order mapping M13 is then composed with the next first-order schema mapping M34 using a different composition component C2 (or the same composition component C1). The process continues until no more first-order schema mappings 604 are available to be composed, and generating the resulting schema mapping M1N at the output.
Alternatively, or in addition to the algorithm of FIG. 6, FIG. 7 illustrates a system 700 that facilitates composition of multiple mappings that can be performed using a single invocation of the algorithm to obtain the output mapping M1N. Here, a composition component 704 receives multiple inputs of the first-order schema mappings 702 (denoted (denoted M12, M23, . . . M(N−1)(N)), processes the mappings 702, and generates the resulting schema mapping M1N at the output in a single pass.
All algorithms and variations considered infra can be applied to multiple mappings in this fashion. Specifically, the algorithm presented in FIG. 6 can be extended to the algorithm of FIG. 7, and as shown below, can produce a correct composition and terminate even when the stepwise procedure of FIG. 6 fails.
Algorithm compose (Σ12, Σ23, . . . , Σ(n−1)n):















Set Σ := Σ12 ∪ Σ23 ∪ ... ∪ Σ(n−1)n



Repeat



 Set Σ′ := Ø



 For every pair of clauses φ, ψ in Σ



  If there exists a σk-resolvent χi of φ, ψ where 2≦k<n



   and there is no variant of χi in Σ



  then set Σ′ := Σ′ ∪ {χi}



  Set Σ := Σ ∪ Σ′



Until Σ′ = Ø



Return Σ13 := constraints in Σ that refer only to symbols of S1, Sn










Analysis of Composition and Non-Functional Mappings
The term “mapping” has become established in the database literature to refer to a binary relation on instances, such as database states or XML documents. A general framework for managing mappings, called model management, studies general operators on mappings and on sets of instances, called models. Among these operators, there are such basic operators as domain, range, composition, inverse, etc.
If a mapping is a function, it is said to be functional. Non-functional mappings appear in many contexts, in particular in data integration and data exchange. There are many natural sources of non-functional mappings. For example, the inverse of a functional mapping which is not injective is a nonfunctional mapping.
Significant interest in the art is found in the development of mappings and models given by constraints, and in particular, mappings given by embedded dependencies and by full dependencies. Such mappings are called CQ=-mappings and CQ0=-mappings, respectively, because they are given by inclusions of conjunctive queries with equality (CQ=) and inclusions of conjunctive queries with equality, but without existential quantification (CQ0=). Similarly, models given by embedded dependencies and by full dependencies are called CQ=-models and CQ0=-models, respectively.
Several fundamental questions are explored for basic operators in the relational setting. Let  be a language for models and mappings. Given an operator  and -models and -mappings for input: (1) Is the output always an -model or an -mapping? (That is,  is closed under ); (2) If not, is there a decision procedure to determine when the output is an -model or an -mapping?; and (3) In case the output is an -model or an -mapping, how hard is it to find an expression for the output?
The present description addresses at least the case when  is CQ0=, CQ=, or SOCQ=. For many operators (e.g., identity, intersection, and Cartesian product) it can be seen that the answer to (1) is ‘yes’ and the answer to (3) is ‘very easy’ (see Proposition 3 infra). For some other operators (e.g., range, domain, and composition) it can be shown that the answers to (1) and (2) are ‘no’. Furthermore, large subclasses of CQ0=, CQ=, and SOCQ= are introduced for which the answer to (1) is ‘yes’ and the answer to (3) is ‘easy.’
It can be seen that domain, range, and composition are closely related and can be reduced to each other (see Proposition 4 infra). Therefore, it suffices to study composition and inverse. The latter is easy if symmetric restrictions are placed on the languages that define the mappings. On the other hand, composition turns out to be very hard.
Composition of mappings has been studied in the art. In one study, the class of source-to-target second-order tuple-generating dependencies (ST SO tgds) is introduced and shown that the class of mappings given by ST SO tgds is closed under composition. Moreover, several examples are found which illustrate cases where smaller classes of mappings are not closed under composition. In particular, it can be shown that CQ=-mappings are not closed under composition, even when further restricted to source-to-target dependencies.
The subject invention extends work in the prior art in several directions. Herein, mappings given by SO tgds are called SOCQ=-mappings. Notice that Skolemizing CQ=-mappings gives SOCQ=-mappings. Thus, composition of three major classes of mappings is addressed, each properly containing the previous ones:

    
    
        1. CQ0=-mappings (full dependencies)
        2. CQ=-mappings (embedded dependencies)
        3. SOCQ=-mappings (SO tgds)
    
    


One case of interest is the case of embedded dependencies (CQ=-mappings). One way to compute composition of such schema mappings, as referenced in FIG. 3 supra, is to (1) Skolemize the CQ=-mappings to get SOCQ=-mappings, (2) find a finite axiomatization of all constraints over the input and output signatures that can be deduced from the constraints that give the mappings, and finally, (3) de-Skolemize the finite axiomatization to get a CQ=-mapping. Difficulties arise from steps 2 and 3.
The subject invention extends the restrictions of languages considered to obtain closure under inverse, which fails in the case of source-to-target constraints, because the inverse of a source-to-target constraint is a target-to-source constraint.
Subclasses of CQ0=, CQ= and SOCQ= are provided which are closed under composition and inverse, and which ideally, include constraints that arise from CQ0= and CQ= queries, which are known to be closed under composition.
It is desired to have widely applicable, polynomial-time-checkable, sufficient conditions for the composition of two CQ0=-mappings (CQ=, SOCQ=) to be a CQ0=-mapping (CQ=, SOCQ=). Moreover, it is preferred to know whether there are computable necessary and sufficient conditions or whether the problem is undecidable.
Summarizing some aspects provided herein, it is shown that CQ0=-mappings are not closed under composition. The problem of determining whether the composition of two CQ0= mappings is a CQ0=-mapping is shown to be undecidable. These results carry over to the case of CQ=-mappings and SOCQ=-mappings. Additionally, several equivalent (non-effective) conditions for composition are provided.
Polynomial-time-checkable sufficient conditions for composition are introduced, which include the case of constraints given by queries. Moreover, subsets of CQ0=, CQ=, and SOCQ= are identified which are closed under composition and inverse, and which include the case of constraints given by queries. Finally, a polynomial-time algorithm is presented for computing the composition of CQ0=, CQ=, and SOCQ=-mappings which satisfy the conditions above.
Preliminary Information
A signature σ={R1, R2, . . . , RN} is a set of relation symbols. A relational atom is a formula of the kind R(t1, . . . , tm), where ti is a variable or constant. An equality atom is a formula of the kind t1=t2, where ti is a term, such as a variable or a constant. CQ is defined as the set of conjunctive queries, i.e., formulas of the kind ∃x1, . . . ∃xm (φ(x1, . . . , xm, y1, . . . , yn)), where φ is a conjunction of relational or equality atoms and each of the free variables y1, . . . , yn occurs in some relational atom. CQ0 is the set of queries with conjunction, but no existential quantifiers (i.e., when m=0; also called select-join queries). Given a query class , = is the corresponding query class that also includes equality.
Skolem(Q) is defined to be the formula obtained from Q by replacing existential quantifiers with Skolem functions; it is an existential second-order formula that asserts the existence of the Skolem functions and which does not have first-order existential quantifiers. For example, if

Q=∃y(Exy, Eyz)→Exz

then

Skolem(Q)=∃ƒ(E(x, ƒ(xz)), E(ƒ(xz), z)→Exz).

Set Sk:={Skolem(Q): Q ∈ }. Given a set of constraints ψ over the signature σ1∪σ2, ψ|σ1 is the set of constraints in ψ which only contain relation symbols in σ1. A constraint which contains a relation symbol from σ1 in the premise or in the conclusion is called a σ1-constraint.
Models and mappings. A model is a set of instances. A model can be expressed in a concrete language, such as SQL DDL, XML Schema, etc. For example, a relational schema denotes a set of database states; an XML schema denotes a set of XML documents; a workflow definition denotes a set of workflow instances; a programming interface denotes a set of implementations that conform to the interface. A mapping is a relation on instances. Unless stated otherwise, it is assumed that all mappings are binary, i.e., they hold between two models. A mapping can be expressed in a concrete language, such as SQL DML, XSLT, etc.
Constraints for specifying mappings. A constraint is a Boolean query. Sets of constraints are denoted with capital Greek letters, and individual constraints with lowercase Greek letters. The constraints to be considered are in

IC():={∀ x (Q1( x)→Q2( y)):Q1, Q2 ∈ }

    
    
        where { x} is the set of free variables in Q1, { y} ⊂ { x}, and  ∈ {CQ0, CQ0=, CQ, CQ=}. These are called query inclusion constraints over . These kinds of constraints express the containment of Q1 in Q2 and are known as embedded dependencies in the case where  is CQ= and as full dependencies in the case where  is CQ0=. Also considered are constraints in
    
    


IC(SOCQ=):=∃ ƒ{∀ x (Q1( x)→Q2( y))}

    
    
        where { x} is the set of free variables in Q1, { y} ⊂ { x}, and Q1, Q2 are like CQ0= queries, except they may also have terms constructed from the function symbols ƒ. IC(SOCQ) is defined similarly, with Q1, Q2 are like CQ0 queries.
    
    


Given a query language , associate to every expression of the form

(σ1, σ2, Σ12)

where Σ12 is a finite subset of IC() over the signature σ1∪σ2 the mapping

{<A, B>: A ∈ mod(σ1), B ∈ mod(σ2), (A, B) Σ12}.

σ1 is the input (or source) signature, and σ2 is the output (or target) signature. Without loss of generality, it is assumed that σ1, σ2 are disjoint or identical.

It is said that m is given by expression E if the mapping that corresponds to E is m. Furthermore, m is an -mapping if m is given by an expression (σ1, σ2, Σ12) with Σ12 a finite subset of IC().
Composition. Given two mappings m12 and m23, the composition m12·m23 is the unique mapping

{<A,C>: ∃B(<A, B>∈m12 ^<B,C>∈m23)}.

Deductions and Chase
Following are additional preliminaries provided to explain the algorithm and the correctness proofs in the following sections. The following fixes a specific deductive system, defines the standard notions of ├DC (•), and chase (•), and gives Propositions 1 and 2.
Constraints in IC(SOCQ=) are written as rules of the form

Q1( x)→Q2( x)

leaving the second-order quantifiers over Skolem functions and the outermost first-order universal quantifiers ∀ x implicit. Call Q1( x) the premise and Q2( x) the conclusion. If the premise is empty, only the conclusion is written. Call rules of the form Q2( c), where c is a tuple of constants, facts.

Definition 1. A deduction from rules Σ is a sequence of rules, each obtained in one of three ways:

    
    
        1. by copying from Σ,
        2. by expanding and/or renaming a rule appearing earlier in the sequence, or
        3. by applying resolution on two rules appearing earlier in the sequence.
        Such rules are called axiom rules, expand/rename rules, and resolution rules respectively.
    
    


A deductive procedure is the one that derives new rules using deductions. A deduction has length n if it consists of n lines. A rule r obtained by expand/rename from rule r′ may have additional atoms in the premise, may have variables replaced consistently by arbitrary terms, and may have replacements in the conclusion consistent with equations in the premise. For example,

R(xy), y=ƒ(xy)→S(xy)

is a valid result of applying expand/rename to R(uv)→S(u ƒ(uv)).

Two formulas can be unified when there exists a variable substitution that renders both formulas syntactically identical. Resolution is a complete logical inference procedure that derives a new rule from two given rules, when an atom of the premise of one rule can be unified with an atom in the conclusion of another rule. For example,

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

is the result of applying resolution to rules

R(xy)→S(xy)

S(xy), S(yz)→S(xz).

The example illustrates a special case of resolution known as modus ponens. A rule r obtained by applying modus ponens to rules r′, r′′ consists of the conclusion in r′′ and the premise atoms in r′, together with those in r′ which do not appear in the conclusion of r′.

Deductions are annotated by numbering the rules in ascending order and by adding justifications to each line indicating how that line was obtained. It is enough to justify a resolution rule with just two numbers and an expand/rename rule with a single number and a variable assignment. Axiom rules can be indicated through a lack of any other annotation. A variable assignment is a list of items of the form x:=y where x is a variable and y is a term.
EXAMPLE 1
Given

Δ={R(1, 1)} and

Σ={R(xy)→S(xy), S(zz)→T(zz)},

the following is a valid deduction from Σ∪Δ:


















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]










Here, rules 1, 2, and 5 are axioms, 3 and 6 are expand/rename, and 4 and 7 are resolution.

Within a deduction, a resolution step is called a σ2-resolution if the resolution is performed by unifying an atom from the signature σ2. The rule ξ obtained by σ2- resolution is called σ2-resolvent. A rule ξ is a variant of ξ′ if it can be deduced from ξ′ without using resolution.
Following is an introduction of prerequisites for proving the correctness of the composition algorithm and the undecidability results.
If there is a deduction from a set of constraints Σ where the last line contains a constraint ξ, it can be said that ξ is deduced from Σ, which is written Σ├ξ. The -deductive closure of Σ is

DC(, Σ):={ξ∈:Σ├ξ}.

Write DC(Σ) when  is clear from context. Write DΣ if all constraints in Σ are true in D. Write ΣΣ′ if for all instances D, DΣ implies DΣ′. It can be checked that if ΣΣ′, then also ΣΣ′; i.e., the deductive system is sound. A deductive system is called complete if it guarantees that if a set of sentences is unsatisfiable, then it will derive a contradiction. A deduction witnesses that the derived rules are implied by the axiom rules.
Proposition 1. If Δ is a set of facts, then the following are equivalent:

    
    
        1. Σ∪Δ├φ.
        2. There is ξ such that Σ├ξ and Δ, ξ├φ.
    
    


Proof. If (2) holds then there exist deductions γ and γ′ witnessing Σ├ξ and Δ, ξ├φ. Then γ that witnesses Σ∪Δ├φis obtained by appending γ′ to γ. Now assume that (1) holds and γ witnesses Σ∪Δ├φ. Set γ to γ except for the following replacements, which are made rule by rule from the first rule in γ to the last:

    
    
        1. If rule r is an axiom rule from Δ, then remove it.
        2. If rule r is an axiom rule not from Δ, then keep it as it is.
        3. If rule r is obtained by expand/rename from rule i, then replace every constant c in r and in the variable assignment for r with the corresponding variable vc.
        4. If rule r is obtained by resolution from rules i and j, and rule i is an axiom rule from Δ, then replace r with a trivial expand/rename from rule j.
        5. If rule r is obtained by resolution from rules i and j, and rule i is not an axiom rule from r, then replace r with the result of applying resolution to the new rules i and j.
    
    


EXAMPLE 2
Given the deduction γ from Example 1, γ is:
















1. <blank line>




2. R(xy) → S(xy)



3. R(v1v1) → S(v1v1)
[2] x := v1 y := v1



4. R(v1v1) → S(v1v1)
[3]



5. S(zz) → T(zz)



6. S(v1v1) → T(v1v1)
[5] z := v1



7. R(v1v1) → T(v1v1)
[4, 6]










The following replacements have been made for each rule:

    
    
        1. Axiom from Δ: removed by 1.
        2. Axiom from Σ; unchanged by 2.
        3. Expand rename: 1 replaced with v1 by 3.
        4. Resolution on 1, 3: trivial expand/rename by 4.
        5. Axiom from Σ; unchanged by 2.
        6. Expand rename: 1 replaced with v1 by 3.
        7. Resolution on 4, 6: resolution by 5.
    
    


γ is a valid deduction witnessing Σ├ξ since axioms from Δ are no longer used, and since replacements 1 through 5 above ensure that rule R is correctly deduced from the previously replaced rules. Additionally, Δ, ξ├R( c) is witnessed by a deduction γ′ which consists of the following sequence,

    
    
        the axioms from Δ which were removed from γ to obtain γ′,
        ξ followed by ξ′ obtained from ξ by renaming each variables vc to the corresponding constant c, and
        a sequence of resolution steps using each axiom from Δ and starting with ξ′.
    
    


Definition 2. Given an instance D, the result of chasing D with constraints Σ⊂IC(SOCQ=) and the set of Skolem functions F is abbreviated by chase (D, Σ, F) and is denoted by the database D′′ obtained from

D′:={Ri( c): Σ∪Δ∪Φ├Ri( c)}

where

    
    
         c is a tuple of constants,
        Δ is the set of facts given by D:

Δ:={Ri( c):DRi( c)}

        and Φ is the set of facts given by F:

Φ:={ƒ( c)=a:ƒ∈F,ƒ( c)=a}

as follows. Define c0≡c1 iff Σ∪Δ∪Φ├c0=c1.

    
    


Now to obtain D′′ from D′, pick one constant c0 from every equivalence class and replace every constant in that equivalence class with c0. That is, D′′:=D′/≡. All functions in F are required to have the same domain. If they are finite, then chase (D, Σ, F) is finite. This definition is a variation on the usual definition, where the functions F are constructed during the chase process.
Proposition 2. Chase (D, Σ, F)Σ.

    
    
        Proof. Set D′′:=chase (D, Σ, F)Σ and assume D′′ξ for some ξ∈Σ. This implies that there must be some assignment of constants c to the variables x in the premises so that the premise in ξ holds and the conclusion fails. Assume that the conclusion consists of a single relational atom R( y) or a single equation y1=y2 where y is a sequence of terms over x. Set y′ to the sequence of terms obtained from y by replacing every variable in x with the corresponding constant c. If the former holds then Δ∪Φ, ξ├R( y′) holds and R( y′) is not in D′. Since ξ∈Σ, Proposition 1 implies that Σ∪Δ∪Φ├R( y′) holds, contradicting the definition of D′. If the latter holds then Δ∪Φ, ξ├y′1=y′2 and y′1=y′2 holds. Since ξ∈Σ, Proposition 1 implies that Σ∪Δ∪Φ├y′1=y′2 holds, contradicting the definition of ≡ and D′′.
    
    


Composition of CQ0= -Mappings
The following description of composition begins by studying composition of CQ0-mappings and CQ0=-mappings. Later, the techniques introduced to handle these cases are extended to handle SOCQ= and CQ=-mappings. Necessary and sufficient, non-computable conditions for the composition of two CQ0=-mappings to be a CQ0=-mapping are given (see Theorem 1 below). Then, CQ0 and CQ0= are shown not to be closed under composition (see Example 3 below) and, furthermore, that determining whether the composition of two CQ0=-mappings is a CQ0=-mapping is undecidable (see Theorem 2 infra). An algorithm for composition (CQ0= COMPOSE) is given, which works correctly on CQ0=-mappings satisfying the conditions of Theorem 3 infra, which can be checked in polynomial time. Also, a subset of CQ0= recognizable in polynomial time, called good-CQ0=, is defined, which is closed under composition (see Theorem 4 infra).
The composition of two CQ0=-mappings given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) can be computed using the following algorithm:
Algorithm CQ0= COMPOSE (Σ12, Σ23)















Set Σ:= Σ12 ∪ Σ23



Repeat



 Set Σ := ø



 For every pair ø, ψ ∈ Σ



  If there exists a σ2-resolvent ξ of ø, ψ



   and there is no variant of ξ in Σ



   then set Σ′ := Σ ∪ {ξ}



 Set Σ := Σ ∪ Σ′



Until Σ′ = ø



Return Σ13 := Σ|σ13










The next step is to verify the correctness of the algorithm and study the conditions under which the algorithm terminates. Notice that CQ0 and CQ0= are not closed under composition, as the following example shows.
EXAMPLE 3
Consider the CQ0-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where Σ12 is

R(xy)→S(xy)

S(xy), S(yz)→S(xz)

and Σ23 is

S(xy)→T(xy)

and where σ1, ={R}, σ2, ={S}, and σ3, ={T}. Together, these constraints say that R⊂S⊂T and that S is closed under transitive closure. This implies tc(R)⊂T, where tc(R) denotes the transitive closure of R. It can be seen that the only CQ0=-constraints that hold between R and T are constraints of the form

R(xv1), R(v1, v2), . . . ,R(vi−1, vi), R(vi, y)→T(xy)

but no finite set of them expresses tc(R)⊂T.

In fact, the composition m12·m23 is not even expressible in FO (first-order logic). Otherwise, given an FO sentence φ such that

<R, T>∈m12·m23 iff (R,T)φ

an FO formula ψ(xy) can be created, which is obtained by replacing every occurrence of T(uv) in φ with x≠u V y≠v. Then given a domain D with R⊂D2, Rψ[ab]

iff (R, D2−<a,b>)φ

iff tc(R)⊂D2−<a,b>

iff <a,b>∈tc(R)

and therefore, ∀(x,y)ψ(x,y) says that R is a connected graph, which cannot be expressed in FO.

When is the composition of two CQ0=-mappings a CQ0=-mapping? Theorem 1 herein gives necessary and sufficient conditions. An obstacle for the composition to be a CQ0=-mapping can be recursion, yet recursion is not always a problem. In Theorem 3, sufficient conditions are provided that can be checked efficiently, and in Theorem 4, it is shown that good-CQ0=, a subset of CQ0= defined below, is closed under composition. All these results also hold for CQ0.
Theorem 1. If the CQ0=-mappings m1, m2 are given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) with Σ123:=Σ12∪Σ23 and σ13=σ1∪σ3, then the following are equivalent:

    
    
        (1) There is a finite set of constraints Σ13⊂IC(CQ0=) over a signature σ13 such that m:=m1·m2 is given by (σ1, σ3, Σ13).
        (2) There is a finite set of constraints Σ13⊂IC(CQ0=) over the signature σ13 such that

DC(CQ0=, Σ123)|σ13=DC(CQ0=, Σ13)

        (3) There is m such that for every ξ over the signature σ13 satisfying Σ123ξ there is a deduction of ξ from Σ123 using at most m σ2-resolutions.
    
    


Proof. The proof uses Lemmas 1 and 2 below. The proof first shows the equivalence of (1) and (2), and then shows the equivalence of (2) and (3).

    
    
        Assume (2) holds. Then <A, C>∈m1·m2
    
    


















iff ∃B (A, B, C)   Σ123
(by definition of ·)



iff (A, C)   DC(CQ0=, Σ123) |σ13
(by Lemma 1)



iff (A, C)   DC(CQ0=, Σ13)
(since (1) holds)



iff (A, C)   Σ13.
(by soundness of DC)










This shows that (1) holds.

    
    
        Conversely, assume (1) holds. Then (A, C)DC(CQ0=, Σ123)|σ13
    
    


















iff ∃B (A, B, C)   Σ123
(by Lemma 1))



iff <A, B> ∈ m1 · m2
(by definition of ·)



iff (A, C)   Σ13
(since (2) holds)



iff (A, C)  DC(CQ0=, Σ13).
(by soundness of DC)










    
    
        This shows that (2) holds.
    
    


Now assume (3) holds. Set Σ to the set of all constraints in DC(CQ0=, Σ123)|σ13 which can be deduced using at most m σ2-resolutions and no other resolutions. Every constraint in Σ can be obtained by expand/rename from a finite subset Σ13⊂Σ. It can be shown that (2) holds.
Assume that there is a deduction γ witnessing Σ123├ξ. Since (3) holds, it can be assumed that γ has m′ σ2-resolutions. By Lemma 2, there is a deduction γ witnessing Σ123├ξ also with m′ σ2-resolutions, and with all of them occurring before any other resolutions. Since the last line of γ does not contain any symbols from σ2, it can be assumed that γ does not contain any lines containing symbols from σ2 after the last σ2-resolution.
Break γ into two parts: γ1 the initial segment of γ up to and including the last σ2-resolution; and γ2 the remainder of γ. By definition of Σ, every constraint ψ in γ1 must be in Σ, and therefore Σ13├ψ holds. Every constraint ψ in γ2 does not contain any symbols from σ2, and Σ123|σ13 ⊂Σ13, which imply that Σ13├ψ. Therefore, Σ13├ξ as desired.
Conversely, assume (2) holds. Take m to be the total number of σ2-resolutions needed to deduce every ψ∈Σ13 from Σ123. Assume Σ123├ξ. Then there is a deduction γ witnessing Σ13├ξ. Clearly, γ has no σ2-resolutions. From γ, one can obtain γ witnessing Σ123├ξ by appending to γ a deduction of every constraint in Σ13 and by replacing every line where an axiom from Σ13 is used by a vacuous expand/rename of the line where the deduction of that axiom ends. Clearly, γ has exactly m σ2-resolutions as desired. This shows that (3) holds.
Lemma 1. Under the hypotheses of Theorem 1, the following are equivalent:

    
    
        1. (A, C)DC(CQ0=, Σ123)|σ13.
        2. ∃B (A, B, C)Σ123.
    
    


Proof. Assume (A, B, C)Σ123 for some B. Then (A, B, C)DC(CQ0=, Σ123) (by soundness) and therefore (A, C)DC(CQ0=, Σ123)|σ13 since B is not mentioned in DC(CQ0=, Σ123)|σ13.
Conversely, assume (A, C)DC(CQ0=, Σ123) |σ13. Set

(A′, B′, C):=chase((A, Ø, C),Σ123).

If the chase terminates and A=A′ and C=C′, then (A, B, C)Σ123 by Proposition 2, which implies (A, B)Σ12 and (B, C)Σ23, as desired.

It is clear that the chase terminates, since no new constants are introduced. Now assume, to get a contradiction, that A≠A′ and C≠C′. Set ΔAC to the set of facts given by A and C. Then,

Σ123∪ΔAC├R( c)

where R is a relation in A or C not containing c or

Σ123∪ΔAC├c0=c1 

where c0, c1 are distinct constants in A or C.

Consider the former case; the latter is similar. If Σ123∪ΔAC├R( c) then by Proposition 1 there exists ξ such that Σ123├ξ and ΔAC, ξ├R( c). Since (A, C)ΔAC, it follows that (A, C)ξ and ξ∈DC(CQ0=, Σ123)|σ13, contradicting the initial assumption.
Lemma 2. Under the hypotheses of Theorem 1, if there is a deduction γ witnessing Σ123├ξ with at most m σ2-resolutions, then there is γ witnessing Σ123├ξ with at most m σ2-resolutions and where furthermore, all σ2-resolutions occur before all other resolutions.
Proof. Assume k<m and γk,l witness Σ123├ξ with

    
    
        1. exactly m σ2-resolutions,
        2. where the first k resolutions are σ2-resolutions, and
        3. where there are exactly l non-σ2-resolutions before the k+1-th σ2-resolution or the end of the deduction.
    
    


The proof proceeds by induction on k and l. Given γk,l with l>0, the proof shows how to obtain γk,l−1. To prove the case where l=0, simply set γk+1 ,l′:=γk,0 where l′ fulfills the conditions above. Once γm,l′ is obtained for some l′, set γ:=γm,l′ and the lemma is proved.
Consider the line s containing δ, the (k+1)th σ2-resolution in γk,l of, for example, lines i and j containing, respectively, α and β. Consider also the line r containing λ, the l-th non-σ2-resolution in γk,l of, for example, lines r1 and r2 containing, respectively, λ1 and λ2.
Now consider several cases. If i, j<r<s, then obtain γk,l−1 by moving line s to just before r. If lines i, j are not derived from line r, then obtain γk,l−1 by first rearranging γk,l to γk,l so that i, j<r<s, then proceeding as above.
Otherwise, either α or β have been obtained through expand/rename from line r. To simplify the presentation, assume that both have been obtained through a single expand/rename from line r (the other cases are similar). There now exists r<i, j<s. By rearranging γk,l if needed, assume i=r+1, j=r+2 and s=r+3. Since α and β can be obtained from r by expand/rename, α1, α2 and β1, β2 can be obtained, respectively, from r1, r2 by expand/rename so that α is the resolution of α1, α2 and β is the resolution of β1, β2. Replace the four contiguous lines r, i, j, s with the following seven lines.

















r
α1
[r1]



r + 1
α2
[r2]



r + 2
β1
[r1]



r + 3
β2
[r2]



r + 4
δ1
[r + 1, r + 2]



r + 5
δ2
[r + 4]



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










An important point is that line r+4 now contains a σ2-resolution, since α2 and β1 must resolve through a relation symbol of σ2, because α and β do. Notice that δ is on line r+6, since the result of resolution on α1, α2, β1 and β2 is the same as the result of resolution on α and β (this is because resolution is “associative”).
Corollary 1. Under the hypotheses of Theorem 1, whenever CQ0= COMPOSE (Σ12, Σ23) terminates, it yields Σ13 such that m12·m23 is given by (σ1, σ3, Σ13).
Notice that after the m-th iteration of the main loop, Σ will contain a variant of every constraint that can be deduced using at most m σ2-resolution steps. The constraints of Example 3 fail to satisfy (3) of Theorem 1, and therefore, CQ0= COMPOSE (Σ12, Σ23) will not terminate when Σ12 and Σ23 are as in Example 3 for input. In contrast, CQ0= COMPOSE (Σ12, Σ23) will terminate on Σ12, Σ23 from the example below, which does satisfy (3) of Theorem 1, so recursion is not always bad.
EXAMPLE 4
Consider the CQ0-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where Σ12 is

R(xy)→S(xy)

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

and Σ23 is

S(xy)→T(xy),

and where σ1={R}, σ2={S}, and σ3={T}. Together, these constraints say that R⊂S⊂T, that R and S are closed under transitive closure (because the constraints

S(xy), S(yz)→S(xz)

R(xy), R(yz)→R(xz)

can be deduced from the constraints above), and that R(xz) holds whenever S(xy), S(yz) holds. The constraints

R(xy), R(yz)→R(xz)

R(xy)→T(xy)

express exactly the composition m1·m2, and are exactly those found by CQ0= COMPOSE (Σ12, Σ23).

Theorem 2. Checking whether the composition of two CQ0-mappings is a CQ0-mapping is undecidable (in fact, coRE-hard). The same holds with CQ0= instead of CQ0.
Proof. The proof reduces Post's correspondence problem (PCP)—known to be undecidable—to the problem of deciding whether m12·m23 is a CQ0-mapping where m12 and m23 are CQ0 mappings. Given a PCP problem, define m23 so that there is a solution to the PCP problem iff m12·m23 is not a CQ0-mapping (m12 does not depend on the PCP problem).

    
    
        The CQ0-mappings m12·m23 are given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where
        σ1={A, B, O, Z},
        σ2={Â, {circumflex over (B)}, Ô, {circumflex over (Z)}}, and
        σ3={T}
        with A, B unary and all other relations binary and with Σ12 and Σ23 as described below.
    
    


Write x0011y for the set of atoms

A(x), Z(xa), Z(ab), O(bc), O(cy), B(y)

over σ1, which corresponds to a path from A to B through Z, O (stands for “zero” and O stands for “one”). Similarly, write x′x0011y′y for the set of atoms

Â(xx′), {circumflex over (Z)}(xa), {circumflex over (Z)}(ab), Ô(bc), {circumflex over (Z)}(cy), {circumflex over (Z)}(x′a′), {circumflex over (Z)}(a′b′), Ô(b′c′), Ô(c′y′), {circumflex over (B)}(yy′)

over σ2. Σ12 contains the constraint

A(x), Z(xy), A (x′), Z(x′y′)→Â(xx′), {circumflex over (Z)}(xy), {circumflex over (Z)}(x′y′)

and all corresponding constraints for all combinations AO, ZZ, ZO, OZ, OO, ZB, OB. These constraints imply that xSy, x′Sy′→x′xSy′y can be deduced for any string S.

Encode each PCP “domino” by a constraint in Σ23 as follows. For example, encode the domino 0011/011 as the constraint

Â(xx′), {circumflex over (Z)}(xa), {circumflex over (Z)}(ab), Ô(bc), Ô(cy), {circumflex over (Z)}(x′a′), Ô(a′b′), Ô(b′y′)→Â(xx′), Â(yy′)

Finally, add to Σ23 the constraint

Â(xx′), Â(yy′), {circumflex over (B)}(yy′)→{circumflex over (T)}(xy).

Now assume that the PCP problem has a solution for the string S over {0, 1}*. Then deduce infinitely many constraints of the form

xSk y, x′Sky′→T(xy)

where Sk is the string S repeated k times as follows. Notice that these constraints are over σ1∪σ3 and that none of them can be obtained from any other.

For k=1 (the other cases are similar), first obtain

xSy, x′SyS→x′xSy′y 

by using the constraints in Σ12, and then obtain

xSy, x′SyS→A(xx′), A(yy′), B(yy′)

by resolution, in order, using the rules in Σ23 which correspond to the sequence of blocks necessary to obtain S. Finally, obtain

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

using the last constraint in Σ23.

Conversely, if the PCP problem has no solutions, no deduction with premise in σ1∪σ3 and conclusion

Â(xx′), Â(yy′), {circumflex over (B)}(yy′)

is possible. Since this is the only premise matching a conclusion in σ1∪σ3, no constraints in σ1∪σ3 are deduced. In this case Σ13=Ø gives the composition m12·m23.

The coRE-hardness from Theorem 2 implies that algorithm CQ0= COMPOSE may not terminate even when the composition is a CQ0=-mapping. This happens, for example, in the following case.
EXAMPLE 5
Consider the CQ0-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where Σ12 is

R(xy)→S(xy)

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

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

and Σ23 is

S(xy)→T(xy)

and where σ1, ={R, R′}, σ2={S, S′}, and σ3={T}. The constraints

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

R(xy)→T(xy)

express exactly the composition m1·m2, but algorithm CQ0= COMPOSE will never terminate, since it will deduce the infinitely many constraints it would deduce in Example 3.

The following conditions are sufficient for algorithm CQ0= COMPOSE to terminate. These conditions can be checked in polynomial time, as follows. Run kσ2−1 iterations of CQ0= COMPOSE (Σ12, Σ23) where kσ2 is the number of relation symbols in σ2, and check whether a constraint of the form given below appears in Σ.
Theorem 3. Under the hypotheses of Theorem 1, if no constraint of the form φ( z), S( y)→S( x) where

    
    
        1. φ( z) is a conjunction of atoms over σ123,
        2. there is no atom S( w) in φ( z) with { x}⊂{ w},
        3. { x}{ y}, and
        4. S is a relation symbol in σ2 can be deduced from Σ123 using only σ2-unifications (this is called a bad constraint), then CQ0= COMPOSE (Σ12, Σ23) terminates, and therefore, m1·m2 is a CQ0=-mapping. The same holds for CQ0-mappings.
    
    


Proof. Assume the hypotheses hold. Consider any deduction γ witnessing Σ123 ├ξ which uses only σ2-unifications where ξ contains a σ2 atom in the conclusion. Assume without loss of generality that all rename operations are performed first, followed by all resolution operations. Assume also that every rule in γ contains a single atom in its conclusion and that every rule is used in at most one resolution step.
Such a deduction can be represented as a tree T where every node is one atom. Every non-leaf node in T is the conclusion of some rule r. The children of r are the atoms in the premise of rule r. The premise of ξ consists of all the leaves of T and its conclusion is the root of T.
It is easy to check that any subtree T′ of T which contains, for every node, either all its children in T or none of them, can be converted into a deduction γ witnessing Σ123├ξ′ where the premise of ξ′ consists of all the leaves of T′ and its conclusion is the root of T′.
Since the hypothesis holds, no such subtree may contain S( x) as its root and S( y) as a leaf where S is a relation symbol in σ2 and x y. Therefore, any path from the leaves to the root in T containing a node S( y) may only contain at most 2r r!8 other nodes with S atoms where r is the arity of S. This means that any such path must have length bounded by kσ22rσ2rσ2! where kσ2 is the number of relation symbols in σ2 and rσ2 is the maximum arity of a relation symbols in σ2. As a result, up to variants, there is only a finite number of conclusions of Σ123 obtainable through σ2-unifications and this implies that CQ0= C0MPOSE (Σ12, Σ23) terminates.
Definition 3. A CQ0=-mapping is a good-CQ0=-mapping if it is given by (σ1, σ2, Σ12) such that no constraint of the form φ( z), S( y)→S( x) where

    
    
        1. φ( z) is a conjunction of atoms over or σ1∪σ2 
        2. there is no atom S( w) in φ( z) with {( x}⊂{ w},
        3. { x}{ y}, and
        4. S and S′ are both relation symbol in σ1 or both in σ2 can be deduced from Σ123 using only σ1-unifications or only σ2-unifications. Define good-CQ0 similarly.
    
    


Theorem 4. Good-CQ0= and good-CQ0 are closed under composition and inverse.
Comment 1. CQ0=-queries are included in good-CQ0=-mappings. Notice that total and surjective CQ0=-mappings are not closed under composition.
EXAMPLE 6
Consider the CQ0-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where Σ12 is

R(xy)→S(xy)

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

and Σ23 is

S(xy)→T(xy)

and where σ1={R}, σ2={S}, and σ3={T}. Here m12 and m23 are total and surjective and their composition says that tc(R) ⊂T, which can be seen in Example 5, is not expressible even in FO.

Composition of SOCQ=-Mappings
The focus of this section is the composition of SOCQ=-mappings. In order to handle existential quantifiers in CQ=-mappings, first convert CQ=-mappings constraints into Skolem form, which yields SOCQ=-mappings. Theorem 5 below shows that SOCQ=-mappings are closed under composition, because it can assert the existence of the relations in the intermediate signature or σ2 using existentially-quantified function symbols.
The following related question is also very important:

    
    
        If the SOCQ=-mappings m12, m23 are given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23), is there a SOCQ=-mapping m13 given by (σ1, σ3, Σ13) satisfying m13=m12·m23 such that Σ13⊂SOCQ= has no function symbols or constants other than those appearing in Σ12∪Σ23? If so, it is said that m12 and m23 have a conservative composition.
    
    


Conservative composition is important because ultimately there is a need to eliminate all function symbols to obtain CQ=-mappings, and it is not known how to eliminate function symbols introduced in equations such as those used in the proof of Theorem 5 below. Theorems 1 and 2 from the previous section show that SOCQ and SOCQ= are not closed under conservative composition, and that determining whether the conservative composition of two SOCQ=-mappings is a SOCQ=-mapping is undecidable. As in the case of CQ0=-mappings, necessary and sufficient non-computable conditions are given for two SOCQ=-mappings to have a conservative composition (see Theorem 6 below), and sufficient conditions for conservative composition are given that can be checked efficiently. An algorithm for conservative composition (SOCQ= COMPOSE) is given which works correctly on SOCQ=-mappings, satisfying these conditions. Additionally, good-SOCQ= is defined as a polynomial-time subset of SOCQ=, which is closed under conservative composition. In contrast with the previous section, it turns out that in this case, equations are essential and therefore, these results do not hold for SOCQ.
Before proceeding to the results, the semantics of IC(SOCQ=) constraints are briefly described. A question is, what is the universe from which the functions can take values, i.e., what is their allowed range? Intuitively, the problem is with the universe of the existentially quantified intermediate database. All databases are required to be finite (i.e., all relations are finite), but to have an implicit countably infinite universe. The functions are allowed to take any values from this implicit universe, as long as their range is finite. These assumptions ensure that the deductive system introduced in Section 2 is sound for IC(SOCQ=), which is needed for Theorem 6 below.
Theorem 5. SOCQ=-mappings are closed under composition. Proof. If SOCQ=-mappings m12 and m23 are given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23), Σ13 is obtained such that the composition m12·m23 is given by (σ1, σ2, Σ23) as follows. Set Σ13:=Σ′12∪Σ′23 where Σ′12 and Σ′23 are obtained from Σ12 and Σ23 by replacing every occurrence of an atom R( x) where R∈σ2 with fin( x), gR( x)=hR( x), where fin( x):=_Λx∈{ x}x=ƒ(x), and ƒ, gR, hR are new function symbols.
Then if <A,C>∈m12·m23, then there is a B such that (A,B)m12 and (B,C)m23. Set gR( c)=hR( c) iff R( c) holds in B for every relation R in σ2 by using any two values from the domain. Furthermore, set ƒ(c):=c, if c is in the active domain of B and ƒ(c):=c′, otherwise, where c′ is some value from the domain. Then (A,C)Σ13. Conversely, if (A,C)Σ13, then set R:={ c:fin( c), gR( c)=hR( c)} for every relation R in σ2 to obtain B such that (A,B)m12 and (B,C)m23. fin( x) is a finite predicate, since the range of ƒ is finite. Hence, every relation R in B is finite.
Theorem 6. If the SOCQ=-mappings m12, m23 are given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) with Σ123:=Σ12∪Σ23 and σ13=σ1∪σ3, then the following are equivalent;

    
    
        1. There is a finite set of constraints Σ13⊂IC(SOCQ=) over the signature σ3 such that m:=m12·m23 is given by (σ1, σ3, Σ13) where Σ13 has no function symbols or constants other than those appearing in Σ123.
        2. There is a finite set of constraints Σ13⊂IC(SOCQ=) over the signature σ13 such that DC(SOCQ=, Σ123)|σ13=DC(SOCQ=, Σ13) where Σ13 has no function symbols or constants other than those appearing in Σ123.
        3. There is k such that for every ξ over σ13 satisfying Σ123├ξ there is a deduction of ξ from Σ123 using at most k σ2-resolutions.
        Proof: Essentially the same as that of Theorem 3, using Lemma 3 below instead of Lemma 1.
    
    


Lemma 3. Under the hypotheses of Theorem 6, the following are equivalent:

    
    
        1. (A,C)DC(SOCQ=,Σ123)|σ13.
        2. ∃B (A, B, C)Σ123.
        Theorem 6 suggests essentially the same algorithm for composition of SOCQ=-mappings as CQ0= COMPOSE; call it SOCQ= COMPOSE. The only difference between them is that SOCQ= COMPOSE operates on IC(SOCQ=) constraints while CQ0= COMPOSE operates on IC(CQ0=) constraints. Correctness of SOCQ=COMPOSE, sufficient conditions for its termination, and good-SOCQ=-mappings are defined for SOCQ= just like for CQ0=.
    
    


Composition of CQ=-Mappings
This section considers how to convert SOCQ=-mappings back to CQ=-mappings. Consider the case of CQ=-mappings and CQ=-mappings. In order to compute the composition of two CQ=-mappings m12, m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) progress is in three steps, as follows.

    
    
        Procedure CQ= COMPOSE (Σ12, Σ23)
        1. Σ′12:=SKOLEMIZE (Σ12)
        
            Σ′23:=SKOLEMIZE (Σ23)
        
        
        2. Σ′13:=SOCQ= COMPOSE (Σ′12, Σ23)
        3. Return DESKOLEMIZE (Σ′13)
    
    


The first step, SKOLEMIZE, is straightforward. The second step, SOCQ= COMPOSE, has been discussed in the previous section. For the third step, DESKOLEMIZE, an algorithm is given below which is shown to be correct (see Theorem 7). It is shown that even if the second step succeeds, it may be impossible to find Σ13⊂IC(CQ=) such that Σ′13≡Σ13 (see Example 4). Thus, a necessary and sufficient polynomial-time checkable condition is identified for the third step to succeed (see Proposition 2). DESKOLEMIZE may produce a result of size exponential in the size of its input. It is shown that in the general case, this is unavoidable (see Theorem 8), yet polynomial-time checkable conditions are provided for DESKOLEMIZE to run in polynomial time in the size of its input (see Proposition 2).
The following example, from prior art, shows that de-Skolemization is not always possible.
EXAMPLE 7
Consider the CQ=-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where

    
    
        Σ12 is E(x, y)→F(x, y)
        
            E(x, y)→∃uC(x, u)
            E(x, y)→∃vC(y, v)
        
        
        Σ23 is F(x, y), C(x, u), C(y, v)→D(u, v)

and where σ1={E}, σ2={F, C}, and σ3={D}. Here, Steps 1 and 2 of CQ= COMPOSE succeed, but Step 3 fails no matter what algorithm is used for it, since m12·m23 is not a CQ=-mapping, as shown in the art.

    
    


The algorithm DESKOLEMIZE which is presented below depends on ├*, which is some polynomial-time approximation of . That is, if Σ├*φ, then Σφ. The converse may not hold. There are known cases in which there exists such ├* which is also complete (i.e., the converse does hold). For example, this is the case when Σ has stratified witnesses. For sake of brevity, options for the implementation of ├* are not described. DESKOLEMIZE works for any ├* satisfying the condition above; the more complete ├* is, the larger the set of inputs on which DESKOLEMIZE succeeds. Accordingly, FIG. 8 illustrates a methodology for de-Skolemization in accordance with the subject invention.
Procedure DESKOLEMIZE (Σ)
At 800, an unnesting process is initiated. Set Λ1:={φ′:φ∈Σ} where φ′ is equivalent to and obtained from φ by “unnesting” terms and eliminating terms from relational atoms and from the conclusion so that in φ:

    
    
        (a) Function symbols occur only in equations in the premise.
        (b) Every term ƒ(ū) occurs in only one atom.
        (c) Every equation is of the form v=ƒ(ū) for some variable v (a term variable for ƒ), function ƒ, and sequence of variables ū (a defining equation) or of the form v=u for two term variables u and v (a restricting equation).
        (d) The conclusion contains at most one atom, which is not a defining equation.
    
    


Relational atoms in which a term variable occurs are called restricting atoms. If A is a restricting relational atom or a restricting equation in which v occurs, where v is a term variable for ƒ, A is called an ƒ-restricting atom. A constraint is called restricted if it has restricting atoms in the premise.
At 802, a check for cycles is performed. For every φ∈Λ1, construct the graph Gφ where the edges are variables in φ and where there is an edge (v, u) iff there is an equation of the form v=ƒ(. . . u . . . ). If Gφ has a cycle, abort. Otherwise, set Λ2:=Λ1.
At 804, a check for argument compatibility is performed. For every φ∈Λ2, check that φ does not contain two atoms with the same function symbol. If it does, abort. Otherwise, set Λ3:=Λ2.
At 806, variables are aligned. Rename the variables in Λ3 to obtain Λ4 satisfying:

    
    
        (a) For every function symbol θ and any two equations of the form v=ƒ(ū) and y=ƒ( x) in θ4, v is the same variable as y and ū is the same sequence of variables as x.
        (b) For every two different function symbols ƒ and g and any two equations of the form v=ƒ(ū) and y=g( x) in Λ4, v and y are different variables.
        If this is not possible, abort.
    
    


At 808, restricting atoms are eliminated. Pick some ordering of the function symbols in Λ4:ƒ1, . . . ƒk. Set Δ0=Λ4. For n=1, . . . , k−1, set Δn+1:={φ′:φ∈Δn} where φ′ is obtained from φ as follows. Set ψ to be φ with the ƒn+1-restricting atoms removed from the premise. If Δn├*ψ, set φ′:=ψ; otherwise set φ′:=φ. In any case, Δn+1≡Δn. Set Λ5:=Δk.
At 810, constraints with restricting atoms are eliminated. Set Λ6 to be the set of constraints φ∈Λ5 which can not be eliminated according to the following test: φ can be eliminated if

    
    
        (a) φ contains an ƒ-restricting atom in the premise, and
        (b) there is no constraint ψ∈Λ5 which has an ƒ-restricting atom in the conclusion and no ƒ-restricting atoms in the premise.
    
    


At 812, a check for restricted constraints is performed. Set Λ to the set of unrestricted constraints in Λ6. If there is any φ∈Λ6 such that Λ*φ, abort. Otherwise, set Λ7:=Λ.
At 814, a check for dependencies is performed. For every φ∈Λ7 and every variable v in φ, define Dφ,v as follows. If v is not a term variable, set Dφ,v={v}. If v is a term variable and v=ƒ(ū) is its defining equation in φ, then set Dφ,v:=∪u∈{ū}Dφ,u. Intuitively, Dφ,v is the set of variables on which v depends. Set Vφ:=the set of variables which appear in the conclusion of φ. For every term variable v in Vφ, check that Dφ,v=∪u∈VφDφ,u. If this fails, abort. Otherwise, set Λ8:=Λ7.
At 816, dependencies are combined. Set Λ9:={ψΦ:Ø≠Φ⊂Λ8} where ψΦ is defined as follows. If there is a function ƒ which appears in every φ∈Φ, then the premise of ψΦ consists of the atoms in all the premises in Φ and the conclusion of ψΦ consists of the atoms in all the conclusions of Φ (remove duplicate atoms). Otherwise, ψΦ is some constraint in Φ. Notice that Λ9 ⊂Λ8 since ψ{φ}=φ.
At 818, redundant constraints are removed. Pick some set Λ10 Λ9 such that Λ10├φ for every φ∈Λg, and such that this does not hold for any proper subset of Λ10.
Additionally, at 818, functions with ∃ variables are replaced. Set Λ11:={φ′:φ∈Λ10} where the premise of φ′ is the premise of φ with all equations removed and where the conclusion of φ′ is the conclusion of φ, with all variables appearing on the left of equations in φ existentially quantified.
At 820, unnecessary ∃ variables are eliminated. Set Λ12:={φ′:φ∈Λ11} and return Λ12 where φ′ is like φ, but where existentially quantified variables which do not appear in the conclusion atom have been removed (with their corresponding existential quantifier).
EXAMPLE 8
Consider three runs of the algorithm DESKOLEMIZE (Σ13i), for i∈{1, 2, 3}. Let Σ13i={γ1, . . . , γi} be a set of the following (unnested) SOCQ=-dependencies:
















γ1
R1(y), R2(x), y = f(x) → T1(x)



γ2
R2(x), y = f(x) → T2(y)



γ3
R2(x), y = f(x) → R1(y)










For completeness, note that each Σ13i is obtained by first de-Skolemizing CQ=-mappings given by Σ12i and Σ23i, which are shown below, and then invoking SOCQ= COMPOSE: 













i
Σ12i
Σ23i
Σ13i







1.
{α1, α2}
{β2}
{γ1}


2.
{α1, α2}
{β1, β2}
{γ1, γ2}


3.
{α1, α2, α3}
{β1, β2}
{γ1, γ2, γ3}









Dependencies α1, α2, α3, β1, β2 are specified as:

















α1
R1(x) → S1(x)



α2
R2(y) → ∃z(S2(zy))



α3
S2(zy) → R1(z)



β1
S2(zy) → T2(z)



β2
S1(x), S2(xy) → T1(y)










In all three runs of DESKOLEMIZE (Σ13i), processes 802 and 804 pass, since each of γ1, γ2, γ3 is cycle-free and has no multiple atoms with the same function symbol. Process 806 has no effect, since the variable names of the dependencies are already aligned. The remaining processes are explained below.
In the run DESKOLEMIZE ({γ1}), process 808 has no effect, because {γ1} is a singleton set. Its only member γ1 gets eliminated in process 810, since there are no rules in {γ1} with ƒ-restricting atoms in conclusions. Intuitively, γ1 is a tautology because an ƒ can be constructed whose range is disjoint with R1. Hence, {γ1} is equivalent to the empty set of constraints, which is trivially in IC(CQ).
In the run DESKOLEMIZE ({γ1, γ2}), γ2 contains an ƒ-restricting atom T2 in its conclusion. Hence, the restricted constraint γ1 can not be eliminated in process 810, and so de-Skolemization aborts in process 812.
In the run DESKOLEMIZE ({γ1, γ2, γ3}), de-Skolemization is possible despite γ2. In process 808, Δ0={γ1, γ2, γ3}. By considering the only function symbol θ get Δ1={ψ, γ2, γ3}≡Δ0 where ψ is obtained by eliminating the restricting atom R1(y) from the premise of γ1 as

ψ:=R2(x), y=ƒ(x)→T1(x).

Clearly, Δ0├*ψ, since Δ0⊃{γ1, γ3}├*ψ. Δ1 has no restricting constraints, so process 810 has no effect and process 812 passes. Process 814 succeeds with Λ8=Λ7={ψ, γ2, γ3}, since every dependency in Δ1 has at most one term variable y in its conclusion. For example, doing the calculation for γ3 yields Vγ3={x, y}, Dγ3,x=Dγ3,y=∪u∈V γ3Dγ3,u={x}. In process 816, combining the dependencies for Φ=Λ8 yields

γ4:=R1(y), R2(x), y=ƒ(x)→T1(x), T2(y), R1(y)

(Combinations resulting from proper subsets of Λ8 are not shown for brevity.) In process 818, the redundant constraints which include ψ, γ2, γ3 are removed because they share the premise with γ4 and their conclusion is subsumed by that of γ4; the result is Λ10={γ4}. Finally, at 818, replacing function ƒ by an existential variable in γ4 yields

Λ12={R2(x)→∃y(T1(x)^T2(y)^R1(y))}

Thus, DESKOLEMIZE ({γ1, γ2, γ3}) ⊂IC(CQ).

Theorem 7. If DESKOLEMIZE (Σ) succeeds on input Σ⊂IC(SOCQ=), then Σ′:=DESKOLEMIZE (Σ) satisfies

Σ′⊂IC(CQ=) and Σ′≡Σ.

The following follows from the description of the algorithm.

Proposition 3.

    
    
        1. DESKOLEMIZE (Σ) succeeds on input Σ⊂IC(SOCQ=) iff it reaches process 816, which can be checked in polynomial time in the size of Σ.
        2. Furthermore, if for some constant l independent of Σ, for every function symbol in Λ8 there are no more than l rules in Λ8 in which ƒ occurs, then DESKOLEMIZE (Σ) runs in polynomial time in the size of Σ.
    
    


From the first part of Proposition 3, it follows that sufficient conditions for success of CQ= COMPOSE (Σ12, Σ23) can be checked in polynomial time, because the size of the result of SKOLEMIZE is polynomial in the size of its input, and because sufficient conditions can be checked for the termination of SOCQ= COMPOSE (Σ′12, Σ′23) in polynomial time.
Since DESKOLEMIZE (Σ) may produce a result of size exponential in the size of Σ due to process 816, CQ= COMPOSE ompose (Σ12, Σ23) may produce a result of size exponential in the size of Σ12∪Σ23. The following example shows that in the general case this is unavoidable. However, the second part of Proposition 3 shows that we can efficiently check for more restrictive conditions that ensure not only that DESKOLEMIZE succeeds, but also that it terminates in polynomial time.
Theorem 8. For any subexponential function ƒ, there are source-to-target CQ-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) such that m13:=m12·m23 is a CQ-mapping which is not given by (σ1, Σ3, Σ13) for any Σ13 whose size is less than ƒ(s) where s is the size of Σ12∪Σ23.
Proof. (Outline) Pick k large enough so that ƒ(2kl)<2k where l is the size of the longest constraint below (which 9 is about 18+log k characters long). Such k must exist, since ƒ is subexponential. Set [k]:={1, . . . , k}. Consider the CQ=-mappings m12 and m23 given by (σ1, σ2, Σ12) and (σ2, σ3, Σ23) where

    
    
        E12 is R0(x)→∃y S0(xy)
        
            Ri(x)→Si(x)
        
        
        Σ23 is S0(xy), Si(x)→Ti(y)

for i∈[k], and where σ1={Ri: i∈{0, . . . , k}}, σ2={Si: i∈{0, . . . , k}}, and σ3={Ti: i∈[k]}. The composition m13:=m12·m13 is given by the set Σ13 of constraints

R0(x), RZ(x)→∃y TZ(y)

such that Z⊂[k], where RZ(x):=^i∈ZRi(x) and similarly for TZ. On the other hand, m 13 is not given by any (σ1, σ3, Σ) where Σ has fewer than 2k−1 constraints.

    
    


Domain, Range, and Other Operators
Composition is one of the operators that take models and/or mappings as inputs and give models and/or mappings as output. Composition can be performed using a combination of other operators, which in turn can be implemented using similar techniques as outlined above. These other operators include:
















Domain
dom(m)



Range
rng(m)



Intersection
A ∩ B



Identity
id(A)



Cross product
A × B



Intersection
m1 ∩ m2



Inverse
m−1










These operators are defined as follows.

dom(m):={A:∃B<A, B>∈m}.

rng(m):={B:∃A<A, B>∈m}.

∩:={A:A ∈, A∈B}.

id():={<A, A>:A∈}.

×:={<A, B>:A∈, B ∈}.

m1∩m2:={<A, B>:<A, B>∈m1<A, B>∈m2}.

m−1:={<B, A>:<A, B>∈m}.

In a relational case, with signatures, a signature is associated to every model and, input and output signatures to every mapping, and the obvious signature-compatibility conditions on these operators are required.
Proposition 4. Every ⊂CQ0 is closed under identity, cross product and intersection.
Proof If m12 and m34 are given by (σ1, σ2, Σ12) and (σ3, σ4, Σ34), and  and  are given by (σ1, Σ1) and (σ2, Σ2), then

    
    
        × is given by (σ1, σ2, Σ1, ∪Σ2).
        ∩ is given by (σ1, Σ1∪Σ2) (here σ1=σ2).
        m12∩m34 is given by (σ1, σ2, Σ12∪Σ34) (here σ1=σ3, and σ2=σ4).
    
    


To express identity, refer to the third auxiliary signature σ′2 (which is normally ignored) which contains, for every relation symbol R in or σ2, a relation symbol R of the same arity. In this case, σ1=σ2, so σ2=σ′1.

    
    
        id() is given by (σ1, σ1, σ′1, Σ1∪Σ) where Σ consists of two constraints of the form

∀( x)(R x→R′ x)

∀( x)(R′ x→R x)

        for every R in σ1.
    
    


Proposition 5. Each one of the operators, composition, range, and domain can be reduced to any one of the others.

    
    
        Proof. Suppose
        m12 is given by (σ1, σ2, Σ12),
        m23 is given by (σ2, σ3, Σ23),
        Let
        m1 be given by (σ1∪σ3, σ2, Σ12∪Σ23),
        m2 be given by (σ2, σ1∪σ3, Σ12∪Σ23),
        dom(m1) be given (σ1∪σ3, Σ1), and
        rng(m2) be given (σ1∪σ3, Σ2),
        Then m12·m23 is given by (σ1, σ3, Σ1) and by (σ1, σ3, Σ2).
    
    


This proves the composition can be expressed by either domain or range.
Conversely, suppose

    
    
        m12 is given by (σ1, σ2, Σ12).
        Let
        m21 be given by (σ2, σ1, Ø),
        m12·m21 be given by (σ1, σ1, Σ1), and
        m21·m12 be given by (σ2, σ2, Σ2).
    
    


Then dom(m12) and rng(m12) are given respectively by

(σ1, Σ1) and (σ2, Σ2).

This proves that domain and range can be expressed by composition.
All the languages considered satisfy the premises of Proposition 4. Therefore, Proposition 5 indicates that attention can be focused on closure under composition and inverse. Notice that if an -mapping m is given by (σ1, σ2, Σ12), then its inverse is given by (σ2, σ1, Σ12). However, the restrictions on  may be such that the second expression no longer gives an -mapping. For example, this happens with “source-to-target” expressions. In contrast, CQ0=, CQ=, and SOCQ= mappings are closed under inverse, so it is sufficient to study composition.
Proposition 5 implies that any algorithmic procedure that can be used to implement domain and range can be deployed for implementing composition. This can be achieved either directly, by invoking the algorithms presented supra, or indirectly, by first executing the operators domain and range, and then using their results to obtain the composition.
Computing Environments
Referring now to FIG. 9, there is illustrated a block diagram of a computer operable to execute the disclosed architecture. In order to provide additional context for various aspects of the subject invention, FIG. 9 and the following discussion are intended to provide a brief, general description of a suitable computing environment 900 in which the various aspects of the invention can be implemented. While the invention has been described above in the general context of computer-executable instructions that may run on one or more computers, those skilled in the art will recognize that the invention also can be implemented in combination with other program modules and/or as a combination of hardware and software.
Generally, program modules include routines, programs, components, data structures, etc., that perform particular tasks or implement particular abstract data types. Moreover, those skilled in the art will appreciate that the inventive methods can be practiced with other computer system configurations, including single-processor or multiprocessor computer systems, minicomputers, mainframe computers, as well as personal computers, hand-held computing devices, microprocessor-based or programmable consumer electronics, and the like, each of which can be operatively coupled to one or more associated devices.
The illustrated aspects of the invention may also be practiced in distributed computing environments where certain tasks are performed by remote processing devices that are linked through a communications network. In a distributed computing environment, program modules can be located in both local and remote memory storage devices.
A computer typically includes a variety of computer-readable media. Computer-readable media can be any available media that can be accessed by the computer and includes both volatile and nonvolatile media, removable and non-removable media. By way of example, and not limitation, computer readable media can comprise computer storage media and communication media. Computer storage media includes both volatile and nonvolatile, removable and non-removable media implemented in any method or technology for storage of information such as computer readable instructions, data structures, program modules or other data. Computer storage media includes, but is not limited to, RAM, ROM, EEPROM, flash memory or other memory technology, CD-ROM, digital video disk (DVD) or other optical disk storage, or any other medium which can be used to store the desired information and which can be accessed by the computer.
Communication media typically embodies computer-readable instructions, data structures, program modules, and includes any information delivery media. By way of example, and not limitation, communication media includes wired media such as a wired network or direct-wired connection, and wireless media such as acoustic, RF, infrared and other wireless media. Combinations of the any of the above should also be included within the scope of computer-readable media.
With reference again to FIG. 9, there is illustrated an exemplary environment 900 for implementing various aspects of the invention that includes a computer 902, the computer 902 including a processing unit 904, a system memory 906 and a system bus 908. The system bus 908 couples system components including, but not limited to, the system memory 906 to the processing unit 904. The processing unit 904 can be any of various commercially available processors. Dual microprocessors and other multi-processor architectures may also be employed as the processing unit 904.
The system bus 908 can be any of several types of bus structure that may further interconnect to a memory bus (with or without a memory controller), a peripheral bus, and a local bus using any of a variety of commercially available bus architectures. The system memory 906 includes read only memory (ROM) 910 and random access memory (RAM) 912. A basic input/output system (BIOS) is stored in a non-volatile memory 910 such as ROM, EPROM, EEPROM, which BIOS contains the basic routines that help to transfer information between elements within the computer 902, such as during start-up. The RAM 912 can also include a high-speed RAM such as static RAM for caching data.
The computer 902 further includes an internal hard disk drive (HDD) 914 (e.g., EIDE, SATA), which internal hard disk drive 914 may also be configured for external use in a suitable chassis (not shown), a magnetic floppy disk drive (FDD) 916, (e.g., to read from or write to a removable diskette 918) and an optical disk drive 920, (e.g., reading a CD-ROM disk 922 or, to read from or write to other high capacity optical media such as the DVD). The hard disk drive 914, magnetic disk drive 916 and optical disk drive 920 can be connected to the system bus 908 by a hard disk drive interface 924, a magnetic disk drive interface 926 and an optical drive interface 928, respectively. The interface 924 for external drive implementations includes at least one or both of Universal Serial Bus (USB) and IEEE 1394 interface technologies.
The drives and their associated computer-readable media provide nonvolatile storage of data, data structures, computer-executable instructions, and so forth. For the computer 902, the drives and media accommodate the storage of any data in a suitable digital format. Although the description of computer-readable media above refers to a HDD, a removable magnetic diskette, and a removable optical media such as a CD or DVD, it should be appreciated by those skilled in the art that other types of media which are readable by a computer, such as zip drives, magnetic cassettes, flash memory cards, cartridges, and the like, may also be used in the exemplary operating environment, and further, that any such media may contain computer-executable instructions for performing the methods of the invention.
A number of program modules can be stored in the drives and RAM 912, including an operating system 930, one or more application programs 932, other program modules 934 and program data 936. All or portions of the operating system, applications, modules, and/or data can also be cached in the RAM 912. It is appreciated that the invention can be implemented with various commercially available operating systems or combinations of operating systems.
A user can enter commands and information into the computer 902 through one or more wired/wireless input devices, e.g., a keyboard 938 and a pointing device, such as a mouse 940. Other input devices (not shown) may include a microphone, an IR remote control, a joystick, a game pad, a stylus pen, touch screen, or the like. These and other input devices are often connected to the processing unit 904 through an input device interface 942 that is coupled to the system bus 908, but can be connected by other interfaces, such as a parallel port, an IEEE 1394 serial port, a game port, a USB port, an IR interface, etc.
A monitor 944 or other type of display device is also connected to the system bus 908 via an interface, such as a video adapter 946. In addition to the monitor 944, a computer typically includes other peripheral output devices (not shown), such as speakers, printers, etc.
The computer 902 may operate in a networked environment using logical connections via wired and/or wireless communications to one or more remote computers, such as a remote computer(s) 948. The remote computer(s) 948 can be a workstation, a server computer, a router, a personal computer, portable computer, microprocessor-based entertainment appliance, a peer device or other common network node, and typically includes many or all of the elements described relative to the computer 902, although, for purposes of brevity, only a memory storage device 950 is illustrated. The logical connections depicted include wired/wireless connectivity to a local area network (LAN) 952 and/or larger networks, e.g., a wide area network (WAN) 954. Such LAN and WAN networking environments are commonplace in offices, and companies, and facilitate enterprise-wide computer networks, such as intranets, all of which may connect to a global communication network, e.g., the Internet.
When used in a LAN networking environment, the computer 902 is connected to the local network 952 through a wired and/or wireless communication network interface or adapter 956. The adaptor 956 may facilitate wired or wireless communication to the LAN 952, which may also include a wireless access point disposed thereon for communicating with the wireless adaptor 956.
When used in a WAN networking environment, the computer 902 can include a modem 958, or is connected to a communications server on the WAN 954, or has other means for establishing communications over the WAN 954, such as by way of the Internet. The modem 958, which can be internal or external and a wired or wireless device, is connected to the system bus 908 via the serial port interface 942. In a networked environment, program modules depicted relative to the computer 902, or portions thereof, can be stored in the remote memory/storage device 950. It will be appreciated that the network connections shown are exemplary and other means of establishing a communications link between the computers can be used.
The computer 902 is operable to communicate with any wireless devices or entities operatively disposed in wireless communication, e.g., a printer, scanner, desktop and/or portable computer, portable data assistant, communications satellite, any piece of equipment or location associated with a wirelessly detectable tag (e.g., a kiosk, news stand, restroom), and telephone. This includes at least Wi-Fi and BluetoothTM wireless technologies. Thus, the communication can be a predefined structure as with a conventional network or simply an ad hoc communication between at least two devices.
Wi-Fi, or Wireless Fidelity, allows connection to the Internet from a couch at home, a bed in a hotel room, or a conference room at work, without wires. Wi-Fi is a wireless technology similar to that used in a cell phone that enables such devices, e.g., computers, to send and receive data indoors and out; anywhere within the range of a base station. Wi-Fi networks use radio technologies called IEEE 802.11(a, b, g, etc.) to provide secure, reliable, fast wireless connectivity. A Wi-Fi network can be used to connect computers to each other, to the Internet, and to wired networks (which use IEEE 802.3 or Ethernet). Wi-Fi networks operate in the unlicensed 2.4 and 5 GHz radio bands, at an 11 Mbps (802.11a) or 54 Mbps (802.11b) data rate, for example, or with products that contain both bands (dual band), so the networks can provide real-world performance similar to the basic 10BaseT wired Ethernet networks used in many offices.
Referring now to FIG. 10, there is illustrated a schematic block diagram of an exemplary computing environment 1000 in accordance with the subject invention. The system 1000 includes one or more client(s) 1002. The client(s) 1002 can be hardware and/or software (e.g., threads, processes, computing devices). The client(s) 1002 can house cookie(s) and/or associated contextual information by employing the invention, for example.
The system 1000 also includes one or more server(s) 1004. The server(s) 1004 can also be hardware and/or software (e.g., threads, processes, computing devices). The servers 1004 can house threads to perform transformations by employing the invention, for example. One possible communication between a client 1002 and a server 1004 can be in the form of a data packet adapted to be transmitted between two or more computer processes. The data packet may include a cookie and/or associated contextual information, for example. The system 1000 includes a communication framework 1006 (e.g., a global communication network such as the Internet) that can be employed to facilitate communications between the client(s) 1002 and the server(s) 1004.
Communications can be facilitated via a wired (including optical fiber) and/or wireless technology. The client(s) 1002 are operatively connected to one or more client data store(s) 1008 that can be employed to store information local to the client(s) 1002 (e.g., cookie(s) and/or associated contextual information). Similarly, the server(s) 1004 are operatively connected to one or more server data store(s) 1010 that can be employed to store information local to the servers 1004.
What has been described above includes examples of the invention. It is, of course, not possible to describe every conceivable combination of components or methodologies for purposes of describing the subject invention, but one of ordinary skill in the art may recognize that many further combinations and permutations of the invention are possible. Accordingly, the invention is intended to embrace all such alterations, modifications and variations that fall within the spirit and scope of the appended claims. Furthermore, to the extent that the term “includes” is used in either the detailed description or the claims, such term is intended to be inclusive in a manner similar to the term “comprising” as “comprising” is interpreted when employed as a transitional word in a claim.

## Claims

1. A system that facilitates data mapping, comprising:
a processor that executes the following computer executable components stored on a computer readable medium:
a composition component that composes input schema mappings using a deductive procedure to obtain a finite axiomatization of all constraints that appear in the composition mapping and outputs a resulting schema mapping derived from the input schema mappings and that specifies a same set of constraints given by the input schema mappings to support data transformation and exchange for data warehousing, where data is received from many different sources for storage and access, and where the different sources are defined as a wired or a wireless network;
wherein the deductive procedure is concurrently performed on all constraints present in the input schema mappings when composing a sequence of three or more mappings, and wherein one or both of the input schema mappings are not functions, such as constraints between two schemas and the inverse of functions;
wherein the axiomatization includes a finite second-order axiomatization that is de-Skolemized to obtain a schema mapping expressed by first-order constraints; and the de-Skolemized finite second-order axiomatization comprises unnested second-order dependencies;
wherein the input schema mappings expressed by embedded dependencies are Skolemized to obtain intermediate schema mappings expressed by second-order dependencies and a finite axiomatization is computed of all constraints over input and output signatures which are deduced from constraints that give the intermediate schema mappings; and
wherein a check is performed to determine if a constraint of a form φ(z), R(y)→R(x) appears in the finite axiomatization, such that,
φ(z) is a conjunction of atoms over S1∪S3;

there is no atom R(w) in φ(z) with {x}⊂{w};
{x}is not a subset of {y}; and
R is a relation symbol in the schema S2.

2. The system of claim 1, wherein the deductive procedure is a complete deductive procedure that includes resolution.

3. The system of claim 1, wherein the deductive procedure is checked for termination and yielding of a correct result.

4. The system of claim 1, wherein the input schema mappings are expressed by embedded dependencies and Skolemized to obtain schema mappings expressed by a second-order dependencies.

5. The system of claim 1, wherein the deductive procedure computes at least one of an operator domain and an operator range using such that the input schema mappings are composed using the first procedure.

6. A computer readable medium having stored thereon the component of claim 1.

7. The system of claim 1, wherein the schema mappings are expressed by at least one of full, embedded, and second-order dependencies, which the second-order dependencies need not be in source-to-target form.

8. A method of mapping data, comprising:
employing a processor to execute computer executable instructions stored on a computer readable medium to perform the following acts:
composing input schema mappings with a composition component by using a deductive procedure to obtain a finite axiomatization of all constraints that appear in the composition mapping to support data transformation and exchange for data warehousing, where data is received from many different sources for storage and access, and where the different sources are defined as a wired or a wireless network;
concurrently performing the deductive procedure on all constraints present in the input schema mappings when composing a sequence of three or more mappings, wherein one or both of the input schema mappings are not functions, such as constraints between two schemas and the inverse of functions;
de-Skolemizing a finite second-order axiomatization to obtain a schema mapping expressed by first-order constraints and unnesting second-order dependencies;
Skolemizing input schema mappings expressed by embedded dependencies to obtain intermediate schema mappings expressed by second-order dependencies;
computing a finite axiomatization of all constraints over input and output signatures which are deduced from constraints that give the intermediate schema mappings;
outputting a resulting schema mapping derived from the input schema mappings to support data transformation and exchange; and
performing a check to determine if a constraint of a form φ(z), R(y)→R(x) appears in the finite axiomatization, such that,
φ(z) is a conjunction of atoms over S1∪S3;

there is no atom R(w) in φ(z) with {x}⊂{w};
{x}is not a subset of {y}; and
R is a relation symbol in the schema S2.

9. The method of claim 8, wherein the act of de-Skolemizing the finite axiomatization further comprises renaming variables in constraints such that all terms containing a same function symbol are unified.

10. The method of claim 9, further comprising renaming the variables by considering all pairs of constraints, which can be done in polynomial time.

11. The method of claim 8, wherein the act of de-Skolemizing the finite axiomatization further comprises an act of eliminating atoms that contain variables bound to Skolem terms.

12. The method of claim 8, further comprising the acts of:
Skolemizing the input schema mappings expressed by embedded dependencies to obtain intermediate schema mappings expressed by second-order dependencies;
computing a finite axiomatization of all constraints over input and output signatures which can be deduced from constraints that give the intermediate schema mappings; and
de-Skolemizing the finite axiomatization to obtain a schema mapping expressed by embedded dependencies.

13. A system that facilitates data mapping, comprising:
a processor coupled to a memory, the processor executing:
means for composing input schema mappings with a composition component by using a deductive procedure to obtain a finite axiomatization of all constraints that appear in the composition mapping to support data transformation and exchange for data warehousing, where data is received from many different sources for storage and access, and where the different sources are defined as a wired or a wireless network;
means for concurrently performing the deductive procedure on all constraints present in the input schema mappings when composing a sequence of three or more mappings, wherein one or both of the input schema mappings are not functions, such as constraints between two schemas and the inverse of functions;
means for Skolemizing the input schema mappings expressed by embedded dependencies to obtain schema mappings expressed by a second-order dependencies;
means for de-Skolemizing a finite second-order axiomatization to obtain a schema mapping expressed by first-order constraints and unnesting second-order dependencies;
means for Skolemizing input schema mappings expressed by embedded dependencies to obtain intermediate schema mappings expressed by second-order dependencies;
means for computing a finite axiomatization of all constraints over input and output signatures which are deduced from constraints that give the intermediate schema mappings;
means for outputting a resulting schema mapping derived from the input schema mappings to support data transformation and exchange; and
means for performing a check to determine if a constraint of a form φ(z), R(y)→R(x) appears in the finite axiomatization, such that,
φ(z) is a conjunction of atoms over S1∪S3;
there is no atom R(w) in φ(z) with {x}⊂{w};
{x}is not a subset of {y}; and
R is a relation symbol in the schema S2.