Editing Finite-state transducer (section)

==Operations on finite-state transducers==

The following operations defined on finite automata also apply to finite transducers:

* [[Union (set theory)|Union]].  Given transducers {{mvar|T}} and {{mvar|S}}, there exists a transducer <math>T\cup S</math> such that <math>x[T\cup S]y</math> if and only if <math>x[T]y</math> or <math>x[S]y</math>.
* [[Concatenation]].  Given transducers {{mvar|T}} and {{mvar|S}}, there exists a transducer <math>T\cdot S</math> such that <math>x[T\cdot S]y</math> if and only if there exist <math>x_1, x_2, y_1, y_2</math> with <math>x=x_1x_2, y =y_1y_2, x_1[T]y_1</math> and <math>x_2[S]y_2.</math>
* [[Kleene closure]].  Given a transducer {{mvar|T}}, there might exist a transducer <math>T^*</math> with the following properties:<ref name="BoigelotLegayWolper2003">{{cite book | title = Computer Aided Verification | last1 = Boigelot | first1 = Bernard | last2 = Legay | first2 = Axel | last3 = Wolper | first3 = Pierre | chapter = Iterating Transducers in the Large | series = Lecture Notes in Computer Science | date = 2003 | volume = 2725 | pages = 223–235 | publisher = Springer Berlin Heidelberg | issn = 0302-9743 | eissn = 1611-3349 | doi = 10.1007/978-3-540-45069-6_24 | isbn = 978-3-540-40524-5 | url = }}</ref>
{{NumBlk|*::| <math>\epsilon[T^*]\epsilon</math>; |{{EquationRef|k1}}}}
{{NumBlk|*::| if <math>w[T^*]y</math> and <math>x[T]z</math>, then <math>wx[T^*]yz</math>; |{{EquationRef|k2}}}}
:: and <math>x[T^*]y</math> does not hold unless mandated by ({{EquationNote|k1}}) or ({{EquationNote|k2}}).
* [[Composition of relations|Composition]]. Given a transducer {{mvar|T}} on alphabets Σ and Γ and a transducer {{mvar|S}} on alphabets Γ and Δ, there exists a transducer <math>T \circ S</math> on Σ and Δ such that <math>x[T \circ S]z</math> if and only if there exists a string <math>y\in\Gamma^*</math> such that <math>x[T]y</math> and <math>y[S]z</math>. This operation extends to the weighted case.<ref>{{harvnb|Mohri|2004|pp=3–5}}</ref>

:This definition uses the same notation used in mathematics for [[Composition of relations|relation composition]]. However, the conventional reading for relation composition is the other way around: given two relations {{mvar|T}} and {{mvar|S}}, <math>(x,z)\in T\circ S</math> when there exist some {{mvar|y}} such that <math>(x,y)\in S</math> and <math>(y,z)\in T.</math>

* [[Projection (mathematics)|Projection]] to an automaton.  There are two projection functions: <math>\pi_1</math> preserves the input tape, and <math>\pi_2</math> preserves the output tape.  The first projection, <math>\pi_1</math> is defined as follows:

: Given a transducer {{mvar|T}}, there exists a finite automaton <math>\pi_1 T</math> such that <math>\pi_1 T</math> accepts ''x'' if and only if there exists a string ''y'' for which <math>x[T]y.</math>

:The second projection, <math>\pi_2</math> is defined similarly.

* [[Determinization]]. Given a transducer {{mvar|T}}, we want to build an equivalent transducer that has a unique initial state and such that no two transitions leaving any state share the same input label. The [[powerset construction]] can be extended to transducers, or even weighted transducers, but sometimes fails to halt; indeed, some non-deterministic transducers do not admit equivalent deterministic transducers.<ref>{{Cite web|url=http://www.let.rug.nl/~vannoord/papers/preds/node22.html|title = Determinization of Transducers}}</ref> [[Characterization (mathematics)|Characterizations]] of determinizable transducers have been proposed<ref>{{harvnb|Mohri|2004|pp=5–6}}</ref> along with efficient algorithms to test them:<ref>{{harvnb|Allauzen|Mohri|2003}}</ref> they rely on the [[semiring]] used in the weighted case as well as a general property on the structure of the transducer (the [[twins property]]).
* Weight pushing for the weighted case.<ref>{{harvnb|Mohri|2004|pp=7–9}}</ref>
* Minimization for the weighted case.<ref>{{harvnb|Mohri|2004|pp=9–11}}</ref>
* Removal of [[Nondeterministic finite automaton|epsilon-transitions]].