Information Technology Reference
In-Depth Information
Non-deterministic state-based models.
We have already seen in Section 4.1 how
to extend FST with non-determinism. Similarly, 2FST can also be extended with
non-determinism, the transition relation
ʔ
being of type
ʔ
ↆ
Q
×
(
ʣ
∪{
,
}
ʣ
∗
. Unlike FST, there can be infinitely many runs on the
same input word, leading to infinitely many outputs for that word. For instance,
2NFT can loop an arbitrary number of times between two input positions and
non-deterministically decide to apply the halting transition function. Their runs
can even be infinite but we consider only finite runs to define the transformation.
SST can, as well, be extended with non-determinism, with transition relation
)
×
Q
×{
+1
,
−
1
}×
ʔ
Q
. Unlike 2NFT, there is alway a finite number (exponential in
the worst-case) of accepting runs on the same input word.
ↆ
Q
×
ʣ
×
Non-deterministic MSO-transducers (NMSOT).
MSO-transducers can be ex-
tended with non-determinism by allowing all the formulas (including the domain
formula) to use a finite set of second-order of variables
X
1
,...,X
n
. Given an in-
put word
u
, the outputs of
u
depend on the valuations of these second order
variables by subsets of dom(
u
). In particular, modulo a valuation of
X
1
,...,X
n
by subsets of dom(
u
), the transformation becomes functional, and the outputs
of
u
are the set of output words defined for each valuation. For instance, it is
possible to define with an NMSO-transducer
T
sub
the tranformation
R
sub
which
maps any word
u
to all its subwords, using one second-order variable
X
and
only one copy, as follows:
ˆ
dom
≡
,
ˆ
pos
(
x, X
)=
x
X
,
ˆ
˃
(
x
)=
L
˃
(
x
)for
∈
ʣ
,and
ˆ
1
,
1
all
˃
y
. If one wants to restrict all the subwords to
subwords generated by the even positions, it suces to strengthen the domain
formula to
ˆ
dom
(
X
)
∈
(
x, y
)
≡
x
≡∃
Yˆ
o/e
(
Y,X
), where
ˆ
o/e
has been defined in Example 2.
Transducer-Logic Connections.
A transformation
R
is
finitary
if for all words
u ∈ ʣ
∗
,
R
(
u
) is finite. It is clear that NFT, NSST and NMSOT define fini-
tary transformations. However, 2NFT does not define, in general, finitary trans-
formations. It turns out that 2NFT and NMSOT define incomparable classes
of transformations.To capture exactly NMSOT with a two-way device,
Hennie
machines
have been introduced in [21]. Hennie machine can rewrite their input
tape, but each input position must be visited a constant number of times. On
the one-way model side, it has been shown that NSTT corresponds exactly to
NMSOT [5].
a,b
b
U
:=
Ua
V
:=
U
:=
U
V
:=
Vb
q
0
q
1
a
UUV
U
:=
U
V
:=
b
Fig. 7.
Example of
ˉ
-SST defining
f
ˉ
, with output function
O
(
{q
1
}
)=
UV
