Information Technology Reference
In-Depth Information
In the rest of this section, by MSO-transducer and MSOT we always mean
an MSO-transducer of finite words.
FO-transducers of finite words.
An FO-transducer (FOT)
T
is defined as an
MSO-transducer, except that each formula of
T
is an FO formula over
S
ʣ
.
Definability.
We say that a transformation
R
of finite words is definable by a
logical transducer
T
if
R
=
T
.Wesaythat
R
is MSOT-definable (resp. FOT-
definable) if it is definable by an MSO-transducer (resp. FO-transducer) of finite
words.
3.4 Logical Transducers: Examples
In this section, we give several examples of transformations that can be defined
by MSO-transducers.
Example 3.
We show that all transformations of Example 1 but
f
exp
are MSOT-
definable. They are illustrated in Fig. 1. Only the successor relations are depicted.
Input nodes filtered out by formulas
ˆ
pos
(
x
) are represented by fuzzy nodes.
•
The transformation
f
del
on
ʣ
=
{
a, b
}
is definable by the transducer
L
˃
(
x
))
˃∈ʣ
,ˆ
1
,
1
,ˆ
pos
(
x
)
L
a
(
x
)
,
(
ˆ
L
σ
(
x
)
T
del
=(1
,ˆ
dom
≡
≡¬
≡
(
x, y
)
≡
x
y
)
ʣ
∗
,let
v
ʣ
∗
such that
v
=
Given an input word
u
∈
∈
T
del
(
u
). Then
dom
(
v
)=
i
1
, as defined by
ˆ
pos
,and
v
=
(
i
1
,j
1
)
i
1
,j
1
{
∈
dom(
u
)
|
u
(
i
)=
b
}
{
|
∈
dom(
v
)
,i
≤
j
}
.
•
To define transformation
f
double
, one needs to take two copies of the input
structure. It is defined by the transducer
T
double
with
k
= 2 and for
i
∈{
1
,
2
}
:
ˆ
dom
≡
ˆ
pos
(
x
)
≡
ˆ
i
L
a
(
x
)=
L
a
(
x
)
ˆ
i
L
b
(
x
)=
L
b
(
x
)
ˆ
1
,
1
yˆ
1
,
2
yˆ
2
,
1
yˆ
2
,
2
(
x, y
)
≡
x
(
x, y
)
≡
x
(
x, y
)
≡
x
≺
(
x, y
)
≡
x
y
Note that the output predicate
from copy 2 to copy 1 is only defined when
x
occurs strictly before
y
. It implies that an output node
y
d
is a successor of
x
d
iff one of the two following conditions hold: (
i
)
c
=1and
d
=2and
x
=
y
,or
(
ii
)
c
=2and
d
=1and
y
is a successor of
x
in the input word. If one wants
to restrict the domain of
T
double
to words in
a
∗
, it suces to define the domain
formula by
ˆ
dom
≡∀
x
·
L
a
(
x
).
•
Let us consider transformation
f
copy
. Again, one needs two copies of the input
structure. It is similar to
T
double
except the way the output order is defined:
ˆ
pos
(
x
)
ˆ
i
L
a
(
x
)=
L
a
(
x
)
ˆ
i
L
b
(
x
)=
L
b
(
x
)
ˆ
dom
≡
≡
ˆ
1
,
1
yˆ
1
,
2
yˆ
2
,
1
ˆ
2
,
2
(
x, y
)
≡
x
(
x, y
)
≡
x
(
x, y
)
≡↥
(
x, y
)
≡
x
y
Note that compared to
T
double
, only the definition of
ˆ
2
,
1
differs. We indeed
completely disallow a node from copy 2 to be smaller than a node from copy 1.
