Database Reference
In-Depth Information
In order to simulate transitions of
A
we need to include two tgds in
Σ
t
. These are defined
as:
ϕ
left
(
t
,
q
,
q
,
a
,
a
,
p
,
p
)
t
ψ
(
t
,
t
,
q
,
a
,
a
,
p
,
p
)
→∃
ϕ
right
(
t
,
q
,
q
,
a
,
a
,
p
,
p
)
t
ψ
(
t
,
t
,
q
,
a
,
a
,
p
,
p
)
,
→∃
where the formula
ϕ
left
is defined as:
ˆ
ˆ
Positions
(
t
,
p
,
p
)
(
q
,
a
,
q
,
a
,
d
)
Config
(
t
,
q
,
p
)
∧
Symbols
(
t
,
a
,
p
)
∧
∧
Δ
∧
Left
(
d
)
,
the formula
ϕ
right
is defined as:
ˆ
ˆ
Positions
(
t
,
p
,
p
)
(
q
,
a
,
q
,
a
,
d
)
Config
(
t
,
q
,
p
)
∧
Symbols
(
t
,
a
,
p
)
∧
∧
Δ
∧
Right
(
d
)
,
and the formula
ψ
is defined as:
Steps
(
t
,
t
)
Config
(
t
,
q
,
p
)
Symbols
(
t
,
a
,
p
)
∧
∧
∧
LeftCopy
(
t
,
t
,
p
)
RightCopy
(
t
,
t
,
p
)
.
∧
Intuitively,
ϕ
right
) states that a transition from the configuration
c
t
in step
t
to its
successor configuration
c
t
in step
t
is possible by moving the head of the Turing machine
to the left (resp. right). On the other hand,
ϕ
left
(resp.
populates the initial part of configuration
c
t
and establishes the link between the configurations
c
t
and
c
t
.
Afterwards, we need to extend
ψ
t
with two new tgds that check that if
c
t
and
c
t
are
successor configurations then they coincide in all unmodified positions:
Σ
1.
LeftCopy
(
t
,
t
,
p
)
Positions
(
t
,
p
,
p
)
Symbols
(
t
,
a
,
p
)
∧
∧
→
LeftCopy
(
t
,
t
,
p
)
Positions
(
t
,
p
,
p
)
Symbols
(
t
,
a
,
p
)
.
∧
∧
2.
RightCopy
(
t
,
t
,
p
)
Positions
(
t
,
p
,
p
)
Symbols
(
t
,
a
,
p
)
∧
∧
→
RightCopy
(
t
,
t
,
p
)
Positions
(
t
,
p
,
p
)
Symbols
(
t
,
a
,
p
)
.
∧
∧
Notice that these tgds also check that the positions from
c
t
occur in the same order in
c
t
.
Finally, we extend
Σ
t
with the tgd:
Steps
(
t
,
t
)
ˆ
∧
End
(
t
,
p
)
∧
Blank
(
x
)
→
p
Positions
(
t
,
p
,
p
)
End
(
t
,
p
)
.
Symbols
(
t
,
x
,
p
)
∃
∧
∧
This tgd extends
c
t
with a new position at the right-end of the tape, puts the blank symbol
in it, and declares it to be the last relevant position for
c
t
.
Let
M
=(R
s
,
R
t
,
Σ
st
,
Σ
t
),whereR
s
, R
t
,
Σ
st
and
Σ
t
are as defined above. We show that
A
.Inorder
to prove this, we use the following claim that directly relates source instance
S
(
halts on the empty input if and only if
S
(
A
) has a universal solution under
M
A
) with
target instance
T
(
A
,
c
), assuming that
c
is a computation of
A
.
Claim 6.6
For every computation c
=(
c
0
,...,
c
n
)
of
A
it is the case that T
(
A
,
c
)
is the
result of some finite chase sequence for S
(
A
)
under
M
.
