Information Technology Reference
In-Depth Information
As an example, consider the
ˉ
-SST of Fig. 7 that defines transformation
f
ˉ
.It
can loop an arbitrary number of steps in state
q
0
while replacing all symbols by
a
, and storing the current output in register
U
. Non-deterministically, it guesses
the last occurrence of an input
a
symbol, and from that point on, never modifies
register
U
again, and always append
b
to register
V
. Register
U
is intended to
capture the word
a
|u|
in the definition of
f
ˉ
, while
V
captures
b
ˉ
. The output is
then
UV
, and it is defined only for the singleton
{
q
1
}
, which enforces that after
some time, only
b
symbols are read.
It has been shown in [3] that MSO-transducers of infinite words correspond ex-
actly to
ˉ
-2FST with regular look-ahead, to
ˉ
-SST with finite transition monoid,
and to
ˉ
-SST with copyless transition monoid.
6.3 Tree Transformations
We present a result that establishes a correspondence between MSO-transducers,
and a transducer model for functional transformations of finite ranked trees.
Recall that ranked trees are ordered trees over a ranked alphabet. Each symbol
f
of the alphabet has a rank denoted by
r
(
f
) and, if some node
ʱ
is labelled
f
, this node has exactly
r
(
f
) successor nodes, called the children of
ʱ
(see [13]
for a formal definition). We denote by
T
ʓ
the set of ranked trees over a ranked
alphabet
ʓ
, and a (ranked) tree transformation is a binary relation over
T
ʓ
.
Tree transducers and their connection with term rewriting systems have been
deeply studied, see for instance [27]. More recent results on tree transducers can
be found in [15]. Like words, ranked trees over
ʓ
can be seen as logical structures
over the signature
,where
n
is the maximum arity in
ʓ
,
S
i
are binary successor predicates interpreted by pairs of nodes (
ʱ, ʲ
)such
that
ʲ
is the
i
-th child of
ʱ
,and
L
a
are unary predicates for the node labels. An
MSO-transducer over the signature
S
=
{
S
1
,...,S
n
,
(
L
a
)
a∈ʓ
}
S
defines a functional tree transformation
T
ʓ
, provided the output is a ranked tree structure (which is a decidable
property). For instance, consider a ranked alphabet
ʓ
=
{g,a}
where
g
is a
binary symbol and
a
a constant, and the transformation
t
rev
which reverses a
tree, i.e., reverses the order relation between the children of any internal node.
The transformation
t
rev
is definable by the following one-copy MSO-transducer:
on
L
ʳ
(
x
)
ˆ
1
,
1
ˆ
pos
(
x
)
ˆ
L
ʳ
(
x
)
ˆ
dom
≡
≡
≡
S
i
(
x, y
)
≡
L
ʳ
(
x
)
∧
ˆ
S
r
(
ʳ
)
−i
+1
(
x, y
)
ʳ∈ʓ
for
ʳ
.
Correspondences between MSO-transducers on ranked trees and tree trans-
ducers has been first studied in [22,8,23] for attribute grammars and macro tree
transducers, and more recently in [4] for streaming tree transducers.
Macro tree transducers extend top-down tree transducers with parameters in
which to store partial output trees. They correspond to purely functional pro-
grams working on tree structures: states are mutually recursive functions and
can carry parameters. Due to lack of space, we do not define formally macro tree
transducers. MSO-transducers on ranked trees correspond exactly to (determin-
istic) macro tree transducers of linear-size increase, i.e. macro tree transducers
∈
ʓ
and
i
∈{
1
,
2
}
