Database Reference
In-Depth Information
•
The interpretation of
Config
contains the information about the state and the position of
the head in each configuration; namely,
Config
T
(
A ,
c
)
=
{
(
u
j
,
q
j
,
v
i
j
)
|
0
≤
j
≤
n
}
.
•
Finally, the interpretation of
Symbols
contains the information about the symbol
present at each position that is relevant for a configuration; namely,
Symbols
T
(
A ,
c
)
=
{
(
u
j
,
a
j
,
,
v
)
|
0
≤
j
≤
n
,
0
≤
≤
j
+1
}
.
Our goal is to construct a set
Σ
st
∪
Σ
t
of (st)-tgds that check whether
c
is a halting
computation of
A
. However, in order to be able to do that we need to enhance the target
ˆ
ˆ
instance
T
(
A
,
c
) with new relations. We extend R
t
with new relation symbols
Left
,
Right
,
Blank
,
ˆ
ˆ
ˆ
ˆ
Blank
are unary,
ˆ
ˆ
is 5-ary,
LeftCopy
and
RightCopy
are ternary, and
End
is binary - and interpret them as follows:
Δ
,
LeftCopy
,
RightCopy
and
End
- such that
Left
,
Right
,
Δ
Left
T
(
A ,
c
)
,
Blank
T
(
A ,
c
)
are simply copies of
Left
S
(
A
)
,
Right
S
(
A
)
and
Blank
S
(
A
)
, respectively. That is,
Right
T
(
A ,
c
)
and
ˆ
ˆ
ˆ
•
Left
T
(
A ,
c
)
contains only the direction
left
,
Right
T
(
A ,
c
)
ˆ
ˆ
Blank
T
(
A ,
c
)
contains only the symbol #.
ˆ
contains only the direction
right
, and, finally,
ˆ
)
,thatis,
ˆ
T
(
A
,
c
)
S
(
A
T
(
A
,
c
)
encodes the transition graph of
•
Δ
is simply a copy of
Δ
Δ
δ
.
LeftCopy
T
(
A ,
c
)
•
, and will be used
to verify that configurations
c
j
and
c
j
+1
coincide in all positions that are strictly to the
left of position
i
j
.
is defined as
{
(
u
j
+1
,
u
j
,
v
)
|
0
≤
j
≤
n
−
1
,
0
≤
≤
i
j
}
RightCopy
T
(
A ,
c
)
•
, and will be
used to verify that configurations
c
j
and
c
j
+1
coincide in all positions that are strictly to
the right of position
i
j
.
is defined as
{
(
u
j
+1
,
u
j
,
v
)
|
0
≤
j
≤
n
−
1
,
i
j
≤
≤
j
+1
}
End
T
(
A ,
c
)
•
is defined as
{
(
u
j
,
v
j
+1
)
|
0
≤
j
≤
n
}
, and marks the last position that is rele-
vant for a configuration.
We are now ready to define
Σ
st
∪
Σ
t
. First of all,
Σ
st
contains the full st-tgds:
ˆ
Left
(
x
)
→
Left
(
x
)
ˆ
Right
(
x
)
→
Right
(
x
)
ˆ
Blank
(
x
)
→
Blank
(
x
)
ˆ
(
q
,
a
,
q
,
a
,
d
)
(
q
,
a
,
q
,
a
,
d
)
,
Δ
→
Δ
ˆ
ˆ
Blank
and
ˆ
ˆ
that simply “copy” tuples in
Left
,
Right
,
Blank
and
Left
,
Right
,
Δ
into
Δ
,re-
spectively. Second,
Σ
st
contains the full st-tgd:
Init
(
x
)
∧
Zero
(
y
)
∧
One
(
z
)
→
Config
(
y
,
x
,
y
)
∧
Blank
(
w
)
∧
Symbols
(
y
,
y
,
w
)
∧
Symbols
(
y
,
z
,
w
)
∧
Positions
(
y
,
y
,
z
)
∧
End
(
y
,
z
)
.
Notice that this st-tgd implies that any solution for
S
(
) must contain the tuples
Config
(0
,
q
0
,
0),
Symbols
(0
,
#
,
0),
Symbols
(0
,
#
,
1),
Positions
(0
,
0
,
1) and
End
(0
,
1),which
encode the initial configuration of
A
A
.
