Information Technology Reference
In-Depth Information
such that
ˆ
˃
m
(
x
)=
˃<˃
m
¬
ˆ
˃
(
x
), where
˃
m
is the maximal element of
ʣ
.
Then, for all
w
∈
ʣ
∗
of length
n
,
T
(
w
)=
˃
1
...˃
n
such that for all
i
∈{
1
,...,n
}
,
∧
˃<˃
i
¬
w
ˆ
˃
(
i
). Note that
T
defines a total and length-preserving
function, which is actually definable by a one-copy (Courcelle) FO-transducer.
It is shown in [32] that a function is definable by an FO-translation in one-free
variable iff it is definable by an aperiodic NFT, where aperiodic NFT are the
NFT whose underlying automata is aperiodic (i.e. they have aperiodic transition
monoid). This result was later on, in [34], generalised to
V
-translations and NFT
whose transition monoid is in
V
,where
V
is a pseudovariety of (finite) monoids
(for instance, the pseudovariety of finite aperiodic monoids).
|
=
ˆ
˃
i
(
i
)
5.3 Order-Preserving MSO Transducers
An MSO-transducer
T
with
k
copies is
order-preserving
if for all words
w
∈
=
ˆ
c,d
dom(
T
), all positions
i,j
∈
dom(
w
), and copies
c, d
∈{
1
,...,k
}
,if
w
|
(
i,j
),
then
i
j
holds true. Note that this can be syntactically ensured by requiring
that formulas
ˆ
c,d
ˆ
. We show in Theorem 4 that
order-preserving MSO-transducers characterise exactly the NFT-definable func-
tions. This theorem can also be obtained as a consequence of a result shown
in [9] for order-preserving transformations with origin semantics. However, we
give here a direct proof, which illustrates the techniques that are usually used
to derive automata-logic connections. Origin semantics is discussed later in Sec-
tion 5.4.
(
x, y
) are of the form
x
y
∧
Theorem 4.
Afunctionf
:
ʣ
∗
→
ʣ
∗
is NFT-definable iff it is definable by an
order-preserving MSO-transducer.
Proof.
We first show the “only if” direction. Let
T
=(
Q,q
0
,F,ʔ
)beanNFT
over
ʣ
that defines a
f
. We construct an order-preserving MSO-transducer
T
such that
T
=
T
=
f
.Since
T
defines a function, it is known that
T
is
equivalent to an unambiguous NFT [31], i.e. an NFT such that there exists at
most one accepting run on every input word. Therefore, we assume that
T
is
unambiguous.
Let
K
be the maximal length of the words occurring on the transitions of
T
, i.e.
K
=max
∈
N
{|
w
||∃
p, q
∈
Q
∃
˃
∈
ʣ, ʔ
(
p, ˃, q
)=
w
}
. Clearly, for all words
u
by an MSO-transducer,
one needs to take
K
copies of the input structure. Let us intuitively explain how
these copies will be used. Let
u
=
˃
1
...˃
n
∈
∈
dom(
T
),
|
T
(
u
)
|≤
K.
|
u
|
. In order to define
T
dom(
T
)and
r
=
q
0
˃
1
q
1
...˃
n
q
n
be
the
accepting run of
T
on
u
, and let
O
(
r
)=
v
1
...v
n
, where each word
v
i
is
produced by the
i
-th transition of
r
.Everyposition
j
dom(
v
i
) will be encoded
by the
j
-th copy of the input position
i
, i.e., by the node
i
j
.Ofcourse,the
j
-th
copy exists since
∈
K
, one needs to filter
out all nodes
i
j
, by the formula
ˆ
pos
(
x
). The encoding is illustrated on Fig. 6.
The definition of
T
relies on the existence of MSO formulas
ˆ
t
(
x
), for all
tuples
t
=(
p, ˃, v, q
)
|
v
i
|≤
K
. For all
j
such that
|
v
i
|
<j
≤
ʣ
∗
×
ʣ
∗
and
∈
Q
×
ʣ
×
Q
, such that for all words
u
∈
all positions
i
∈
dom(
u
),
u
|
=
ˆ
t
(
i
)iff
u
∈
dom(
T
) and the run of
T
on
u
,say
