Information Technology Reference
In-Depth Information
-
The transformation
f
copy
copies input words twice, i.e. for all
u
∈
ʣ
∗
,
f
copy
(
u
)=
uu
.
-
The transformation
f
rev
reverses input words, i.e.
f
rev
(
˃
1
...˃
n
)=
˃
n
...˃
1
.
E.g.
f
rev
(
abaa
)=
aaba
.
-
The transformation
f
1
/
2
is defined over
a
∗
by, for all
n
0,
f
1
/
2
(
a
n
)=
≥
a
n/
2
. E.g.
f
1
/
2
(
a
8
)=
a
4
and
f
1
/
2
(
a
3
)=
a
.
-
The transformation
f
exp
exponentiates the number of
a
symbols in a word
of the form
a
n
, e.g.
f
exp
(
a
n
)=
a
2
n
,and
f
exp
(
w
) is undefined if
w
contains
at least one
b
.
3 Logical Transducers for Word Transformations
In this section, we introduce
logical transducers
, a logic-based formalism intro-
duced by B. Courcelle [14] to define transformations of logical structures. We
refer the reader to [15] for more details and results about logical transducers. Al-
though logical transducers can generally define transformations of arbitrary log-
ical structures, we specialise them to finite word transformations in this section.
We first introduce the notion of word logical structures, and then the classical
first-order and monadic second-order logics, interpreted over (logical structures
of) words.
3.1 Words as Logical Structures
Aword
w
over an alphabet
ʣ
can be seen as a
logical structure
1
w
over the
signature
,where(
L
a
)
a∈ʣ
are monadic predicates that define
the labels of the positions in
w
,and
S
ʣ
=
{
(
L
a
)
a∈ʣ
,
}
is a binary predicate that defines the order
on word positions. Formally,
w
=(dom(
w
)
,
(
L
w
) is the logical structure
whose domain is dom(
w
), and such that the predicates are interpreted as follows:
a
)
a∈ʣ
,
w
=
L
a
=
{
i
∈
dom(
w
)
|
w
(
i
)=
a
}
{
(
i,j
)
|
i,j
∈
dom(
w
)
∧
i
≤
j
}
When it is clear from the context, we rather write
w
instead of
w
.
A structure on
S
ʣ
is also called a
S
ʣ
-structure. We denote by
M
(
S
ʣ
)theset
of
S
ʣ
-structures. Note that a
S
ʣ
-structure may not be isomorphic to any word.
ʣ
∗
,
w
However for all
w
∈
∈M
(
S
ʣ
). Given a structure in
M
∈M
(
S
ʣ
), we
denote by dom(
M
) its domain.
3.2 First-Order and Monadic Second-Order Logics on Words
Givenanalphabet
ʣ
,
monadic second-order formulas
(
MSO formulas
)over
the signature
S
ʣ
are built over first-order variables
x,y...
and second-order
variables
X,Y ...
. They are defined by the following grammar:
ˆ
::=
∃
X
·
ˆ
|∃
x
·
ˆ
|
ˆ
∧
ˆ
|¬
ˆ
|
x
∈
X
|
L
a
(
x
)
|
x
y
|
(
ˆ
)
1
See for instance [19] or [40] for a definition of logical structures.
