Information Technology Reference
In-Depth Information
Remark 1.
Note that the size of the output structure
N
is linearly bounded by
the size of
M
,asitisatmost
k.
|
dom
(
M
)
|
. We say that MSO-transducers define
linear-size increase
transformations.
Logical transducers as word-to-word transformers
Note that in general, an MSO-
transducer
T
over
S
ʣ
may not define a word-to-word transformation, as the
output structure of an input word structure may not be a word. We say that
T
is an
MSO-transducer of finite words over ʣ
if for all words
w
ʣ
∗
such that
∈
ʣ
∗
such that
w
∈
dom(
T
),
T
(
w
) is a word, i.e., there exists
v
∈
T
(
w
)is
isomorphic to
v
. This property is decidable:
Proposition 1.
It is decidable whether an MSO-transducer over
S
ʣ
is an MSO-
transducer of finite words over ʣ.
Proof.
Let
T
=(
k,ˆ
dom
,
(
ˆ
pos
(
x
))
1
≤c≤k
,
(
ˆ
c
L
a
(
x
))
1
≤c≤k,a∈ʣ
,
(
ˆ
c,d
(
x, y
))
1
≤c,d≤k
).
We construct a formula is word
T
which is satisfiable in
ʣ
∗
iff
T
is an MSO-
transducer of finite words over
ʣ
. The result follows since MSO over finite words
is decidable, by Buchi-Elgot-Trakhtenbrot's Theorem.
Before giving the construction, let us introduce the following useful shortcuts.
We write
·
c
=1
ˆ
and
·
c
=1
ˆ
. We also
x
c
x
c
∀
·
ˆ
instead of
∀
x
∃
·
ˆ
instead of
∃
x
ˆ
)tomeanthat
x
c
is quantified over
output nodes that belong to the domain of the output structure. By
x
c
=
y
d
we
denote the formula
x
=
y
if
c
=
d
,and
x
c
]
x
c
(
ˆ
pos
(
x
)
write [
∀
·
ˆ
instead of
∀
·
→
=
d
. Therefore, by
x
c
=
y
d
we
↥
if
c
denote the formula
x
=
d
.
It is also convenient to define the output successor relation. For all
c, d
=
y
if
c
=
d
,and
if
c
∈
{
1
,...,k
}
,welet
ˆ
c,
S
(
x, y
)
ˆ
c,d
(
ˆ
c,e
ˆ
e,d
x
c
=
y
d
z
e
z
e
=
x
c
z
e
=
y
d
)
≡
(
x, y
)
∧
∧∀
·
(
x, z
)
∧
(
z,y
)
→
∨
Finally, we can construct the expected formula:
is word
T
≡
ˆ
dom
→
(1) [
·
a
=
b∈ʣ
¬
x
c
]
ˆ
i
L
a
(
x
)
ˆ
i
L
b
(
x
)
∀
∨¬
·
a∈ʣ
ˆ
c
L
a
(
x
)
x
c
]
∧
(2) [
∀
(
ˆ
c,
S
(
x, y
)
ˆ
c,
S
(
x, z
)
x
c
y
d
z
e
]
y
d
=
z
e
)
∧
(3) [
∀
∀
∀
·
∧
→
∀z
e
]
·
(
ˆ
d,
S
(
y,x
)
∧ ˆ
e,
S
(
z,x
)
→ y
d
=
z
e
)
∧
(4) [
∀x
c
∀y
d
ˆ
e,
S
(
z,x
)
ˆ
e,
S
(
z,y
))
∧
∀
x
c
∀
y
d
]
·
(
x
c
=
y
d
)
→
∃
z
e
]
·
∨
∃
z
e
]
·
(5) [
([
[
ˆ
d,
S
(
y,x
)
x
c
y
d
]
∧
(6) [
∃
∀
·¬
Subformula (1) ensures that each output node is labeled by at most one letter.
Subformula (2) ensures that each output node is labeled by at least one letter.
Subformula (3) ensures that the output successor relation is a function. Subfor-
mula (4) ensures that the inverse of the output successor relation is a function.
Finally, Subformulas (5) and (6) ensures that there is exactly one output node
without predecessor.
