Information Technology Reference
In-Depth Information
Formally, a
two-way finite state transducer (2FST)
over an alphabet
ʣ
is
a tuple
T
=(
Q,q
0
,ʴ,ʴ
halt
)where
Q
is a finite set of states,
q
0
∈
Q
is the
initial state, and
ʴ
is the transition relation
3
,oftype
ʴ
:
Q
×
(
ʣ
∪{
,
}
→
Q
×
)
{
+1
,
−
1
}×
ʣ
∗
, such that
ʴ
(
q,
)
∈
Q
×{
+1
}×
ʣ
∗
,and
ʴ
(
q,
)
∈
Q
×{−
1
}×
ʣ
∗
,for
all
q
∈
Q
. Finally,
ʴ
halt
is the halting function, of type
ʴ
halt
:
Q
×
(
ʣ
∪{
,
}
)
→
ʣ
∗
. In order to ensure determinism, it is required that dom(
ʴ
)
∩
dom(
ʴ
halt
)=
∅
.
ʣ
∗
is evaluated by
T
, it is convenient to see
In order to see how a word
u
∈
the input as a tape containing
u
. Initially the head of
T
is on the first cell in
state
q
0
(the cell labelled
). When
T
reads an input symbol, depending on the
transitions in
ʴ
, its head moves to the left (
1) if the head was not in the first
cell, or to the right (+1) if the head was not in the last cell, then it updates its
state, and appends a partial output word to the final output.
T
stops as soon
as it can apply the halting transition
ʴ
halt
, and produces a last partial output
word.
A
configuration
of
T
is a pair (
q,i
)
−
where
q
is a state and
i
is a
position on the input tape. A
run r
of
T
is a finite sequence of configurations.
Let
u
=
˃
1
...˃
n
∈
∈
Q
×
N
ʣ
∗
,let
˃
0
=
.Arun
r
=(
p
1
,i
0
)
...
(
p
m
,i
m
)
is
accepting on u
if (
i
)
p
1
=
q
0
,
i
0
=0;(
ii
)
ʴ
halt
(
p
m
,˃
i
m
) is defined and equal
to
v
m
for some
v
m
∈
and let
˃
n
+1
=
ʣ
∗
;(
iii
) for all
k
∈{
0
,...,m
−
1
}
,
ʴ
(
p
k
,˃
i
k
) is defined
ʣ
∗
.The
output
of
r
is defined
by
O
(
r
)=
v
1
...v
m
. Like FST, the (functional) transformation defined by
T
,
denoted by
and equal to (
p
k
+1
,i
k
+1
−
i
k
,v
k
)forsome
v
k
∈
,isthesetofpairs(
u,v
) such that there exists an accepting run
r
of
T
on
u
such that
O
(
r
)=
v
.
T
Example 5.
Unlike FST, 2FST can define the functions
f
copy
and
f
rev
,asshown
in Fig. 3. Therefore, there are strictly more expressive than FST. However, check-
ing whether a 2FST is equivalent to some FST is decidable [25]. 2FST define
linear-size increase transformations, because it can be proved that due to de-
terminism, the number of times an input position can be visited is in
O
(
|
Q
|
).
Therefore,
f
exp
is not 2FST-definable.
4.3 Streaming String Transducers
Recently, an appealing transducer model for word transformations, whose expres-
siveness is exactly the same as 2FST, has been proposed in [2], as an extension
of FST with registers, called
streaming string transducers (SST)
. Partial output
words are stored in a fixed number of registers that can be concurrently updated
and combined in different ways to define the output word. Moreover, SST are de-
terministic and, unlike 2FST, are one-way (left-to-right), making them easier to
manipulate algorithmically. It is has been applied, for instance, to the automatic
verification of some important classes of list-processing programs [1].
3
In the literature, some definitions also include stay transition, i.e. transitions where
the input head does not move. In the deterministic case, these transitions can how-
ever be removed without loss of expressiveness.
