Information Technology Reference
In-Depth Information
r
=
q
0
˃
1
q
1
...˃
n
q
n
, is such that
q
i−
1
=
p
,
˃
i
=
˃
,
q
i
=
q
and
ʔ
(
p, ˃, q
)=
v
.
We do not prove the existence of such formulas in this paper, it is obtained
as a direct consequence of Buchi-Elgot-Trakhtenbrot's Theorem. Another direct
consequence of this theorem is the existence of an MSO formula
ˆ
dom(
T
)
which
defines the domain of
T
(which is a regular language).
We define formally
T
=(
k,ˆ
dom
,
(
ˆ
pos
)
1
≤c≤k
,
(
ˆ
c
L
σ
)
1
≤c≤k,˃∈ʣ
,
(
ˆ
c,d
)
1
≤c,d≤k
):
k
=
K
ˆ
dom
≡
ˆ
dom(
T
)
≡
{
ˆ
pos
(
x
)
ˆ
t
(
x
)
→|
v
|≥
c
|
t
:= (
p, ˃, v, q
) s.t.
ʔ
(
p, ˃, q
)=
v
}
≡
{
ˆ
c
L
σ
(
x
)
ˆ
t
(
x
)
→
(
c
≤|
v
|∧
v
(
c
)=
˃
)
|
t
:= (
p, ˃, v, q
) s.t.
ʔ
(
p, ˃, q
)=
v
}
ˆ
c,d
(
x, y
)
≡
(
x
=
y
∧
c
≤
d
)
∨
x
≺
y
where the subformulas
|v|≥c
,
c ≤|v|∧v
(
c
)=
˃
and
c ≤ d
(which do not
actually belong to MSO syntax) are either defined by
or
↥
depending on
whether the Boolean expressions they represent hold true or not. Finally, note
that
T
is indeed order-preserving since clearly, if
u
=
ˆ
c,d
j
.
Conversely
, given an order-preserving MSO-transducer
T
, one shows how
to construct an equivalent NFT
T
. We start by a first observation. Let
u
=
˃
1
...˃
n
∈
|
(
i,j
), then
i
≤
(
u
). Since
T
is order-preserving, there is no
backward edges in the output word structures produced by
T
. Therefore the
word
v
can be decomposed into
v
1
...v
n
such that each word
v
i
is the subword
of
v
induced by the non-filtered copies of the input position
i
, i.e. the set
N
i
=
{
dom(
T
)and
v
=
T
i
1
,...,i
k
i
j
=
ˆ
pos
(
i
)
. It can be seen on Fig. 6: each vertical block of
the output structure correspond to a partial output word, and the result output
word of the transformation is obtained by concatenating, in order, these partial
words. Let
ʣ
k
be all the words over
ʣ
of length at most
k
. For all
w
}∩{
|
u
|
}
ʣ
k
,one
∈
can define an MSO formula
Ψ
w
(
x
) such that
u
dom(
T
) implies
that
w
=
v
i
,where
v
i
is defined by the decomposition explained before. Note
that the definition of order-preservation does not require that copies are ordered
according to
|
=
Ψ
w
(
i
)iff
u
∈
(on integers), i.e., whenever formula
ˆ
c,d
≤
(
x, y
) holds, it implies
that
x
d
, unlike the example of Fig. 6. In other words,
it could be that the first position of
v
i
corresponds to node
i
2
while the second
position corresponds to node
i
1
of the output structure. Therefore, in order to
define
Ψ
w
(
x
), one has to quantify, by a huge disjunction, over possible orders over
these copies. Formally, for all tuples
t
=(
j
1
,...,j
|w|
) such that
j
∈{
y
, but not necessarily
c
≤
1
,...,k
}
for all
, we define an
intermediate formula
Ψ
(
j
1
,...,j
|w|
w
(
x
) which holds true whenever the
x
-th partial
output word is
w
, and each position of
w
correspond to nodes
x
j
. Then,
Ψ
w
(
x
)
is obtained as the disjunction of the formulas
Ψ
(
j
1
,...,j
|w|
)
∈{
1
,...,
|
w
|}
,and
j
1
=
j
2
for all
1
=
2
∈{
1
,...,
|
w
|}
(
x
) for all tuples:
w
=1
|w|
ˆ
pos
(
x
)
|w|−
1
ˆ
j
L
w
(
)
ˆ
j
,j
+1
Ψ
w
(
x
)
ˆ
j
pos
(
x
)
≡
∧
(
x
)
∧
¬
(
x, x
)
=1
j∈{
1
,...,k}\{j
1
,...,j
|w|
}
≡
{
Ψ
w
(
x
)
}
|w|
,j
1
Ψ
w
(
x
)
|
t
=(
j
1
,...,j
|w|
)
∈{
1
,...,k
=
j
2
,
∀
1
=
2
}
