Database Reference
In-Depth Information
of the powerset automaton contains
q
i
. This is ensured by adding for each
q
k
∈
δ
(
a
l
,
q
i
,
q
j
)
the st-tgd
//
[
q
k
/
no
,
label
/
a
l
,
left
/
q
i
/
yes
,
right
/
q
j
/
yes
]
−→ ⊥
,
where
⊥
is a fixed pattern inconsistent with
S
t
,e.g.
r
/
r
. Similarly we enforce that every
state, in which
A
can be after reading a leaf with a given label, is a
yes
-state:
//
[
q
k
/
no
,
label
/
a
l
,
leaf
]
−→ ⊥
for
q
k
∈
δ
(
a
l
,
q
0
,
q
0
)
.
Finally, we check that in the root of the run only nonfinal states are present:
r
/
q
k
/
yes
−→ ⊥
for
q
k
∈
Q
−
F
.
The obtained mapping is consistent iff there is a tree rejected by
A
.
Now using a simple observation we can immediately extend the algorithm presented
above to the case with variables, provided that data comparisons are not allowed, and con-
clude the proof of
Theorem 18.1
.
Proof of
Theorem 18.1
In the absence of data comparisons we can simply “forget” about
the data values. For a tree pattern
π
◦
denote a tree pattern obtained from
π
,let
π
by replac-
{
π
1
−→
π
2
ing all subformulae of the form
(
t
) with
,for
being a label or .Let
Σ
st
=
Σ
st
)
(
π
1
−→ ∃
z
π
2
)
∈
Σ
st
}
. It is not difficult to see that (
S
s
,
S
t
,
Σ
st
) is consistent iff (
S
s
,
S
t
,
is consistent.
Note that the complexity is relatively high, but the input to the problem consists of
metadata
only (the schemas, and dependencies between them) and not the actual data.
Thus, in many cases a single-exponential bound is actually acceptable. Later we shall see
how to lower it under some restrictions.
Undecidable cases of consistency
We now move to classes of schema mappings that allow comparisons of attribute values.
It is common to lose decidability (or low complexity solutions) of static analysis prob-
lems once data values and their comparisons are considered. Here we witness a similar
situation: having either descendant or next-sibling, together with either = or
=, leads to
undecidability of consistency.
+
,
=)
,
Theorem 18.4
Each
of
the
following
problems
is
undecidable:
C
ONS
(
↓
,
↓
+
,
↓
,
↓
↓
,
→
,
=)
, and
C
ONS
(
↓
,
→
,
C
ONS
(
=)
,
C
ONS
(
=)
.
+
,
=). The remaining cases are left as
an exercise. We describe a reduction from the halting problem of a two-register machine,
which is known to be undecidable. That is, given a two-register machine (defined below),
we construct a schema mapping that is consistent iff the machine halts. Trees encoding
runs of a two-register machine will be of the form:
Proof
We only prove undecidability of C
ONS
(
↓
,
↓
