Information Technology Reference
In-Depth Information
Then, the set of words of even length is defined by the sentence
∃
X
o
∃
X
e
·
ˆ
o/e
(
X
o
,X
e
)
∧∀
x
·
(last(
x
)
→
x
∈
X
e
)
.
3.3 Logical Transducers: Definition
Logical transducers define functional transformations from input to output word
structures. The output structure is defined by taking a fixed number
k
of copies
of the input structure domain. Some node of these copies can be filtered out by
formulas with one free first-order variable. In particular, the nodes of the
c
-th
copy are the input positions that satisfy some given formula
ˆ
pos
(
x
). The predi-
cates
L
a
and
of the output structure are defined by formulas with respectively
one and two free first-order variables, interpreted over the input structure. More
precisely, position labelled
a
of the
c
-th copy are defined by a given formula
ˆ
c
L
a
(
x
), interpreted over the input word. If this formula holds true, it means
that the
c
-th copy of
x
, if it exists, is labelled
a
in the output word. The order
relation between two output positions is defined by formulas with two free vari-
ables interpreted over the input word. For instance, the order relation between
positions of the
c
-th copy and the
d
-th copy (
c
and
d
canbeequal)isdefinedby
aformula
ˆ
(
x, y
)
c,d
interpreted over the input structure. If this formula holds
true, it means the the
c
-th copy of
x
occurs before the
d
-th copy of
y
in the
output word. Let us formally define logical transducers.
Definition 1.
Let ʣ be an alphabet. A logical MSO-transducer (MSOT) on the
signature
S
ʣ
is a tuple
T
=(
k,ˆ
dom
,
(
ˆ
pos
(
x
))
1
≤c≤k
,
(
ˆ
c
L
a
(
x
))
1
≤c≤k,a∈ʣ
,
(
ˆ
c,d
(
x, y
))
1
≤c,d≤k
)
and the formulas ˆ
dom
, ˆ
pos
, ˆ
c
L
a
and ˆ
c,d
where k
∈
N
for all c, d
∈{
1
,...,k
}
and a
∈
ʣ are MSO formulas over
S
ʣ
.
Semantics
A logical MSO-transducer
T
defines a function from
S
ʣ
-structures
to
S
ʣ
-structures, denoted by
T
:
M
(
S
ʣ
)
→M
(
S
ʣ
). The domain of
T
consists of all structures
M
such that
M
|
=
ˆ
dom
. Given a structure
M
∈
dom
(
T
), the
output structure N
such that (
M,N
)
∈
T
is defined by
N
=
(
D
N
,
(
L
a
)
a∈ʣ
,
N
)where:
-
D
N
ↆ
dom(
M
)
×{
1
,...,k
}
is defined by
D
N
=
=
ˆ
pos
(
i
)
{
(
i,c
)
|
i
∈
dom(
M
)
,c
∈{
1
,...,k
}
,M
|
}
We rather denote by
i
c
the elements of
D
M
.
-
for all
a
ʣ
, the interpretation
L
a
is defined by
L
a
=
∈
i
c
=
ˆ
c
L
a
(
i
)
D
N
{
|
i
∈
dom(
M
)
,c
∈{
1
,...,k
}
,M
|
}∩
N
is defined by
-
the interpretation
=
ˆ
c,d
N
=
(
i
c
,j
d
)
(
D
N
D
N
)
{
|
i,j
∈
dom(
M
)
,c,d
∈{
1
,...,k
}
,M
|
(
i,j
)
}∩
×
