Information Technology Reference
In-Depth Information
6.2 Infinite Word Transformations
An
ˉ-word
over
ʣ
is a mapping
w
:
ʣ
.The
i
-th letter of
w
is
w
(
i
).
An infinite words
w
over
ʣ
is either a finite word or an
ˉ
-word. The set of
ˉ
-words over
ʣ
is denoted by
ʣ
ˉ
, and the set of infinite words by
ʣ
∞
.Note
that
ʣ
∞
=
ʣ
∗
∪
N
→
ʣ
ˉ
. A transformation
R
of infinite words over
ʣ
is a binary
relation from
ʣ
ˉ
to
ʣ
∞
(we assume indeed in this section that the input word
is an
ˉ
-word).
MSO-transducers can naturally be generalised to define functional infinite
word transformations, by seeing an
ˉ
-word as a structure over
S
ʣ
whose domain
is
. For an MSO-transducer
T
to be an MSO-transducer of infinite words, we
require that for all input words
u
N
ʣ
ˉ
, the image
(
u
) is a structure that
corresponds to an infinite word. Although it is a semantical restriction, it is
decidable, similarly as in the proof of Proposition 1.
As an example, consider the transformation
f
ˉ
:
ʣ
ˉ
∈
T
ʣ
ˉ
,where
ʣ
=
→
{
a, b
}
,
that maps any input word of the form
uab
ˉ
to
a
|u|
b
ˉ
,where
u
ʣ
∗
.Itis
definable by the following MSO-transducer with one copy and
ˆ
dom
≡∃
∈
x
·
L
a
(
x
),
ˆ
a
(
x
)
ˆ
1
,
1
ˆ
pos
(
x
)
ˆ
a
(
x
)
L
a
(
y
)
ˆ
b
(
x
)
≡
≡∃
y
x
·
≡¬
(
x, y
)
≡
x
y
(Deterministic) 2FST can be extended to define functional infinite word trans-
formations, by using for instance a Muller acceptance condition (they are called
ˉ
-2FST). However, they cannot even define
f
ˉ
, because they can never decide
locally whether a
b
letter should be transformed into an
a
letterorkeptun-
changed, because it depends on the existence of an
a
letter in the future. They
could use the two-wayness as a kind of look-ahead to check the existence of
such an
a
, but they cannot come back exactly to the position they were coming
from, because they get lost, due to the finite state device. One therefore needs
to extend
ˉ
-2FST with regular look-ahead: each transition of an
ˉ
-2FST with
regular look-ahead is extended with a finite state automaton over
ˉ
-words that
checks a property of the (infinite) sux. Such transition can be triggered only if
the sux belong to the look-ahead automaton. It should be clear that
ˉ
-2FST
with regular look-ahead strictly extend the expressive power of
ˉ
-2FST.
SST have been extended to define functional infinite word transformations,
with a Muller accepting condition (called
ˉ
-SST). They run on
ˉ
-words in a
deterministic way, and the (partial) output function
O
has type 2
Q
→X
∗
.
Given a run
r
over an
ˉ
-word
u
,let
P
the set of states visited infinitely many
times in
r
. The output of
r
is defined only if
O
(
P
) is defined, as the limit of the
sequence of finite words
s
s
r,i
(
O
(
P
)) for
i
(remind that
s
and
s
r,i
have
been defined in Section 4.3). In order to ensure the existence of that limit (and
to make sure that this limit is an infinite word), syntactic restrictions are put
on the SST: if
P
→∞
dom(
O
)and
O
(
P
)=
U
1
...U
n
, it is required that on the
connected component induced by
P
in
T
,theregisters
U
1
,...,U
n−
1
are never
modified, and the register
U
n
can only be modified by appending something (i.e.
updates are of the form
U
n
:=
U
n
ʱ
for some
ʱ
∈
)
∗
). The transition
∈
(
ʣ
∪X
monoid of an
ˉ
-SST is defined similarly as SST.
