Information Technology Reference
In-Depth Information
Similarly to the syntactic equivalence relation for languages, one can define
left-
and
right-
equivalence relations for transformations with origin
f
,resp.
denoted by
L
f
and
R
f
.
ʣ
∗
.
Definition 4.
Let f be a transformation with origin on ʣ.Letv
1
,v
2
∈
f
v
2
if for all w
ʣ
∗
:
Then, v
1
L
∈
1. v
1
w
∈
dom(
f
)
iff v
2
w
∈
dom(
f
)
dom(
f
)
,thenf
(
v
1
w
)
/
dom(
v
1
)
∼
↥
f
(
v
2
w
)
/
dom(
v
2
)
.
Symmetrically,
2. if v
1
w
∈
f
=
rev
(
f
)
.
R
L
Example 7.
For instance, consider the
o
-transformation
g
that maps any
u
∈
ʣ
∗
to (
f
rev
(
u
)
u,
o
), where, naturally, for all
i ∈{
1
,...,|u|}
,
o
(
i
)=
|u|−i
+1 and
o
(
|u|
+
i
)=
i
. Then, there are only two equivalence classes for both equivalence
relation:
and
ʣ
+
.Indeed,forall
w
ʣ
∗
,
{
}
∈
2
|
v
1
|
w.
f
(
v
1
w
)
/
dom(
v
1
)
=(
f
rev
(
w
)
f
rev
(
v
1
)
v
1
w
)
/
dom(
v
1
)
=
f
rev
(
w
)
↥
Therefore
f
(
v
1
w
)
/
dom(
v
1
)
∼
↥
f
rev
(
w
)
w
if
v
1
=
and
f
(
v
1
w
)
/
dom(
v
1
)
∼
↥
f
.
f
rev
(
w
)
↥
w
otherwise. A similar arguments applies for
R
It is then possible to characterise MSOT-definable
o
-transformations by a
Myhill-Nerode like theorem, and to give an effective characterisation of FOT-
definable
o
-transformations.
Theorem 5 (M. Bojanczyk [9]
4
).
Let f be a transformation with origin over
ʣ. The following two statements hold true:
1. f is MSOT-definable iff both
f
and
f
have finite index.
L
R
f
and
f
have finite index and for all u
ʣ
∗
,
2. f is FOT-definable iff both
L
R
∈
f
-class of u and the
f
-class of u are FO-definable languages.
the
L
R
f
-equivalence
classes are regular languages that can be effectively represented by automata.
Characterization (2) is therefore effective, as it suces to decide whether all
equivalence classes are FO-definable, which is decidable [18].
f
-and
As shown in [9], if
f
is MSOT-definable, then the
L
R
6 Beyond Functional Finite Word Transformations
In this section, we discuss other transducer-logic connections for non-functional
transformations and other structures (infinite words and trees).
6.1 Non-functional Finite Word Transformations
The state-based transducer models (FST, 2FST and SST) can all be extended
with non-determinism (leading to the classes NFT, 2NFT, and NSST resp.), and
rather define relations from word to words instead of functions. MSO-transducers
can, as well, be extended with non-determinism.
4
We adopt in this paper a slightly different, but equivalent, formalisation as in [9].
