Database Reference
In-Depth Information
and
Σ
23
consists of the following st-tgds:
edge
(
x
,
y
)
∧
coloring
(
x
,
u
)
∧
coloring
(
y
,
u
)
→∃
v
error
(
v
)
,
coloring
(
x
,
y
)
→
color
(
y
)
.
As in the proof of
Theorem 19.3
, it is possible to prove that the composition of
M
12
and
M
23
can be used to encode the graph 3-coloring problem.
Consider now the SO tgds representing mappings
M
12
and
M
23
.Thatis,let
σ
12
be the
SO tgd given by the following rules:
node
(
x
)
→
coloring
(
x
,
f
(
x
))
,
edge
(
x
,
y
)
,
edge
(
x
,
y
)
→
which is equivalent to
Σ
12
,andlet
σ
23
be given by
edge
(
x
,
y
)
∧
coloring
(
x
,
u
)
∧
coloring
(
y
,
u
)
→
error
(
g
(
x
,
y
,
u
))
,
coloring
(
x
,
y
)
→
color
(
y
)
,
which is equivalent to
23
.
The algorithm essentially replaces relational atoms on the source side of
Σ
σ
23
with their
definitions according to
σ
12
only generates certain
kinds of tuples: for instance, in
coloring
(
x
,
f
(
x
)) the second coordinate is assumed to
be the result of applying
f
to the first coordinate. To take account of that, we include a
conjunction of equalities relating the tuple of variables of the replaced atom with the tuple
of terms in corresponding atom on the target side of
σ
12
. Some care is needed though, as
σ
12
. For instance,
coloring
(
x
,
u
) is
replaced with
node
(
x
)
x
=
x
∧
u
=
f
(
x
),and
edge
(
x
,
y
) is replaced by
edge
(
x
,
y
)
∧
∧
x
=
x
∧
y
=
y
. Note that for each atom we rename the variables in
σ
12
to avoid conflicts.
The following set of rules is obtained as a result of this process:
⎛
⎞
edge
(
x
,
y
)
x
=
x
∧
y
=
y
∧
∧
⎝
⎠
→
∧
node
(
x
)
x
=
x
∧
u
=
f
(
x
)
∧
∧
error
(
g
(
x
,
y
,
u
))
,
∧
node
(
y
)
y
=
y
∧
u
=
f
(
y
)
∧
node
(
x
)
x
=
x
∧
y
=
f
(
x
)
∧
→
color
(
y
)
.
The above set of rules is not yet an SO tgd as it does not satisfy condition (4) in the
definition of SO tgds: variables
x
,
y
,
u
originally used in the relational atoms on the source
side of
σ
23
are not used in relational atoms (on the source side) any more. As a final step,
the algorithm eliminates all such variables. This is achieved by replacing these variables by
the terms they are equal to according to the newly introduced equalities. More precisely,
in the first rule the equalities
x
=
x
,
y
=
y
and
u
=
f
(
x
) are removed and all occurrences
of
x
,
y
,
u
are replaced by
x
,
y
,
f
(
x
) respectively, and similarly in the second rule. The
first rule can be further simplified by eliminating variables
x
and
y
in the same way. The
