Information Technology Reference
In-Depth Information
is a function. Although transformations are as fundamental as languages, much
less is known on the relation between automata and logic for transformations.
Nevertheless, some important results have been obtained in the last decade. In
this paper, we survey some of them.
A transformation
R
of finite words over an alphabet
ʣ
can be seen as a lan-
guage, for instance the language
ʣ
. However,
the formalisms from language theory, such as automata, are not well-suited to
describe transformations defined on this encoding and therefore, proper exten-
sions have been introduced to define transformations. Automata have been for
instance extended to
automata with outputs
, usually called
transducers
. Perhaps
the most studied transducer model is that of
finite state transducers
[31,37].
Finite state transducers (FST) extend finite state automata with an output
mechanism. Whenever an FST reads an input symbol, it moves to the next
symbol, updates its internal state, and write a partial output word. The final
output word is the concatenation, taken in order, of all the partial output words
produced while processing the whole input word.
The expressiveness of FST is limited and other, more powerful, state-based
models have been introduced and studied, such as two-way transducers and more
recently, streaming string transducers [2]. On the logic side, monadic-second or-
der logic has been extended in a natural way to
MSO-transducers
by B. Cour-
celle, to define transformations of logical structures [14,15]. The predicates of
the output structure are defined by MSO formulas interpreted over a fixed num-
ber of copies of the input structure. The first automata-logic connection, or one
should say transducer-logic connection, has been shown in [21] by J. Engelfriet
and H.J. Hoogeboom. They have extended Buchi-Elgot-Trakhtenbrot's theorem
to functional transformations by showing that any transformation definable by a
deterministic two-way finite state transducer is definable by an MSO-transducer
(interpreted over finite words), and conversely. Moreover, this correspondence is
effective, i.e., an MSO-transducer can be effectively constructed from a determin-
istic two-way finite state transducer and conversely. An important consequence
of this result is the decidability of equivalence of MSO-transducers, since the
equivalence problem for deterministic two-way transducers is decidable [16].
Since then, other transducer-logic connections have been established for fi-
nite word transformations and other structures such as infinite words and finite
trees. Functional MSO-transformations of finite words have been shown to cor-
respond to transformations definable by streaming string transducers [2], and
this result has been extended to infinite words [3] and to non-functional MSO-
transformations [21,5]. Engelfriet-Hoogeboom's theorem has been extended to
finite trees [8,22,23]. First-order definable transformations of finite words have
been considered in [26] and [32]. Some of these connections have been considered
under a stronger semantics, the origin semantics, in [9].
This paper surveys some of these important results. All the transducer-logic
connections presented in this paper are effective. The setting of functional trans-
formations of finite words is presented in details, in contrast to the other results,
which come nevertheless with the main bibliographic references. In Section 2, we
{
u
#
v
|
(
u,v
)
∈
R
}
,where#
∈
