Information Technology Reference
In-Depth Information
•
a
n/
2
,one
takes one copy of the input domain, sets the domain formula to
ˆ
dom
≡∀
To define with an MSO-transducer the transformation
f
1
/
2
:
a
n
→
L
a
(
x
),
and filters out all odd positions of the input word, which is possible by the MSO
formula
ˆ
pos
(
x
)
x
·
X
e
,where
ˆ
o/e
has been defined
in Example 2. Finally, the order relation is just defined by
ˆ
1
,
1
≡∃
X
o
∃
X
e
·
ˆ
o/e
(
X
o
,X
e
)
∧
x
∈
(
x, y
)
≡
x
y
.
a
2
n
is not MSOT-definable, because it is not
linear-size increase, while MSOT-definable transformations are, by Remark 1.
•
The transformation
f
exp
:
a
n
→
Remark 2.
Let us mention an other, logic-based, transformation formalism,
called
first-order translations
, that has been introduced by N. Immerman in
[30], as a way to define reductions between problems. In first-order translations,
the domain of the output structure is a set of
k
-tuples of elements of the input
domain, for some
k
. It is defined by a first-order formula with
k
free variables.
Predicates of arity
n
of the output structure are defined, similarly to Courcelle's
logical transducers, by formulas with
kn
free variables, interpreted over the in-
put structure. In contrast to logical transducers which are linear-size increase,
first-order translations can map a structure to a polynomially larger output
structure. First-order translations have been introduced as a logical way to de-
fine reductions between decision problems and nothing is known about their
expressiveness as a formalism to define transformations. In this paper, we rather
focus on (Courcelle) logical transducers, for which connections with state-based
formalisms have been established. Nevertheless, let us mention the two papers
[32] and [34], where the particular case of length-preserving FO-translations with
k
= 1 has been studied, as well as their connections with finite state transducers.
See Section 5.2 for more details.
4 State-Based Models for Word Transformations
In this section, we introduce some of the main state-based models for defining
(finite) word transformations for which connections with logics are known. These
models are automata models extended with outputs, and are usually called
trans-
ducers
. We present three models: finite state transducers, two-way finite state
transducers, and streaming string transducers.
4.1 Finite State Transducers
Finite state transducers
(FST) extend finite state automata with partial output
words on their transitions. Whenever an FST reads an input letter, it moves
deterministically to the next state and appends a word to the output tape.
Formally, an FST on an alphabet
ʣ
is a tuple
T
=(
Q,q
0
,F,ʴ
) such that
Q
is a
finite set of states,
q
0
∈
Q
is the initial state,
F
ↆ
Q
is a set of accepting states,
ʣ
∗
is the transition function.
A
run
of
T
is a sequence
r
=
p
0
˃
1
p
1
...˃
n
p
n
∈
and
ʴ
:
Q
×
ʣ
→
Q
×
(
Qʣ
)
∗
Q
such that
p
0
=
q
0
ʣ
∗
such that
ʴ
(
p
i−
1
,˃
i
)=(
p
i
,v
i
).
and for all
i
∈{
1
,...,n
}
,thereexists
v
i
∈
ʣ
∗
,onesaysthat
r
is a
run on u
if
u
=
˃
1
...˃
n
. The output of
r
,
Given
u
∈
