Information Technology Reference
In-Depth Information
In other words, for all
u
=
Ψ
w
(
i
)iff
w
is the
i
-the subword
of the output of
u
. This formula is of particular interest if we want to define
an NFT, because it tells us exactly what partial output word must be produced
while reading the
i
-th input letter.
The rest of the proof explains how one can construct an automaton
A
on the
alphabet
ʓ
=
ʣ
∈
dom(
T
), we have
u
|
ʣ
k
which accepts all words (
˃
1
,v
1
)
...
(
˃
n
,v
n
)
ʓ
∗
such that
×
∈
for all
i
=
Ψ
v
i
(
i
). The
final NFT
T
is obtained from this automaton
A
by replacing every transition
(
q,
(
˃, v
)
,p
)of
A
by the transition
q
˃|v
∈{
1
,...,n
}
,
v
i
is the (unique) word such that
˃
1
...˃
n
|
p
of
T
. Clearly,
T
is equivalent to
T
.
In order to construct
A
, we again apply Buchi-Elgot-Trakhtenbrot's theorem,
since the language of
A
is MSO-definable, by the sentence (on
−−→
S
ʓ
)
ˆ
A
≡
[
ˆ
dom
]
ʓ
∧∀
x
·
L
(
˃,v
)
(
x
)
→
[
Ψ
v
(
x
)]
ʓ
(
˃,v
)
∈ʓ
where [
ˆ
dom
]
ʓ
(resp. [
Ψ
v
(
x
)]
ʓ
) is obtained from
ˆ
dom
(resp.
Ψ
v
(
x
)), which is on
the signature
S
ʣ
, by replacing every atom
L
ʲ
(
y
)by
w∈ʣ
k
L
(
ʲ,w
)
(
y
). Clearly,
aword
s
=(
˃
1
,v
1
)
...
(
˃
n
,v
n
)over
ʣ
ʣ
k
satisfies [
ˆ
dom
]
ʓ
iff
u
=
˃
1
...˃
n
|
×
=
ˆ
dom
. Similarly,
s
|
=
Ψ
v
(
i
)]
ʓ
iff
u
|
=
Ψ
v
(
i
), and therefore the correctness
follows.
Again, the power of transducer-logic connections is illustrated by the follow-
ing definability problem. It is decidable whether a deterministic two-way finite
state transducer
T
is equivalent to a (one-way) functional finite state transducer
[25]. As a consequence of this result, the connection between 2FST and MSOT
(Theorem 1), and the previous theorem (Theorem 4), we obtain the following
corollary:
Corollary 1.
Given an MSO-transducer T, it is decidable whether T is equiva-
lent to some order-preserving MSO-transducer.
Proof.
It suces to translate
T
into a deterministic two-way transducer
T
,by
applying the (effective) encoding of Theorem 1, then to apply the procedure
of [25] which decides whether
T
is equivalent some NFT, and finally to apply
Theorem 4.
5.4 Transformations with Origin
One of the diculties in the theory of transducers is to deal with the asynchronic-
ity in the production of the output. For instance, two FST may not produce there
output letters at the same time when reading the same input position, but still,
they can be equivalent. This asynchronicity, which is implicitly present in the
Post correspondence problem (PCP), can even, in some cases, lead to undecid-
able problems. For instance, the equivalence problem of non-deterministic FST
is undecidable, and the undecidability proof is non surprisingly based on PCP
[28]. The asynchronicity between output words have been captured by a notion
