Database Reference
In-Depth Information
chine halts. The source DTD
D
s
over the alphabet
{
r
,
I
1
,
I
2
,...,
I
f
,
R
,
}
is given by
r
→
I
1
R
I
i
→
I
j
for all
i
such that
I
i
=(
r
,
j
)
I
i
→
I
j
|
I
k
for all
i
such that
I
i
=(
r
,
j
,
k
)
R
→
R
|
I
f
,
→
ε
where each
I
i
has two attributes corresponding to the values of the registers, and
R
has one
attribute.
The target DTD
D
t
is simply
.
As mentioned above, the sequence of
R
's is meant to be that of natural numbers, but what
represents a number is the depth in the tree instead of a value itself. In other words, the
data values are used as indices, so they must be unique. This is enforced by the following
dependency
{
r
→
ε
}
r
//
R
(
x
)
//
R
(
x
)
−→ ⊥
.
Let us now deal with the left branch, which is meant to encode the run itself. We have
assumed that the initial configuration is (1
,
0
,
0); the constraints below exclude other situ-
ations
r
[
I
1
(
x
,
y
)
,//
R
/
R
(
x
)]
−→ ⊥
r
[
I
1
(
x
,
y
)
,//
R
/
R
(
y
)]
−→ ⊥
.
Now, let us check that we proceed correctly. For each
i
such that
I
i
=(
r
1
,
j
), we need to
enforce that there is a number in the
R
-branch to set the value of
r
1
to, and that the next
configuration is indeed obtained by increasing
r
1
r
[
//
I
i
(
x
,
y
)
,//
R
(
x
)
/
]
−→ ⊥
r
[
//
I
i
(
x
,
y
)
/
I
j
(
x
,
y
)
,//
R
(
x
)
/
R
(
x
)]
x
=
x
,
y
=
y
.
−→
For each
i
such that
I
i
=(
r
1
,
j
,
k
), we need to say: if the next state is
k
,then
r
1
stores 0, and
both registers stay the same; if the next state is
j
,then
r
1
does not store 0, the register
r
1
gets decreased, and
r
2
stays the same
r
[
//
I
i
(
x
,
y
)
/
I
k
(
x
,
y
)
,
R
(
x
)]
x
=
x
,
x
=
x
,
y
=
y
−→
r
[
//
I
i
(
x
,
y
)
/
I
j
,
R
(
x
)]
−→ ⊥
r
[
//
I
i
(
x
,
y
)
/
I
j
(
x
,
y
)
,//
R
(
x
)
/
R
(
x
)]
x
=
x
,
y
=
y
.
−→
For each
i
such that
I
i
=(
r
2
,
j
) or
I
i
=(
r
2
,
j
,
k
) we add analogous st-tgds.
Finally, we have to make sure that we end properly. In each source tree, the left branch
must end with
I
f
, so we do not need to check that. It is enough to say that both registers
