On the Undecidability of the Equivalence of Second-Order Tuple Generating Dependencies ? Ingo Feinerer, Reinhard Pichler, Emanuel Sallinger, and Vadim Savenkov Vienna University of Technology {feinerer|pichler|sallinger|savenkov}@dbai.tuwien.ac.at Abstract. Second-Order tuple generating dependencies (SO tgds) were intro- duced by Fagin et al. to capture the composition of simple schema mappings. Testing the equivalence of SO tgds would be important for applications like model management and mapping optimization. However, we prove the undecid- ability of the logical equivalence of SO tgds. Moreover, under weak additional assumptions, we also show the undecidability of a relaxed notion of equivalence between two SO tgds, namely the so-called conjunctive query equivalence. 1 Introduction Schema mappings play an important role in several areas of database research, notably in data integration [13], data exchange [9], peer data management [14], and model man- agement [6]. A schema mapping is given by two schemas, called the source schema and the target schema, as well as a set of dependencies describing the relationship between the source and target schema. The most fundamental form of schema mappings are mappings defined by a set of source-to-target tuple generating dependencies (s-t tgds): They are First-Order formulae of the form ∀x(ϕ(x) → ∃yψ(x, y)), where the an- tecedent ϕ(x) is a conjunctive query (CQ) over the source schema and the conclusion ψ(x, y) is a CQ over the target schema. Intuitively, such an s-t tgd defines a constraint that the presence of certain tuples in the source database I (namely those in the image of some homomorphism h from ϕ(x) to I) enforce the presence of certain tuples in the target database J (s.t. h can be extended to a homomorphism from ψ(x, y) to J). Several algebraic operators [6, 15] on schema mappings have been intensively stud- ied in recent time like computing inverses [8, 3, 2] and composing schema mappings [7, 12, 14, 16]. Our work is rather related to the composition operator. Fagin et al. proved that s-t tgds are not powerful enough to express the composition of two mappings de- fined by s-t tgds [12]. To remedy this defect, so-called Second-Order tuple generating dependencies (SO tgds) were introduced in [12]. SO tgds extend s-t tgds by existentially quantified function-variables and equalities of (possibly functional) terms. Details and formal definitions are given in Section 2. It was shown in [12] that SO tgds capture exactly the closure under composition of mappings defined by s-t tgds. Example 1 ([12]). Consider the following three schemas. Let S1 consist of the unary relation symbol Emp(·) of employees. Schema S2 consists of a single binary relation ? This work was supported by the Vienna Science and Technology Fund (WWTF), project ICT08-032. Savenkov was supported by the Erasmus Mundus ECW Program of the EU. symbol Mgr0 (·, ·) that associates each employee with a manager. Schema S3 consists of a similar binary relation symbol Mgr(·, ·) that is intended to provide a copy of Mgr0 and an additional unary relation symbol SelfMgr(·) to store employees who are their own manager. Consider the mappings M12 = (S1 , S2 , Σ12 ) and M23 = (S2 , S3 , Σ23 ) with Σ12 = {∀e(Emp(e) → ∃m Mgr0 (e, m))} and Σ23 = {∀e, m(Mgr0 (e, m) → Mgr(e, m)), ∀e(Mgr0 (e, e) → SelfMgr(e))}. We are looking for the composition of M12 and M23 . It can be verified that this composition can be expressed by the SO tgd σ = ∃f (∀e (Emp(e) → Mgr(e, f (e))) ∧ ∀e (Emp(e) ∧ (e = f (e)) → SelfMgr(e))). In this paper, we want to study the equivalence of SO tgds. Note that the question of equivalence naturally arises in several scenarios. Figure 1 illustrates a model evolution scenario, where data structured under some schema S is first migrated to a database with schema T and then further transformed to meet schema U . Now suppose that there exists an alternative migration path from σ schema S via T 0 to schema U . The question if the two migration paths yield the same re- T sult comes down to checking if the dependen- Σ12 Σ23 cies σ and σ 0 (which represent the respective mapping compositions) are equivalent. Actu- S U ally, Figure 1 can also be thought of as illus- Σ‘12 Σ‘23 trating a peer data management scenario, where T‘ some peer with data structured according to S provides part of its data to some other peer σ‘ with schema T (resp. T 0 ). The latter peer in turn passes this data on to yet another peer with Fig. 1. Mapping compositions. schema U . Now suppose that a user may access the data only at the peer with schema U . What happens if some link in this peer data network is broken, say the one corresponding to mapping Σ23 ? Will the path of mappings from S via T 0 to U still give the user full access to the data provided by the peer with schema S? Testing the equivalence of σ and σ 0 is thus crucial for answering questions of redundancy and reliability in a peer data network. The equivalence of mappings is also fundamental to mapping optimization. As men- tioned in [10], optimizing a mapping ultimately means replacing the mapping by an “equivalent” one with better (computational) properties. This raises the question of how the “equivalence” of two mappings should be defined. Since dependencies are logical formulae, the most natural notion of equivalence is logical equivalence. In this paper, we show that logical equivalence of SO tgds is undecidable. In order to allow for more flexibility in optimizing mappings, Fagin et al. introduced relaxed notions of equivalence [10]. In particular, the potential of conjunctive query (CQ) equivalence for optimizing several kinds of mappings was studied in [10]. Intuitively, two mappings are CQ-equivalent, if conjunctive queries posed against the target database yield the same result for both mappings (for details, see Section 2). For instance, it was shown in [12] that the composition of the mappings M12 and M23 in Example 1 cannot be represented by an SO tgd without equalities in the antecedent. On the other hand, σ in Example 1 is CQ-equivalent to σ 0 = ∃f (∀e (Emp(e) → Mgr(e, f (e))). Under the 2 weak additional assumption that the source schema may have key dependencies, we shall prove the undecidability of CQ-equivalence of SO tgds. Organization of the paper and summary of results. In Section 2, we recall some basic notions and results. A conclusion and an outlook to future work are given in Section 5. The main results of the paper are detailed in Sections 3 and 4, namely: • Logical equivalence. In Section 3 we prove that the logical equivalence of SO tgds is undecidable. This result is easily obtained via a previous undecidability result in the context of inverse schema mappings [3]. • Logical equivalence vs. CQ-equivalence. In Section 3, we also present a different proof strategy for the undecidability of the logical equivalence of two SO tgds in order to identify an important difference between logical equivalence and CQ-equivalence. More precisely, we show that logical equivalence of two SO tgds remains undecidable even if the two SO tgds are already known to be CQ-equivalent. • CQ-equivalence. In Section 4 we prove the undecidability of CQ-equivalence of SO tgds if the source schema may have key dependencies. The proof is by reduction from the domino problem. As a by-product of this proof, we also get the undecidability of logical equivalence of SO tgds without equalities. Due to lack of space, proofs are sketched. Details will be provided in the full version. 2 Preliminaries Schemas and instances. A schema R = {R1 , . . . , Rn } is a set of relation symbols Ri each of a fixed arity. An instance I over a schema R consists of a relation for each relation symbol in R, s.t. both have the same arity. For a relation symbol R, we write RI to denote the relation of R in I. We only consider finite instances here. Schema mappings. Let S = {S1 , . . . , Sn } and T = {T1 , . . . , Tm } be schemas with no relation symbols in common. A schema mapping is given by a triple M = (S, T, Σ) where S is the source schema, T is the target schema, and Σ is a set of logical formulae called dependencies expressing the relationship between S and T. Instances over S (resp. T) are called source (resp. target) instances. We write hS, Ti to denote the schema {S1 , . . . , Sn , T1 , . . . , Tm }. If I is a source instance and J a target instance, then hI, Ji is an instance of the schema hS, Ti. Given a (ground) source instance I, a target instance J is called a solution for I un- der M if hI, Ji |= Σ. The set of all solutions for I under M is denoted by Sol (I, M). Dependencies. Source-to-target tuple generating dependencies (as already defined in the introduction) are logical formulae of the form ∀x(ϕ(x) → ∃yψ(x, y)). We write x for a tuple (x1 , . . . , xn ). However, by slight abuse of notation, we also refer to the set {x1 , . . . , xn } as x. Hence, we may use expressions like xi ∈ x or x ⊆ X, etc. A key dependency over schema R is of the form ∀x(R(u, y, v) ∧ R(u, z, w) → y = z) where R denotes a relation symbol in R with u, v, w ⊆ x and y, z ∈ x. A second-order tuple generating dependency (SO tgd) is a logical formula of the form ∃f ((∀x1 (ϕ1 → ψ1 )) ∧ · · · ∧ (∀xn (ϕn → ψn ))) where (1) each member of f is a function symbol, (2) each ϕi is a conjunction of atomic formulas of the form 3 S(y1 , . . . , yk ) (with S ∈ S and yj ∈ xi ), and equalities of the form t = t0 (with t and t0 terms based on xi and f ), (3) each ψi is a conjunction of atomic formulas of the form T (t1 , . . . , t` ) (with T ∈ T where t1 , . . . , t` are terms based on xi and f ), and (4) each variable in xi appears in some atomic formula of ϕi . When dealing with instances hI, Ji in the context of SO tgds the domain of source instances I is allowed to consist only of constants (i.e., grounded) whereas target in- stances J may contain functional terms which can be treated like fresh variables, also called labelled nulls. [12] Homomorphisms. Let I, I 0 be instances. A homomorphism h: I → I 0 is a mapping s.t. (1) whenever R(x) ∈ I, then R(h(x)) ∈ I 0 , and (2) for every constant c, h(c) = c. If such h exists, we write I → I 0 . Moreover, if I ↔ I 0 then we say that I and I 0 are homomorphically equivalent. If a homomorphism h: I → I 0 is invertible, s.t. h−1 is also a homomorphism from I to I, then h is called an isomorphism, denoted I ∼ 0 = I 0 . An endomorphism is a homo- morphism I → I. An endomorphism is proper if it is not surjective (for finite instances, this is equivalent to being not injective), i.e., if it reduces the domain of I. If I is an instance, and I 0 ⊆ I is such that I → I 0 holds but for no other I 00 ⊂ I : I → I 00 (that is, I 0 cannot be further “shrunk” by a proper endomorphism), then I 0 0 is called a core of I. The core is unique up to isomorphism. Hence, we may speak about the core of I. Cores have the following important property: for arbitrary instances J and J 0 , J ↔ J 0 iff core(J) ∼ = core(J 0 ). If J ∈ Sol (I, M) is such that J → J 0 holds for any other solution J 0 ∈ Sol (I, M), then J is called a universal solution. Since the universal solutions for a source instance I are homomorphically equivalent, their core is unique up to isomorphism [11]. We write UnivSol (I, M) to denote the set of universal solutions for I under mapping M and we write core(I, M) to denote the core of the universal solutions. A substitution λ is a mapping which sends variables to other domain elements (i.e., variables or constants). We write λ = {x1 ← a1 , . . . , xn ← an } if λ maps each xi to ai and λ is the identity outside {x1 , . . . , xn }. The application of a substitution is usually denoted in postfix notation, e.g.: xλ denotes the image of x under λ. For an expression ϕ(x) (e.g., a conjunctive query with variables in x ), we write ϕ(xλ) to denote the result of replacing every occurrence of every variable x ∈ x by xλ. Chase. A target instance for a given source instance and a schema mapping can be computed by the chase [4]. For SO tgds, the original chase procedure of [4] has to be modified since homomorphisms now have to take the equalities in the antecedents into account. Formally, a mapping h from a conjunct Ci = ∀x(ϕi → ψi ) of an SO tgd to an instance I is a homomorphism if for every relational atom S(y1 , . . . , yk ) in ϕi the tuple (h(y1 ), . . . , h(yk )) is in S I and for every equality t = t0 we have h(t) = h(t0 ). Let hI, Ji be an instance of a schema hS, Ti and let Ci = ∀x(ϕi → ψi ) be an SO conjunct. If there is a homomorphism h of ϕi into the instance I, then the conjunct Ci can be applied to hI, J1 i with homomorphism h. I.e., for every target atom T (t1 , . . . , t` ) of ψi the tuple (h(t1 ), . . . , h(t` )) is added to the T relation and the union with J1 is taken yielding a new instance J2 . The instance hI, J2 i is now called the result of applying Ci to hI, J1 i with h. The actual application is called a chase step. 4 A chase sequence is a finite sequence of chase steps. The chase of hI, ∅i with an SO tgd Σ is a chase sequence until no conjuncts can be applied anymore. The result of this chase is denoted by chase(I, Σ). Chasing hI, ∅i with SO tgds can be done in polyno- mial time w.r.t. the size of the source instance and results in a universal solution [12]. Equivalence of schema mappings. Let M = (S, T, Σ) and M0 = (S, T, Σ 0 ) be two schema mappings. M and M0 are logically equivalent (denoted as M ≡ M0 ) if, for every source instance I and target instance J, the equivalence hI, Ji |= Σ ⇔ hI, Ji |= Σ 0 holds. This is the case iff Sol (I, M) = Sol (I, M0 ) holds for every source instance I. M and M0 are conjunctive-query equivalent (denoted as M ≡CQ M0 ) if, for every source instance I, either Sol (I, M) = ∅ = Sol (I, M0 ) or core(I, M) = core(I, M0 ). Note that the original definition of M ≡CQ M0 is that, for every source instance I, any conjunctive query posed against the target schema yields the same certain answers for the mappings M and M0 . The above characterization via the core, which is more convenient for our purposes here, was proved to be equivalent in [10]. 3 Undecidability of Logical Equivalence The undecidability of logical equivalence of two SO tgds follows easily from a previous undecidability result in the context of inverse schema mappings [3]. Theorem 1. Let τ and τ 0 be two SO tgds. It is undecidable whether τ ≡ τ 0 , i.e. that τ is logically equivalent to τ 0 . Proof. (Sketch).1 In [8], a schema mapping M2 is defined to be an inverse of another mapping M1 if their composition M1 ◦ M2 is logically equivalent  to the identity map- ping, i.e., a set of s-t tgds of the form (∀x) P (x) → P̂ (x) for every source relation P . In [3, Corollary 9.5] the authors show that the following problem is undecidable: Given mappings M1 and M2 specified by s-t tgds, check whether M2 is an inverse of M1 . In other words, checking if the composition M1 ◦ M2 is equivalent to the identity mapping is undecidable. Clearly, a set of s-t tgds can be represented as an SO tgd. Let τ denote the SO tgd corresponding to the set of s-t tgds of the identity mapping. Likewise, M1 ◦ M2 can be represented as an SO tgd, say τ 0 . Then τ ≡ τ 0 holds iff M2 is an inverse of M1 . Hence, the logical equivalence of two SO tgds is undecidable.  We now want to strengthen the above result by relating logical equivalence to CQ- equivalence. Below, we show that logical equivalence of two SO tgds remains undecid- able even if the two SO tgds are already known to be CQ-equivalent. To this end, we adopt a different proof strategy which goes by reduction from the following variant of the Halting problem: Given a Turing machine TM, does TM halt when run on empty input? Given an arbitrary instance TM of the Halting problem, we have to construct two SO tgds τ and τ 0 , s.t. the following equivalence holds: TM halts on empty input ⇔ τ 6≡ τ 0 . A major challenge of this reduction is that SO tgds do not directly provide us with recursion or with a means to enforce equalities. 1 We thank the anonymous referee of AMW 2011 who pointed out this proof. 5 Schemas. Let TM be a Turing machine (Q, A, δ, q0 ) with set of states Q = {0, . . . , m}, tape alphabet A = {0, . . . , n}, transition function δ : Q × A → Q × A × {←, →}, and initial state q0 . W.l.o.g., assume that q0 = 0 and let 1 denote the halting state. Moreover, let 1 denote the tape starting symbol . and let 0 denote the blank symbol t. We represent the state, tape and cursor of a Turing machine configuration at time t and tape location l by the function symbols stateq (t), tapea (t, l), and cursor(t, l) (where q ∈ Q, a ∈ A). Each of these functions is intended to have Boolean range, e.g. tapea (t, l) = 1 indicates that at time t, the symbol a is stored on the tape at location l, and tapea (t, l) = 0 otherwise. We will ensure this Boolean range using our SO tgds. As source schema, we use root(·) and chain(·, ·), which is intended to describe a linear order starting at root(r) and continued by chain(·, ·) atoms, i.e. source instance I should have the form I = {root(0), chain(0, 1), chain(1, 2), . . .}. Still, we must make sure through our SO tgds that what is described by root and chain does not deviate from a linear order in a way that adversely affects our simulation. We define our target schema to consist of the relation symbol range(·), which is intended to describe the range of the functions we defined above. Furthermore, we use the target relation symbol halt to indicate a halting computation as well as to signify an error condition. That is, an intended target instance should have the form J = {range(0), range(1)} and possibly include halt(). Dependencies. Given an arbitrary Turing machine TM, we define the SO tgds τ and τ 0 as a “big” conjunction consisting of several groups of conjuncts (i.e., implications). As we will see, it is possible to construct an SO tgd that simulates a computation of TM. We start by describing initialization conjuncts which are used to encode the initial configuration of the TM on the empty input tape. Since we cannot enforce equalities on the right-hand side of implications, all the implications are formulated in such a way that taking the wrong value will lead to an error condition indicated by halt(). E.g., we want to enforce the initial state state0 (r) = 1. Therefore, in the case that state0 (r) = 0 holds, we enforce halt() in the target instance to indicate this error condition: • root(r) ∧ state0 (r) = 0 → halt() Note that this does not yet cover the case that state0 (r) 6∈ {0, 1}. We construct other implications which define the rest of the initial configuration analogously. We now define transition conjuncts, which implement the transition function of TM. In what follows, we write dom(z) as a short-hand for a predicate that is satisfied by instantiating z to an arbitrary constant occurring in the source instance, i.e., dom(z) has to be replaced by root(z), chain(z, ), or chain( , z). Such a predicate is needed to fulfil the safety condition of SO tgds. We first define a common part of the following implications, matching the current state q and the current tape symbol a. ϕ := stateq (t) = 1 ∧ cursor(t, l) = 1 ∧ tapea (t, p) = 1 ∧ chain(t, t0 ) ∧ dom(l) Suppose that the transition function δ contains the transition δ(q, a) = (q 0 , a0 , ←). Then the SO tgds τ and τ 0 contain the following conjuncts: • ϕ ∧ stateq0 (t0 ) = 0 → halt() • ϕ ∧ tapea0 (t0 , l) = 0 → halt() • ϕ ∧ chain(l0 , l) ∧ cursor(t0 , l0 ) = 0 → halt() 6 While the transition conjuncts define what changes, we now construct inertia con- juncts which describe the function values of what remains the same. In particular, we can construct (but for space reasons omit here) conjuncts, which define that the cursor is not located at positions that are (a) more than one move away from the previous cursor location, (b) at the same location, or (c) at the location opposite to the cursor movement. Furthermore, we need to state that the tape symbol remains the same wherever the cursor is not located. That is, for each q ∈ Q, a ∈ A: • stateq (t) = 1 ∧ cursor(t, l) = 0 ∧ tapea (t, l) = 1 ∧ dom(l) ∧ chain(t, t0 ) ∧ tapea (t0 , l) = 0 → halt() Finally, we also have to construct uniqueness conjuncts, ensuring that at each time t, there is exactly one stateq (t) and at each time t and location l exactly one tapea (t, l) whose function value is 1. Guarding conjuncts. It is clear that, since the domain is in general non-Boolean, we cannot prevent functions stateq , tapea and cursor to take a range outside of {0, 1} for arbitrary interpretations. However, the structure of our reduction will show that we have to either, for a given interpretation of the function symbols, define the interpretation of the relation symbols, or for a given interpretation of the relation symbols, define the interpretation of the function symbols. So if we define the functions, we can guarantee Boolean domain ourselves. If we define the relations, and in particular the target relations, we can use function guarding conjuncts to materialize the range in the target: • dom(x) ∧ dom(y) ∧ state (x) = y → range(y) Analogous conjuncts are introduced for tape and cursor. This ensures the Boolean range of our functions, given appropriately constructed target relations (rangeJ = {0, 1}). Now that we have sufficient control over the functions, we still need to gain some control over the source instance, since our simulation is intended to work on a linear order described by root and chain. We therefore define source guarding conjuncts. What we can directly enforce is that the chain relation includes no self-loops and never returns to any root using the following conjuncts: • chain(x, x) → halt() • root(r) ∧ chain( , r) → halt() However, what we cannot directly exclude is that some element x of the chain has two distinct predecessors px 6= px0 with chain(px, x) and chain(px0 , x). In particular, we do not have equality on the right-hand side, which would allow us to require px = px0 . Nor can we use a derivation of halt() when there are two predecessors chain(px, x) and chain(px0 , x) because we cannot guarantee that px 6= px0 on the left-hand side. But what we can do is control the effect of such multiple predecessors (or succes- sors). Notably, if these multiple predecessors or successors actually have no effect on our simulation, then we have no problem with these discrepancies from linear order, since the simulation is doing the correct thing anyway. Altogether, we cannot detect all deviations from a linear order, e.g., two distinct root(r) atoms cannot be ruled out. But we can gain just enough control to ensure the correctness of our reduction. Halting detection. We now construct the two SO tgds for our reduction, namely such that TM halts ⇔ τ 6≡ τ 0 . The first one, τ , simply consists of all the conjuncts we 7 constructed up to this point, that is simulation conjuncts and guarding conjuncts. The function symbols tape , state and cursor are in the scope of an existential quantifier over the entire conjunction. We now define the halting detection conjunct: • dom(t) ∧ state1 (t) = 1 → halt() and construct τ 0 to be the same as τ plus this halting detection conjunct. So overall, both τ and τ 0 simulate the computation of Turing machine TM, but only τ 0 indicates a halting state by enforcing halt(). Theorem 2. Let τ and τ 0 be two SO tgds. It is undecidable whether τ ≡ τ 0 (i.e. τ is logically equivalent to τ 0 ), even when τ ≡CQ τ 0 (i.e. τ is CQ-equivalent to τ 0 ). Proof. (Sketch). We constructed τ 0 as τ with an additional conjunct, therefore it is suf- ficient to show that TM halts ⇔ τ 6 τ 0 . We show both directions separately. The chal- lenging part of the reduction is that, in one direction we have control over the functions, but not over the relations, and the converse for the other direction. Assume that TM halts. Then we have to find an instance K = (I, J) such that K  τ but K 6 τ 0 . Since TM halts, there is a computation of length n that ends in the halting state. We construct the instance K = (I, J) as I = {root(1), chain(1, 2), . . . , chain(n − 1, n)} J = {range(0), range(1)} Then K  τ is clearly the case. What needs to be shown is that K 6 τ 0 . In particular, K 6 τ 0 means that for arbitrary f , we have (K, f ) 6 ϕ0 . That is, we constructed K, but must deal with arbitrary f for ϕ0 . We proceed by case distinction, assuming vt,l,a is the correct value of tapea (t, l) according to the transition function of TM: 1. tapea (t, l) = vt,l,a for all t, l, a, that is, it correctly represents the TM computation 2. tapea (t, l) = ¬vt,l,a for some t, l, a, that is, the simulation violates TM 3. For some tapea (t, p) = y we have that y 6∈ {0, 1}, i.e., non-Boolean range and in each case show K, f 6 τ 0 . This also holds for state and cursor. Assume that TM does not halt. Given an arbitrary instance K = (I, J), we have to show that K  τ implies K  τ 0 . That is, we deal with arbitrary K, but only have to find a single f for ϕ0 . Assume that TM does not halt. Then let K = (I, J) be an arbitrary instance. We proceed by case distinction based on K: 1. J already contains an atom halt() 2. Source instance I deviates from a linear order significantly for our simulation 3. J contains some range(c) atom with c 6∈ {0, 1}, i.e., allows non-Boolean range 4. All range(c) atoms in J have c ∈ {0, 1} and in each case show K, f  τ 0 . Finally, note that the SO tgds τ and τ 0 in the above problem reduction are CQ-equivalent. The claim of the theorem thus follows.  Equalities are fundamental in SO tgds in order to define the composition of two schema mappings [12, Theorem 5.4]. Equalities also play a central role in our unde- cidability proof of logical equivalence for SO tgds in Theorem 2 above. However, if we consider CQ-equivalence rather than logical equivalence, then the equalities are not strictly necessary anymore and can be removed: In [2] it is proved that every SO tgd is CQ-equivalent to a plain SO tgd (a class of SO tgds which do not contain equalities). As a consequence the previous proof idea cannot be reused and we need a set of new proof techniques to show undecidability also for CQ-equivalence. 8 4 Undecidability of Conjunctive Query Equivalence We now show the undecidability of CQ-equivalence of SO tgds by a reduction from the Domino Problem (DP), which was first shown undecidable by Berger [5]. We use the following, slightly modified version of DP [1, p.414]. Definition 1. A domino system (DS) is given by a set D of domino types defined as follows. Let C be a set of colours. Then, each domino type is a quadruple hl, t, r, bi of values from C, corresponding respectively to the left, top, right and bottom colour of a square domino piece. Let d.side denote an accessor function D → C returning the colour of d, corresponding to side. Then, the Domino Problem (DP) given by D asks if for each m, n ∈ N a consistent tiling of an m × n grid with the domino types from D exists. That is, if there is a function tm,n : {1 . . . m} × {1 . . . n} → D, such that the equality tm,n (i, j).right = tm,n (i + 1, j).left holds for 1 ≤ i < m and 1 ≤ j ≤ n and tm,n (k, l).bottom = tm,n (k, l + 1).top for 1 ≤ k ≤ m and 1 ≤ l < n. Chains, proper instances, and coordinates. We model a grid using the source schema S consisting of two binary relations Ch and Cv intended to define a horizontal and vertical successor relation: For an instance I of S, ChI and CvI denote the relations of I. Their intended form is {(a0 , a1 ), (a1 , a2 ) . . . (an−1 , an )}, with ai 6= aj , for every 0 ≤ i < j ≤ n. We define a < b w.r.t. an order C, if (a, b) ∈ C or ∃x, C(x, b) ∧ a < x. Taking the tuples of C as edges of a directed graph (which we call the dual graph), the order defined above corresponds to an acyclic chain. If each relation of an instance I over S contains a single acyclic chain, I is called proper. The size (m, n) of such a proper instance I is defined as (|Ch |, |Cv |). Domino tilings are modelled by the target relation D/4. Each of its four arguments is populated by a functional term cs (x, y) where c corresponds to the colour, s to the side of the domino piece, and the pair (x, y) defines the position in the grid. To save notation, we will omit parentheses when writing the terms in the relation D (e.g. the above term will be written as cs xy). Given a fact d ∈ D, we define the accessor function d.n, returning the term in the nth place of d, 1 ≤ n ≤ 4. Definition 2. Let D be a DS with types d1 . . . dn . A simulation mapping ΣD for D over the source schema S = {Ch (·, ·), Cv (·, ·)} and the target schema T = {D(·, ·, ·, ·)} consists of an SO tgd τD and four source key dependencies: 1 : Ch (x, x1 ) ∧ Ch (x, x2 ) → x1 = x2 2 : Ch (x1 , x) ∧ Ch (x2 , x) → x1 = x2 3 : Cv (x, x1 ) ∧ Cv (x, x2 ) → x1 = x2 4 : Cv (x1 , x) ∧ Cv (x2 , x) → x1 = x2 The SO tgd τD has the form ∃c∃ph ∃pv ∃q h ∃q v (τd1 ∧ . . . ∧ τdn ∧ γ1 ∧ γ2 ), where τd1 . . . τdn encode the corresponding domino types: τdi : Ch (x1 , x2 ) ∧ Cv (y1 , y2 ) → D(lh x1 y2 , tv x2 y1 , rh x2 y2 , bv x2 y2 ), l, t, r, b denoting respectively the left, top, right and bottom colours of di . Superscripts distinguish the horizontal and vertical dimensions, so that there are at most two distinct functions in c for each colour in D. Moreover, c contains neither ph|v nor q h|v . The conjuncts γ1 and γ2 are called guards and have a form similar to τdi : γh : Ch (x0 , x1 ) ∧ Ch (x1 , x2 ) ∧ Cv (y1 , y2 ) → D(ph x1 y2 , pv x2 y1 , ph x2 y2 , pv x2 y2 ) γv : Ch (x1 , x2 ) ∧ Cv (y0 , y1 ) ∧ Cv (y1 , y2 ) → D(q h x1 y2 , q v x2 y1 , q h x2 y2 , q v x2 y2 ) 9 D I = {Ch (0, 1), Ch (1, 2), Ch (2, 3), Cv (0, 1), Cv (1, 2)} wv 1 0 gv 2 0 wv 3 0 a wh 0 1 a gh 1 1 gh 1 1 c gh 2 1 gh 2 1 d wh 3 1 b gv 1 1 wv 2 1 wv 3 1 v c g 11 wv 2 1 wv 3 1 wh 0 2 b wh 1 2 wh 1 2 a gh 2 2 gh 2 2 d wh 3 2 d wv 1 2 gv 2 2 wv 3 2 Fig. 2. Dotted rectangles are facts in core(I, ΣD ), corresponding to a consistent tiling Informally, given a proper source instance of size (m, n), the conjuncts τd1 . . . τd|D| create a stack of |D| domino tiles at each position in the m × n grid. Additionally, the guards γh and γv create two more tiles with unique colours p and q on each position (i, j) with i, j > 1, or a single tile if i = 1 or j = 1. The guards tackle source instances with cycles instead of the linear order, as will be explained later. For a source instance I, a D-fact d enforced by the SO tgd in a simulation map- ping (that is, d ∈ chase(I, ΣD )) has a form D(lh xp y, tv xyp , rh xy, bv xy), such that (xp , x) ∈ ChI , (yp , y) ∈ CvI . Definition 3. Let D be a DS and I a proper instance I of size (m, n). A fact d = D(lh xp y, tv xyp , rh xy, bv xy) ∈ chase(I, ΣD ) is associated with the domino type hl, t, r, bi, and with the pair (x, y) of I-values, occurring as arguments in its two last terms. Moreover, let i be the ordinal of x w.r.t. the order defined by ChI and j be the or- dinal of y w.r.t. CvI . We call the pair (i, j) the coordinates of d defining its grid position. Property 1. Let I be a proper source instance, and ΣD the simulation mapping of a DS D. Moreover, let d1 and d2 be two facts in chase(I, τD ), d1 associated with the pair of I-values (x1 , y1 ), and d2 with (x2 , y2 ). Then, the following properties hold true: 1. d1 .3 = d2 .1 ⇒ (x1 , x2 ) ∈ ChI ∧ y1 = y2 ∧ ∀i 6= 3 ∀j 6= 1 d1 .i 6= d2 .j. 2. d1 .2 = d2 .4 ⇒ (y1 , y2 ) ∈ CvI ∧ x1 = x2 ∧ ∀i 6= 4 ∀j 6= 2 d1 .i 6= d2 .j. 3. ∃i ∈ {1...4} d1 .i = d2 .i ⇒ x1 = x2 ∧ y1 = y2 . 4. d1 .1 6= d2 .2 ∧ d1 .3 6= d2 .4 ∧ d1 .1 6= d2 .4. Claim 1 stipulates, that whenever a term is shared between the 3rd place of d1 and the 1st place of d2 , the facts correspond to horizontally adjacent grid positions (i.e., have first coordinates i and i + 1 and the same second coordinate) and can have no further terms in common. Claim 2 is an analogue of Claim 1 for the equality d1 .4 = d2 .2 and vertical adjacency: d1 and d2 must have coordinates (i, j) and (i, j + 1). Claim 3 states that terms at respective positions can be only shared by facts with the same coordinates. Finally, Claim 4 restricts term equalities to the above cases. Example 2. Consider a DS D containing the four types a, b, c, d in Figure 2. In the sim- ulation mapping ΣD , the first type is modelled by the following implicational conjunct in the SO tgd τa : Ch (x1 , x2 )∧Cv (y1 , y2 ) → D(wh x1 y2 , wv x2 y1 , g h x2 y2 , g v x2 y2 ). Here, w and g stand for white and gray colours, respectively. 10 The 3 × 2 grid is represented by a proper source instance I (see top of Figure 2). Six dotted rectangles represent a consistent tiling of this grid with D. Each rectangle bears the four terms of the corresponding D-fact in chase(I, ΣD ): E.g., the topmost leftmost tile (the one at position (1,1), that is) is encoded by the fact D(wh 01, wv 10, g h 11, g v 11). Problem reduction. Let D be a DS and ΣD its simulation mapping. Furthermore, con- sider a singleton colour set Cb = {b} (where b stands for “black”) and a corresponding domino set B = {hb, b, b, bi} with the simulation mapping ΣB . We claim that D has a solution iff ΣD ≡CQ ΣB holds. The SO tgd in ΣB has the following form: τB : ∃bh ∃bv∃ph ∃pv ∃q h∃q v Ch (x1 , x2 ) ∧ Cv (y1 , y2 ) → D(bh x1 y2 , bv x2 y1 , bh x2 y2 , bv x2 y2 ) ∧ γh ∧ γv . It is easy to see that the conjuncts γh and γv are redundant in τB . Hence, in the follow- ing we assume τB to contain a single implicational conjunct and no guards. Moreover, the following relationship holds between the chase result of τB and τD : Property 2. Let D be a DS with simulation mapping ΣD , let (i1 , j1 ) and (i2 , j2 ) be two distinct grid positions, and let d1 , d2 ∈ chase(I, ΣD ) be facts at positions (i1 , j1 ) resp. (i2 , j2 ). Then also chase(I, ΣB ) contains two facts d01 , d02 at these grid positions. Moreover, for every 1 ≤ k, l ≤ 4, if d1 .k = d2 .l then d01 .k = d02 .l, i.e., if two terms in d1 and d2 are equal, then the terms at these places in d01 and d02 are also equal. This property uses an observation, that every implicational conjunct τdi encoding a domino type di in the SO tgd of a simulation mapping produces exactly one D-fact for each grid position, and that τB ∈ ΣB uses the minimal set of functional symbols. For DPs that have a solution (of which B is obviously an example) the following lemma, which is crucial for our construction, holds: Lemma 1. Let I be a proper instance of size (m, n) and let D be a DS. Then, there is a consistent tiling of an m × n grid with D iff core(I, τD ) ∼ = core(I, ΣB ) holds. Example 3. It is easy to check, that the six D-facts in Figure 2 indeed form core(I, ΣD ). For I, ΣB yields a solution with the isomorphic core: each fact in core(I, ΣB ) can be obtained from some fact of core(I, ΣD ) by replacing leading symbols w and g with b. To lift the equivalence between solvability of D and existence of an isomorphism core(I, ΣD ) ∼ = core(I, ΣB ) to unrestricted source instances I, we will first show, that whenever ChI or CvI contains a single cycle (that is, its dual graph is connected, each ver- tex having a single incoming and a single outgoing edge), then any simulation mapping yields an instance with the same core as chase(I, ΣB ). Lemma 2. Let I contain a single cycle in Ch or in Cv . Then, for arbitrary DS D, core(I, ΣD ) ∼ = core(I, ΣB ) holds. Proof (Sketch). W.l.o.g. assume that the single cycle is contained in Ch . For such I, the guard γh in the SO tgd τD ∈ ΣD is indistinguishable from τB in ΣB . Indeed, the conclusions of these implications coincide up to renaming of functional terms. The antecedent ϕh of γh has an extra atom C(x0 , x1 ), that prevents it from being satisfied by a Ch -fact at the beginning of the chain. However, if ChI is a cycle, the relations q1|2 11 defined as q1 (x1 , x2 ) ↔ Ch (x1 , x2 ) and q2 (x1 , x2 ) ↔ ∃x0 Ch (x0 , x1 ) ∧ Ch (x1 , x2 ), coincide, and so do τB and γh . Hence, J = chase(I, ΣD ) contains a subinstance JB isomorphic to chase(I, ΣB ). Using Property 2, J → JB can be shown.  Next, we address the source instances I containing multiple connected components I in Ch|v . The connectedness is defined as follows: Given an instance K, the fact graph GK has the facts of K as vertices, connected by an undirected edge whenever corre- sponding facts have a common term. The facts f1 , f2 ∈ K are connected, if there is a path between the corresponding vertices in GK . The following property can be shown by induction on the length of the path between two D-facts: Lemma 3. Let ΣD be a simulation mapping, I a source instance over S, and let d1 , d2 be facts in J = chase(I, ΣD ) containing respectively terms α(x1 , y1 ) and β(x2 , y2 ). Assume that x1 is a term in a fact c0h ∈ ChI , and x2 in c00h ∈ ChI . Likewise, let y1 and y2 occur, respectively, in the facts c0v , c00v ∈ CvI . Then, d1 and d2 are connected in J only if the facts c0h and c00h are connected in ChI , and so are c0v and c00v in CvI . The above lemma implies, that if the source I contains lh and lv connected components in ChI and CvI respectively, then for any simulation mapping Σ, chase(I, Σ) can be decomposed into lh lv pairwise disconnected instances. Furthermore, if dual graphs of I the connected components of Ch|v are acyclic chains or cycles, then by applying one of the Lemmas 1, 2 in each of the lh lv cases, the reduction established by these lemmas can I be lifted to the the case when relations Ch|v contain multiple connected components. Finally, we observe that union of chains and cycles is the only type of dual graphs which is relevant. Indeed, if the dual graph of a source instance I contains a V-formed subgraph {C(x, y1 ), C(x, y2 )} or {C(y1 , x), C(y2 , x)} with y1 6= y2 , then the key de- pendencies ensure that for any simulation mapping Σ (including ΣB ) the set Sol (I, Σ) is empty. This concludes our reduction from the domino problem to CQ-equivalence of SO tgds. We may thus formulate the main result of this section. Theorem 3. The CQ-equivalence of mappings consisting of SO tgds and source key dependencies is undecidable. For the simulation mappings ΣD and ΣB in the above problem reduction, it can be easily proved that ΣD ≡CQ ΣB holds iff ΣD ≡ ΣB holds. We thus immediately get Theorem 4. The logical equivalence of mappings consisting of SO tgds without equal- ities in the antecedents and source key dependencies is undecidable. 5 Conclusion Testing the equivalence of schema mappings is a fundamental task. For mappings de- fined by s-t tgds and target dependencies in the form of tgds and equality generating de- pendencies (egds) this problem has been well studied. In the general case, the (logical) equivalence of such mappings is undecidable. If the target tgds admit a finite chase, then the problem becomes decidable [4]. In [10], two relaxed notions of equivalence were introduced, namely the CQ-equivalence studied here and data exchange equivalence 12 (DE-equivalence). Moreover, in [10], the undecidability of CQ-equivalence was proved for mappings consisting of s-t tgds and target tgds. The undecidability was extended in [17] in two directions, namely to mappings with target egds and from CQ-equivalence to DE-equivalence. The equivalence of SO tgds has been unexplored so far. In this paper, we have proved the undecidability of logical equivalence. For the case of source schemas with key dependencies, we proved the undecidability of CQ- equivalence. The status of CQ-equivalence without any assumptions on the source schema has been left open. Closing this gap is on top of the agenda for future work. Moreover, the search for decidable fragments should be initiated. Finally, we also want to study the DE-equivalence [10] mentioned above. We conjecture that DE-equivalence of SO tgds is also undecidable. However, this has to be proved yet. References 1. C. Allauzen and B. Durand. The classical decision problem, by E. Börger, E. Grädel and Yu. Gurevich, chapter “Appendix A: Tiling Problems”, pages 407–420. Springer, 2001. 2. M. Arenas, J. Pérez, J. L. Reutter, and C. Riveros. Composition and inversion of schema mappings. SIGMOD Record, 38(3):17–28, 2009. 3. M. Arenas, J. Pérez, and C. Riveros. The recovery of a schema mapping: Bringing exchanged data back. ACM Trans. Database Syst., 34(4), 2009. 4. C. Beeri and M. Y. Vardi. A proof procedure for data dependencies. J. ACM, 31(4):718–741, 1984. 5. R. Berger. The undecidability of the domino problem. Amer Mathematical Society, 1966. 6. P. A. Bernstein. Applying model management to classical meta data problems. In Proc. CIDR’03, 2003. available from http://www-db.cs.wisc.edu/cidr/cidr2003/program/p19.pdf. 7. P. A. Bernstein, T. J. Green, S. Melnik, and A. Nash. Implementing mapping composition. VLDB J., 17(2):333–353, 2008. 8. R. Fagin. Inverting schema mappings. In Proc. PODS’06, pages 50–59. ACM, 2006. 9. R. Fagin, P. G. Kolaitis, R. J. Miller, and L. Popa. Data exchange: semantics and query answering. Theor. Comput. Sci., 336(1):89–124, 2005. 10. R. Fagin, P. G. Kolaitis, A. Nash, and L. Popa. Towards a theory of schema-mapping opti- mization. In Proc. PODS’08, pages 33–42. ACM, 2008. 11. R. Fagin, P. G. Kolaitis, and L. Popa. Data exchange: getting to the core. ACM Trans. Database Syst., 30(1):174–210, 2005. 12. R. Fagin, P. G. Kolaitis, L. Popa, and W. C. Tan. Composing schema mappings: Second-order dependencies to the rescue. ACM Trans. Database Syst., 30(4):994–1055, 2005. 13. A. Y. Halevy, A. Rajaraman, and J. J. Ordille. Data integration: The teenage years. In Proc. VLDB’06, pages 9–16. ACM, 2006. 14. J. Madhavan and A. Y. Halevy. Composing mappings among data sources. In Proc. VLDB’03, pages 572–583, 2003. 15. S. Melnik. Generic Model Management: Concepts and Algorithms, volume 2967 of Lecture Notes in Computer Science. Springer, 2004. 16. A. Nash, P. A. Bernstein, and S. Melnik. Composition of mappings given by embedded dependencies. ACM Trans. Database Syst., 32(1):4, 2007. 17. R. Pichler, E. Sallinger, and V. Savenkov. Relaxed notions of schema mapping equivalence revisited. In Proc. ICDT’11, pages 90–101. ACM, 2011. 13