Information Technology Reference
In-Depth Information
⃒
MSOT, is shown by first constructing an MSOT that
takes as input a word structure, and output an edge-labeled graph (edges are
labelled by words of bounded length) whose nodes are exactly the configurations
(
q,i
) in which the 2FST is successively (where
q
is a state and
i
a position in the
input word). This MSOT is then composed with an MSOT that transforms an
edge-labeled graph into a node-labeled graph (nodes are here labelled with letters
from
ʣ
). The result follows as MSOT are closed under composition [15,14].
As we have seen in Fig. 4, SST can define functions which are exponential-
size increase (
f
exp
), and therefore, not MSOT-definable. However, any MSOT-
definable transformation is SST-definable, and, by weakening the expressiveness
of SST, it is possible to capture exactly MSOT:
The converse, 2FST
Theorem 2 (R. Alur, P. Cerny [2], R. Alur, E. Filiot, A. Trivedi [3]).
Let f
:
ʣ
∗
→
ʣ
∗
. The following statements are equivalent:
1. f is MSOT-definable.
2. f is definable by an SST with copyless transition monoid.
3. f is definable by an SST with finite transition monoid.
⃒
(2)
of [2] goes through the intermediate model of 2FST and relies on Theorem 1.
More precisely, it is shown that any 2FST can be encoded as an SST, by ex-
tending to transducers the classical Sheperdson's construction that transforms
a two-way finite automaton as a (one-way) finite automaton [39]. The resulting
SST may not be necessarily copyless, and the main challenge is to show that it
can be converted into a copyless SST. Conversely, it is shown how to directly
encode an SST as an MSO-transducer. In [3], it has been shown that SST with
finite transition monoid (called bounded copy) are equivalent to SST with copy-
less transition monoid. Although the proof of (1)
The equivalence between (1) and (2) was shown in [2]. The proof of (1)
(2) in [2] relies on 2FST,
a direct construction was also given in [6], in which the states of the SST are
MSO-types of bounded quantifier rank.
⃒
5.2 FO Transformations
Recall that first-order transformations are transformations definable by FO-
transducers, which are defined as MSO-transducers, except that only first-order
formulas can be used. In automata theory for languages, first-order definable
languages are captured by
aperiodic automata
, i.e. finite automata whose transi-
tion monoid is aperiodic [40,18]. A survey on first-order definable languages can
be found in [18]. A monoid (
M,
·
,e
) (with operator
·
and neutral element
e
)is
M
,
m
k
=
m
k
+1
. Recall that
the language (
aa
)
∗
is not FO-definable, while the language (
ab
)
∗
is.
As we have seen, the functions
f
del
,
f
double
,
f
copy
,and
f
rev
are FOT-definable.
However, the function
f
1
/
2
is not FOT-definable [26], although its domain,
a
∗
, is. So clearly, the FOT-definability of a function not only depends on the
FO-definability of its domain. It can be seen on an example. In Fig. 5(a),
the transition monoid of the underlying automaton of the SST defining
f
1
/
2
aperiodic
if there exists
k
∈
N
such that for all
m
∈
