Information Technology Reference
In-Depth Information
( T ) is indeed a monoid with matrix multiplication and M as
neutral element ( M is equal to the identity matrix on Q
M
Note that
×X
). Moreover, the
mapping w
M w is a morphism, as it can be shown that M w 1 w 2 =
M w 1 M w 2 for all w 1 ,w 2
ʣ
ʣ [26].
Classes of transition monoids. We define several classes of transition monoids.
The transition monoid
M
( T ) of an SST T is copyless if for all M
∈M
( T ),
M is
{↥
, 0 , 1
}
-valued, and every row M [ q,U ][ . ] contains at most one 1, for all
q
.Inotherwords, U can be copied in at most one other
register (included itself). The monoid
Q and U
∈X
M
( T )is restricted copy if all M
∈M
( T )
is
-valued. In other words, a register can be copied more than once, but
these copies must not be combined later on. Finally, we will also consider SST
whose transition monoid is finite . The registers with a finite transition monoid
can be copied, but not on loops. Note that any copyless transition monoid is
restricted copy, and any restricted copy transition monoid is finite. It has been
shown, as we will see, that the corresponding classes of SST are, however, of
equal expressive power.
Several restrictions on register updates that have been defined in several pa-
pers, with ad-hoc definitions, are nicely captured by these simple classes of tran-
sition monoids. The copyless restriction of [2] corresponds to SST with copyless
transition monoid. The restricted copy restriction of [6] corresponds to SST with
restricted copy transition monoids. Finally, the bounded copy restriction of [3]
corresponds to SST with finite transition monoid.
{↥
, 0 , 1
}
5 Automata-Logic Connections for Word Transformations
In this section, we present the main known automata-logic connections for word
transformations.
5.1 MSO Transformations
The first automata-logic connection for word transformations has been discov-
ered by J. Engelfriet and H.J. Hoogeboom [21]:
Theorem 1 (J. Engelfriet, H.J. Hoogeboom [21]). Let f : ʣ
ʣ .The
function f is MSOT-definable iff it is 2FST-definable.
2FST is based on intermediate models of 2FST which
can perform “MSO jumps” ˆ ( x, y ), where ˆ ( x, y ) is an MSO formula that defines
a function from x positions to y positions. Intuitively, the machine can move from
position x to position y providing ˆ ( x, y ) holds true. 2FST with MSO jumps are
then converted, based on Buchi-Elgot-Trakhtenbrot's theorem, into 2FST with
regular look-around. These 2FST can move only to positions which are in the 1-
neighbourhood of the current position, but their move can be based on a regular
property of the current prefix and sux of the word. Finally, it is shown that
2FST with regular look-around are equivalent to 2FST.
The proof of MSOT
 
Search WWH ::




Custom Search