Space-Efficient Bimachine Construction Based on the Equalizer Accumulation Principle
Stefan Gerdjikov Stoyan Mihov Klaus U. Schulz






Faculty of Mathematics and Informatics

Sofia University

5, James Borchier Blvd., Sofia 1164, Bulgaria

stefangerdzhikov@fmi.uni-sofia.bg
Institute of Information and Communication Technologies

Bulgarian Academy of Sciences

25A, Acad. G. Bonchev Str., Sofia 1113, Bulgaria

stoyan@lml.bas.bg
Centrum für Informations- und Sprachverarbeitung (CIS)

Ludwig-Maximilians-Universität München

Oettingenstr. 67, 80538 München, Germany

schulz@cis.uni-muenchen.de


Space-Efficient Bimachine Construction Based on the Equalizer Accumulation Principle
    Stefan Gerdjikov1,2 Stoyan Mihov2 Klaus U. Schulz3
    
====================================================================================










Algorithms for building bimachines from functional transducers found in the literature in a run of the bimachine imitate one successful path of the input transducer. Each single bimachine output exactly corresponds to the output of a single transducer transition. Here we introduce an alternative construction principle where bimachine steps take alternative parallel transducer paths into account, maximizing the possible output at each step using a joint view. The size of both the deterministic left and right automaton of the bimachine is restricted by 2^| Q| where 
| Q| is the number of transducer states. Other bimachine constructions lead to larger subautomata. 
As a concrete example we present a class of real-time functional transducers with n+2 states for which the standard bimachine construction generates a bimachine with at least Θ(n!) states whereas the construction based on the equalizer accumulation principle leads to 2^n + n +3 states. 
Our construction can be applied to rational functions from free monoids to “mge monoids”, a large class of monoids including free monoids, groups, and others that is closed under Cartesian products. 


 



§ INTRODUCTION


Functional finite-state transducers and bimachines <cit.> are devices for translating a given input sequence of symbols to a new output form. With both kinds of devices, the full class of regular string functions can be captured. However, finite-state transducers  
are more restricted in the sense that a non-deterministic behaviour is needed to realize all regular functions. In contrast, with bimachines all regular functions can be processed in a fully deterministic way. From a practical point, both models have their own advantages. For a given translation task it is often much simpler to find a non-deterministic finite-state transducer. 
Bimachines, on the other hand, are much more efficient.  General constructions that convert finite-state transducers into equivalent bimachines help to obtain both benefits at the same time.    






Known algorithms for converting a functional finite-state transducer T with set of states Q into an equivalent bimachine are based on the “path reconstruction principle”: At each step of a bimachine computation, the bimachine output represents the output of a single transducer transition step. 
Furthermore, for any complete input string w the sequence of bimachine outputs for w is given by the sequence of outputs of T for w on a specific path.  
Control of these two principles is achieved either by transforming the source transducer to be unambiguous <cit.> or by using a complex notion of states for the states of the deterministic 
subautomata of the bimachine <cit.>. The “enhanced” power set constructions used to build the two subautomata have the effect that the 
size of at least one subautomaton is not bounded by 2^| Q|. Recall that 2^| Q| is the 
bound obtained for a standard power set determinization. 

Here we introduce a new construction that only needs a conventional power set construction for the states of both subautomata of the bimachine. As a consequence, the size of both subautomata is bound by 2^| Q|. In the new construction, the output of a single bimachine step takes into account the outputs of several parallel alternative transducer transitions, in a way to be explained. Using a principle called “equalizer accumulation” the joint view on all relevant transducer transitions leads to a kind of maximal output for the bimachine. At the same time this “joint look” at parallel paths of the transducer guarantees that the complete bimachine output for an input string w is identical to the combined output of the transducer on any path for w. 

The new construction is not restricted to strings as bimachine output. 
As a second contribution of the paper we introduce and study the class of “monoids with most general equalizers” (mge monoids).
We show that this class includes all free monoids, groups, the tropical semiring, and others and is closed under Cartesian products. 
The aforementioned principle of “equalizer accumulation” is possible for all mge monoids. 

The paper has the following structure. We start with formal preliminaries in Section <ref>. 
In Section <ref> we introduce mge monoids and study formal properties of this class. We define the principle of 
equalizer accumulation and show that equalizer accumulation is possible for all mge monoids. 
In Section <ref> we give an algorithm for deciding the functionality of a transducer with outputs in a mge monoid. 
In Section <ref> we introduce the new algorithm for converting a functional finite-state transducer 
with outputs in a mge monoid into an equivalent bimachine. 
In Section <ref> we present a class of real-time functional transducers with n+2 states for which the standard bimachine construction generates a bimachine with at least Θ(n!) states whereas the construction based on the equalizer accumulation principle leads to 2^n + n +3 states only.
We finish with a short conclusion in Section <ref>. 




§ FORMAL PRELIMINARIES



A monoid M   is a  triple M,∘,e, where M is a non-empty set, ∘ :M × M → M is a total binary function that is associative, i.e.  ∀ a,b,c ∈ M: a ∘ (b ∘ c) = (a ∘ b) ∘ c  and  e ∈ M is the unit element, i.e. ∀ a ∈ M: a ∘ e = e ∘ a = a.  Products a ∘ b are also written a b.


The monoid M supports left cancellation if ∀ a,b,c ∈ M : c ∘ a = c ∘ b → a=b.
The monoid M supports right cancellation if ∀ a,b,c ∈ M : a ∘ c = b ∘ c → a=b.

We list some wellknown notions used in the paper.
An alphabet Σ is a finite set of symbols. 

Words of length n≥ 0 over an alphabet Σ are introduced as usual and written a_1,…,a_n or simply a_1… a_n (a_i ∈Σ). The concatenation of two words u=a_1,…,a_n and v=b_1,…,b_m∈Σ^∗ is u · v = a_1,…,a_n,b_1,…,b_m.  The unique word of length 0 (“empty word”) is written ε. The set of prefixes of a word w is introduced as usual. Σ^∗ denotes the set of all words over Σ. The set  Σ^∗ with concatenation as monoid operation and the empty  word ε  as  unit element is called the free monoid over Σ. The expression u^-1t denotes the word v if u is a prefix of  t and t=u· v, otherwise u^-1t is undefined. 



Let M = M,∘_M,e_M and N = N,∘_N,e_N be two monoids. Let M× N := M× N,∘_M× N,e_M,e_N, where ∘_M× N : (M× N)^2 → M× N  is the total function such that a_1,a_2∘_M× Nb_1,b_2 := a_1 ∘_M b_1, a_2 ∘_N b_2. Then M× N is a monoid.

The monoid M× N is called the Cartesian product of the monoids M and N.




A monoidal finite-state automaton is a tuple of the form
A =  M,Q,I,F,Δ where 


  * M=M,∘,e is a monoid, 

  * Q is a finite set called the set of states, 

  * I⊆ Q is the set of initial states, 

  * F⊆ Q is the set of final states, and 

  * Δ⊆ Q× M × Q 
  is a finite set of transitions called the transition relation. 




Let A =  M,Q,I,F,Δ be a monoidal finite-state automaton. 
The generalized transition relation Δ^∗ is defined as the
smallest subset of Q × M × Q with the following closure 
properties:


  * for all q∈ Q we have q,e,q∈Δ^∗.

  * For all q_1, q_2, q_3∈ Q and w, a ∈ M:
  if q_1,w,q_2∈Δ^∗ and q_2,a,q_3∈Δ,  
  then also q_1,w ∘ a,q_3∈Δ^∗.

The monoidal language  
accepted (or recognized) by A is 

    L( A) :=w∈ M∃ p ∈ I ∃ q ∈ F: p,w,q∈Δ^∗.




Let A =  M,Q,I,F,Δ be a monoidal finite-state automaton. 
A proper path of A is a finite sequence of k>0 transitions

    π = q_0,a_1,q_1q_1,a_2,q_2…q_k-1,a_k,q_k

where q_i-1,a_i,q_i∈Δ for i=1… k.
The number k is called the length of π, we say that π starts in q_0 and ends in q_k. 
States q_0,…,q_k are the states on the path π. If 
q_0=q_k, then the path is called a cycle. 
The monoid element w=a_1 ∘…∘ a_k is called the label of π. 
We denote π as
π = q_0 →^a_1 q_1 …→^a_k q_k.

A successful path is a path starting in an initial state and ending in a final state. 


A state q∈ Q  is accessible if q is the ending of a path of A starting from an initial state. A state q∈ Q  is co-accessible if q is the starting of a path of A ending in a final state. 
A monoidal finite-state automaton A is trimmed iff each state q∈ Q is accessible and co-accessible. 
A monoidal finite-state automaton A is unambiguous iff for every element m ∈ M there exists at most one successful path in A with label m. 


Let A =  M,Q,I,F,Δ be a monoidal finite-state automaton. Then the e-extended automaton for A is the monoidal finite-state automaton A^ext =  M,Q,I,F,Δ^ext, where Δ^ext = Δ∪q,e,qq ∈ Q.

Clearly the e-extended automaton for A is equivalent to A i.e. L( A^ext)=L( A).


A monoidal finite-state automaton A =  M,Q,I,F,Δ  is a mo­noidal finite-state transducer iff M  can be represented as the Cartesian product of a free monoid Σ^∗ with another monoid M',  i.e M = Σ^∗× M' and Δ⊆ Q× (Σ∪{ε}× M') × Q.
A monoidal finite-state transducer A = Σ^∗× M',Q,I,F,Δ is  real-time if Δ⊆ Q× (Σ× M') × Q. A monoidal finite-state transducer A is  functional if L( A) is a function. In this case we denote the function recognized by A as O_ A : Σ^∗→ M'.


Let M be a monoid. A language L ⊆ M is rational iff it is accepted by a monoidal finite-state automaton. A rational function is a rational language that is a function.



A bimachine is a tuple B= M, A_L, A_R,ψ, where:


  * A_L = Σ,L,s_L,L,δ_L and A_R = Σ,R,s_R,R,δ_R are deterministic finite-state automata called the left and right automaton of the bimachine;

  * M = M,∘,e is the output monoid and ψ : (L ×Σ× R) → M is a partial function called the output function.

Note that all states of A_L and A_L are final. The function ψ is naturally extended to the  generalized output functionGeneralized output function of a bimachine ψ^∗ as follows:


  * ψ^∗(l,ε,r)=e for all l∈ L, r∈ R;

  * ψ^∗(l,tσ,r)= ψ^∗(l,t,δ_R(r,σ)) ∘ψ(δ^∗_L(l,t),σ,r) for l∈ L, r∈ R, t∈Σ^∗, σ∈Σ.

The function represented by the bimachine is 

    O_ B:Σ^∗→ M: t  ↦ψ^∗(s_L,t,s_R).

If O_ B(t)=t' we say that the bimachine B translates t into t'. 




§ MONOIDS WITH MOST GENERAL EQUALIZERS


Monoids with most general equalizers (mge monoids), to be introduced below, generalize both free monoids and groups. 
In this section we study properties that provide the basis for the bimachine construction presented afterwards.  







Let M=M,∘,e be a monoid, let n≥ 1. 
A tuple m_1,… m_n in M^n is called 
equalizable iff there exists x_1,…,x_n∈ M^n such that 

    m_1 x_1=… = m_n x_n.
 
In this situation 
x_1,…,x_n is called an equalizer for m_1,… m_n. 

If 
x_1,…,x_n is an equalizer for m_1,… m_n and x∈ M, then  
x_1 x,…,x_n x is called an instance of x_1,…,x_n. An equalizer
x_1,…,x_n for m_1,… m_n is called a most general equalizer (mge) for 
m_1,… m_n if each equalizer
x_1',…,x_n' for m_1,… m_n is an instance of x_1,…,x_n. By Eq^(n)(m_1,…,m_n) ⊆ M^n we denote the set of all equalizers of m_1,… m_n.

As a matter of fact for n>1 in general not all tuples m_1,…,m_n in a monoid are equalizable. There are monoids with equalizable tuples that do not have any mge. 
In our context, most general equalizers become relevant when considering 
intermediate outputs m_1,…,m_n of a functional transducer obtained for the same input word 
w on distinct initial paths. If for some continuation v of w each path can be continued to a final state, on a path with input v, then the completed outputs 
m_1m_1',…,m_nm_n' must be equal. If x_1,…,x_n is a most general equalizer of m_1,…,m_n, then we 
can safely output m_1x_1=… = m_nx_n, “anticipating” necessary output. Below we use this idea for bimachine construction. 

















We introduce a special class of monoids where 
equalizable pairs always have mge's. 


The monoid M=M,∘,e is a mge monoid iff M has right cancellation and 
each equalizable pair m_1,m_2∈ M^2 has a mge.









(a) Let Σ be an alphabet. The free monoid Σ^∗,·,ε for alphabet Σ is 
a mge monoid. In fact, a pair of words u,v is equalizable iff u is a prefix of v=u x or v is a prefix of 
u=vx. In the former (latter) case x,ε (resp. ε,x) is a mge for u,v. 

(b) Another example of a mge monoid is the additive monoid of nonnegative real numbers, (_≥ 0,+,0). Consider a pair of non-negative reals m,n.
Let M=max(m,n), thus M-m,M-n∈ℝ_≥ 0.First, m+(M-m)=n+(M-n)=M shows that M-m,M-n is an equalizer for m,n. Next, if x,y is an arbitrary equalizer for m,n, then m+x=n+y=N. Since x and y are nonnegative N≥ M and N-M∈ℝ_≥ 0. Thus, x=(M-m) +(N-M) and y=(M-n)+(N-M). This proves that
M-m,M-n is a mge of m,n.

(b) Another example of a mge monoid is (^≥ 0,+,0), a submonoid of the “tropical semiring” 
(∪{∞},⊕,⊙) where x⊕ y=min(x,y) and x⊙ y= x +y. 
Consider a pair of non-negative reals (m,n). We may assume that n≥ m.  If (v,w) is any equalizer, then m+v=n+w, (v,w)=(n-m+w,0+w). Since
(n-m,0) is an equalizer for (m,n) it is a mge. 

(c) Both Example (a) and Example (b) are special cases of sequentiable structures in the sense of 
Gerdjikov & Mihov <cit.>. It can be shown that all sequentiable structures are mge monoids. This is a simple consequence of Proposition 2 in <cit.>. 







Let G=G,·,1,^-1 be a group. Then G,·,1 is a mge monoid. For each pair 
g,h of group elements, both 1,h^-1· g and 
g^-1· h,1 are mge's. 



Let M=M,∘_M,e_m and N=N,∘_N,e_n be mge monoids. Then the Cartesian product  
M× N is a mge monoid. 



Let m_1,n_1, m_2,n_2 be an equalizable pair, let 
u_1,v_1, u_2,v_2 be an equalizer. Then 

    m_1u_1,n_1v_1= m_1,n_1 u_1,v_1= m_2,n_2 u_2,v_2= m_2u_2,n_2v_2,

which implies that 

    m_1u_1    =    m_2u_2
    
    n_1v_1    =    n_2v_2.

Both m_1,m_2 and n_1,n_2 are equalizable. Let x_1,x_2 and y_1,y_2 respectively denote
mge's. For some c∈ M and d∈ N we have 
u_i=x_ic and v_i=y_id (i=1,2). The equations

    m_1,n_1 x_1,y_1 =  m_1x_1,n_1y_1= m_2x_2,n_2y_2= m_2,n_2 x_2,y_2.

show that x_1,y_1, x_2,y_2 is an equalizer for 
m_1,n_1, m_2,n_2. Furthermore, 

    x_1,y_1 c,d, x_2,y_2) c,d= x_1c,y_1d, x_2c,y_2d= u_1,v_1, u_2,v_2.

Hence each equalizer is an instance of x_1,y_1, x_2,y_2 and 
x_1,y_1, x_2,y_2 is a mge.


Let M=M,∘,e be a mge monoid. Then M has left cancellation and for each element m ∈ M the pair e,e is a mge of m,m.


Let a,b,c be arbitrary elements of M such that ca=cb. Clearly the pair e,e is an equalizer of c,c and therefore there exists a mge x,y of c,c. Hence there is some d ∈ M such that x d = e = y d. Therefore, by the right cancellation property we get that x = y. On the other hand a,b is also an equalizer of c,c and therefore there is some d' ∈ M such that x d' = a and y d' = b. Since x=y we obtain that a=b. 

Let a,b be an equalizer of m,m. Then ma=mb and thus a=b. Hence e,e is a mge of m,m.


Let M be a monoid, let n≥ 1. A tuple x_1,…,x_n 
is called a joint equalizer for m_1,… m_n and 
m'_1,… m'_n if x_1,…,x_n is an equalizer 
both for m_1,… m_n and for m_1,… m_n.


Note that in the situation of the definition we have m_1x_1=… = m_nx_n and 
m'_1x_1=… =m'_nx_n but we do not demand that m_ix_i=m_i'x_i (1≤ i≤ n). 


Let M=M,∘,e be a mge monoid.

If m_1,…,m_l and n_1,…,n_l have a joint equalizer, then 
each mge for m_1,…,m_l is a mge for n_1,…,n_l and vice versa. Furthermore Eq^(l)(m_1,…,m_l) = Eq^(l)(n_1,…,n_l).



Let k_1,…,k_l denote a joint equalizer for m_1,…,m_l and n_1,…,n_l. 
Let (x_1,…,x_l) be a mge for m_1,…,m_l, let (y_1,…,y_l) be a mge for n_1,…,n_l. 
Then there exists some c∈ M such that k_1,…,k_l=(x_1c,…,x_lc). 
We obtain 
    n_1x_1c= … =n_lx_lc.

Using right cancellation we get n_1x_1=…=n_lx_l, which shows that x_1,…,x_l is an equalizer for n_1,…,n_l and an instance of y_1,…,y_l. 
Symmetrically we see that y_1,…,y_l is an instance of x_1,…,x_l. It follows that both x_1,…,x_l and y_1,…,y_l are mge's for 
m_1,…,m_l and for n_1,…,n_l.


Let M=M,∘,e be a mge monoid. An element m∈ M is invertible if there exists an element n∈ M such that mn=e. It follows from the left cancellation property that n is unique, we write 
m^-1 for n and call m^-1 the inverse of m. 

If m has an inverse m^-1, then 
mm^-1m=m=me and left cancellation shows that m^-1m=e. Hence “right” inverses are left inverses and vice versa. 


Let M=M,∘,e be a mge monoid. Let m,n∈ M be given and assume that the equation
mx=n has a solution. Then the solution is unique and if x_1,x_2 is a mge of m,n then x=x_1 x_2^-1. 

 Uniqueness of solutions follows directly from left cancellation. 
If mx=n has a solution x, then x,e is an equalizer for m,n. 
 Then there exists an element d∈ M such that 
x_1d=x and x_2d=e. Therefore d is the inverse of x_2 i.e. d :=x_2^-1. Now mx_1x_2^-1=nx_2x_2^-1=n. The product 
x_1x_2^-1 represents the unique solution for mx=n.

  
A mge monoid M=(M,∘,e) is effective if 
(i) M can be represented as a recursive subset of  and the monoid operation is computable (ii) the equality of two monoid elements is decidable, (iii) it is decidable whether a 
given pair m,m'∈ M^2 is equalizable, there is a computable function η∈ M^2 → M^2, such that for each equalizable pair m,m' always η(m,m') is a mge of m,m', and
(iv) for every invertible element m∈ M the inverse m^-1 is computable.

It is simple to see that the class of effective mge monoids is closed under Cartesian products and that
the above examples of mge monoids are effective under natural assumptions[The tropical semiring is not effective, but the finite set of transition outputs of a given transducer can be embedded in an effective mge submonoid of the tropical semiring.].


Let M=M,∘,e be an effective mge monoid. Let m,n∈ M be given and assume that the equation
mx=n has a solution. Then we may effectively compute the solution.



Let M=M,∘,e be a mge monoid. Then 
for each n≥ 1, every equalizable tuple m_1,…,m_n has a mge. 



We use induction on n. For n=1 note that e is always a mge for m. For n=2 equalizable pairs have mge's 
by definition of mge monoids. 
Let n≥ 2 and 
m_1,…,m_n,m_n+1
be equalizable, say 
m_1v_1=… = m_nv_n=m_n+1v_n+1. 
By induction hypothesis there exists a mge x_1,…,x_n for m_1,…,m_n. 
For some c∈ M we have x_ic=v_i for 1≤ i≤ n. 

Since m_n and m_n+1 are equalizable there exists a mge y_n,y_n+1 and some d∈ M such that y_n d=v_n, y_n+1 d=v_n+1. 
Now we have two representations for v_n:

    x_n c=v_n=y_n d.

Hence x_n,y_n is equalizable. Let z_x,z_y be a mge. Since c,d is an instance there exists an f∈ M such that c=z_x f, d=z_y f.
Now we can represent the full equalizer v_1,…,v_n,v_n+1 in the following form

    v_1    =    x_1c=x_1z_xf
       …   
    
    v_n    =    x_nc=x_nz_xf
    
    v_n+1   =    y_n+1d=y_n+1z_yf

as an instance of x_1z_x,…,x_n z_x,y_n+1 z_y. As a matter of fact the latter is an equalizer for m_1,…,m_n,m_n+1. 
Since v_1,…,v_n,v_n+1 was any equalizer for m_1,…,m_n,m_n+1
it follows that x_1z_x,…,x_n z_x,y_n+1 z_y is a mge for m_1,…,m_n,m_n+1.





The proof of Lemma <ref> provides us with an effective way to compute mge's. 
The following corollaries describe the principle of equalizer accumulation mentioned in the introduction. 

Let M be an effective mge monoid. If m_1,…,m_n∈ M^n are equalizable, then μ^(n)(m_1,…,m_n) is the mge of 
m_1,…,m_n, where
μ^(n):M^n→ M^n is defined as:


  * μ^(1)(m)=e for every m∈ M,

  * μ^(2)(m_1,m_2)=η(m_1,m_2) for each equalizable pair ⟨ m_1,m_2⟩,

  * If μ^(n) is given, then for every equalizable tuple ⟨ m_1,…,m_n+1⟩∈ M^n+1 the i-th coordinate of μ^(n+1)(m_1,…,m_n+1), denoted μ^(n+1)_i(m_1,…,m_n+1),  is given by

    μ_i^(n+1)(m_1,…,m_n+1)=
          μ_i^(n)(m_1,…,m_n) ∘ z_x for  i≤ n
    η_2(m_n,m_n+1) ∘ z_y  for  i=n+1

where ⟨ z_x,z_y⟩ := η_(μ_n^(n)(m_1,…,m_n),η_1(m_n,m_n+1)).
 
 
The next corollary shows that we can express the function μ using only pairwise mge's.
 In the settings of Corollary <ref>

    μ^(n)(m_1,…,m_n) = γ^(n)(η(m_1,m_2),η(m_2,m_3),…,η(m_n-1,m_n)),

where γ^(n) : (M^2)^n-1→ M^n is a partial function defined inductively:


  * γ^(1)=e,

  * γ^(2)(X)=X for every X ∈ M^2,

  * 
    γ_i^(n+1)(X^(1),…,X^(n))=
          γ_i^(n)(X^(1),…,X^(n-1)) ∘η_1(γ_n^(n)(X^(1),…,X^(n-1)),X_1^(n)) for  i≤ n
    
    X_2^(n)∘η_2(γ_n^(n)(X^(1),…,X^(n-1)),X_1^(n))  for  i=n+1

 

In particular, if two tuples m_1',…,m_n' and m_1”,m_2”,…,m_n” have the property:

    η(m_i',m_n') is a mge for m_i”,m_n” for each  i<n,

then μ^(n)(m_1',m_2',…,m_n')=μ^(n)(m_1”,m_2”,…,m_n”).

Note that if η(e,e)=e,e, then 

    γ^(n)(e,e,e,e,…,e,e)=e,e,…,e






§ SQUARED AUTOMATA AND FUNCTIONALITY TEST FOR MGE MONOIDS


In this section we characterize the class of functional transducers with outputs in an effective mge monoid and give an efficient algorithm for testing the functionality. We make use of the squaring transducer approach presented in <cit.>. 


Let M=(M,∘,e) be an effective mge monoid and η be a computable function computing the mge. 
We start with some simple observations that enables us to restrict attention to real-time transducers.

Let T=Σ^*× M,Q,I,F,Δ be a trimmed functional transducer, let p∈ M. If

p,ε,m,p∈Δ^*,

then m=e.



Since T is trimmed state p is both accessible and co-accessible. There exist u_1,u_2∈Σ^*, i∈ I, f∈ F, and m_1,m_2∈ M such that

    i,u_1,m_1,p∈Δ^*  and p,u_2,m_2,f∈Δ^*.

Therefore u_1u_2,m_1m_2∈ L( T). Using the cycle p,ε,m,p∈Δ^*, we see that i,u_1u_2,m_1mm_2,f∈δ^*. Hence u_1u_2,m_1mm_2∈ L( T). 

Finally, since T is functional we have m_1m_2=m_1mm_2. Since M satisfies the left and the right cancellation properties we obtain e=m.

 
A (trimmed) transducer T=Σ^*× M,Q,I,F,Δ contains 

a cycle with label (ε,m) such that m≠ e if and only if T contains a 

cycle π of length less or equal to |Q|, with label (ε,m') such that m'≠ e. 
Thus we can efficiently check whether there exists a cycle

    p,ε,m,p∈Δ^*  with  m≠ e.

If this is the case, we reject that T is functional. 



If every ε-cycle in T is an (ε,e)-cycle, then we can apply a specialised ε-closure procedure (see e.g. <cit.>) and convert T into a real-time transducer, T', with

    L( T) ∩ (Σ^+ × M)=L( T') ∩ (Σ^+ × M).

In addition we can compute the finite set:

    L_ε( T)= {m | ∃ i∈ I,f∈ F (i,ε,m,f∈Δ^*}.

If | L_ε( T)| > 1, then we reject that T is functional.
Otherwise, the functionality test for T boils down to check whether the real-time transducer T' is functional.


Due to Remarks <ref> and <ref> for the functionality test we may assume 
that T is a real-time transducer. 
(At the end of this section we add a note how the test can be efficiently applied to an arbitrary trimmed transducer directly without such a preprocessing step.) 
As a preparation we need the following structure. 


Let T=Σ^∗× M,Q,I,Δ,F be a  monoidal finite-state transducer, let 
Δ_2⊆ (Q× Q)× ( M× M) × (Q× Q) be finite. 
Then 
    M× M,Q× Q,I× I,F× F,Δ_2
 is a squared output automaton for T if the following holds:

    p_1,q_1,m,n,p_2,q_2∈Δ_2^* ∃ u∈Σ^*      (p_1,u,m,q_1∈Δ^* 
           and p_2,u,n,q_2∈Δ^*).




Let T=Σ× M,Q,I,Δ,F be a  real-time transducer. 
Then the monoidal finite-state-automaton A^sq defined as:

    A^sq   =    M× M,Q× Q,I× I,F× F,Δ_2
    Δ_sq    =    {p_1,p_2,m_1,m_2,q_1,q_2 | ∃ a∈Σ:p_i,a,m_i,q_i∈Δ for  i=1,2}.

is a squared output automaton for T.

The squared automaton A^sq can be efficiently computed, see Algorithm <ref>.




Let A^2 be a squared output automaton for the monoidal finite-state transducer T. 
Let q_1,q_2∈ Q× Q be on a successful path in A^2, let 

    i_1,i_2,m_1,m_2,q_1,q_2∈Δ_2^*
 
for some initial state i_1,i_2∈ I× I. Then m_1,m_2 is called a relevant pair for q_1,q_2.  









Let 

    A^2 =  M× M,Q× Q,I× I,F× F,Δ_2
 
be a squared output automaton for the monoidal finite-state transducer T. 
A valuation of 
A^2 =  M× M,Q× Q,I× I,F× F,Δ_2 
is a pair of partial functions ρ,ν, ρ,ν : Q^2 → M^2 such that for each state q_1,q_2 of the squared automaton ρ(q_1,q_2) choses a relevant pair for q_1,q_2 if such a pair exists, and ρ(q_1,q_2) is undefined otherwise. 
If ρ(q_1,q_2) is defined and equalizable, then ν(q_1,q_2) returns a mge for ρ(q_1,q_2), otherwise ν(q_1,q_2) is undefined. 
In addition we require that 


  * if q_1,q_2∈ I^2, then ρ(q_1,q_2)=e,e,

  * and if the chosen relevant pair is m,m for some m, then ν returns e,e.

More formally:

    ρ(q_1,q_2) = {[                        e,e               q_1,q_2∈ I^2;                    m_1,m_2                   q_1,q_2,;                            q_1,q_2∉I^2 m_1,m_2q_1,q_2;                          !                            ].


    ν(q_1,q_2) = {[                        e,e !ρ(q_1,q_2) ρ(q_1,q_2)=m,m;              η(ρ(q_1,q_2))                !ρ(q_1,q_2);                          !                            ].




We can effectively compute a valuation of A^2.


Clearly e,e is a relevant pair for each initial state q ∈ I^2. Hence, since the monoid operation in M is computable, we can compute ρ by a straightforward traversal, say breadth-first search, of A^2. Since η is computable and the equality of elements of M is decidable, we can also effectively obtain ν. For technical details we refer to Algorithm <ref>. Note that in Algorithm <ref> the function Valuation assumes that the states in Q_2 are ordered in a breadth-first order as returned by the function SquaredAutomaton in Algorithm <ref>. The set C is the set of co-accessible states.




The following lemma is crucial for the bimachine construction method described below. 
Part 1 says that if T is functional, then we may associate with each state of a squared automaton a single mge which acts as a 
mge for all relevant pairs of the state. 


Let T be a trimmed monoidal finite-state transducer with output in the mge monoid M=M,∘,e.
Let A^2 be a squared automaton for T with valuation ρ,ν.
Then T is functional iff


  * for each relevant pair m_1,m_2 of a state p∈ Q^2 always ν(p) is a mge for m_1,m_2

  * for each final and accessible state f∈ F× F we have ν(f)=e,e. 




“⇒”: Let T be functional. 1. Let m_1,m_2 be a relevant pair for p=p_1,p_2∈ Q× Q. Therefore p lies on a successful path in A^2 and furthermore, there is an initial state s=s_1,s_2∈ I^2 such that s,m_1,m_2,p∈Δ_2^*. Since p lies on a successful path, 
there exists also a pair of final states f=f_1,f_2 and a tuple 
p,k_1,k_2,f∈Δ_2^*. Using that A^2 is a squared automaton for T, we conclude that there are words u,v∈Σ^* such that s_i,u,m_i,p_i∈Δ^* and p_i,v,k_i,f_i∈Δ^* for i=1,2.
This shows that uv,m_ik_i∈ L( T) for i=1,2 and since T is functional we get that
m_1k_1=m_2k_2 and k_1,k_2 is an equalizer for m_1,m_2. This implies that ρ(p) and ν(p) are defined. Let ρ(p)=m'_1,m'_2. Since T is functional k_1,k_2 is an equalizer of m'_1,m'_2 and therefore k_1,k_2 is a joint equalizer of m_1,m_2 and m'_1,m'_2. From Lemma <ref> it follows that ν(p) is a mge for m_1,m_2 as well.

2. In the special case where p∈ F× F, we can take k_1=k_2=e. Hence, each relevant pair for p has the form (m,m) and by Definition <ref> we have ν(p)=e,e.

“⇐”: If T is not functional, then for some input string w there are two distinct outputs m_1,m_2. Let 
m_i be produced on a path with input label w from an initial state s_i to the final state f_i (i=1,2). 
Since A^2 is a squared automaton for T, there is a path s_1,s_2,m_1,m_2,f_1,f_2∈Δ_2^*.
Thus, m_1,m_2 is a relevant pair for f_1,f_2. Obviously, f_1,f_2 is final and accessible in A^2. Since m_1≠ m_2 it follows that e,e is not a mge for m_1,m_2.


Let T be a trimmed monoidal finite-state transducer with output in the mge monoid M=M,∘,e.
Let A^2 be a squared automaton for T with valuation ρ,ν.
Then the following two conditions are equivalent:


  * for each relevant pair m_1,m_2 of a state p∈ Q^2 always ν(p) is a mge for m_1,m_2,

  * for all states p,q ∈ Q^2, such that ρ(p)=m_1,m_2 and ρ(q)=n_1,n_2 are defined and for each transition p,u_1,u_2,q∈Δ_2 always η(m_1 u_1,m_2 u_2) is a mge of ρ(q). 



(1 ⇒ 2) Since m_1 u_1, m_2 u_2 is a relevant pair of q it follows from Condition 1 that ν(q) is a mge of m_1 u_1, m_2 u_2 and of ρ(q). From Lemma <ref> it follows that η(m_1 u_1,m_2 u_2) is a mge for ρ(q) as well. 

(2 ⇒ 1) We assume that Condition 2 holds. Let m_1,m_2 be an arbitrary relevant pair of a state p=p_1,p_2∈ Q^2. Then m_1,m_2 is the label of a path with n∈ transitions in A^2. We prove Condition 1 by induction on n.

Let n=0. Then m_1,m_2=e,e and p ∈ I^2, thus ν(p) = e,e is a mge for m_1,m_2.

Let us assume that for every relevant pair m_1,m_2 of a state p ∈ Q^2 that is a label of a path with  n transitions in A^2 we have that ν(p) is a mge for m_1,m_2.

Let n'_1,n'_2 be a relevant pair of a state q∈ Q^2 that is the label of a path with n+1 transitions. Let the last transition of this path be p,u_1,u_2,q∈Δ_2. In this case there exists a pair m'_1,m'_2∈ M^2 such that n'_1=m'_1 u_1, n'_2=m'_2 u_2 and m'_1,m'_2 is a relevant pair of p, and is a label of a path with n transition. Let ρ(p)=m_1,m_2, ρ(q)=n_1,n_2 and η(m_1 u_1, m_2 u_2)=y'_1,y'_2. Then m_1 u_1 y'_1 = m_2 u_2 y'_2 and from Condition 2 we have that n_1 y'_1 = n_2 y'_2. Hence u_1y'_1,u_2y'_2 is an equalizer of m_1,m_2. From the induction hypothesis we have that ν(p) = x_1,x_2 is a mge for m_1,m_2 and m'_1,m'_2 and therefore u_1y'_1,u_2y'_2 will be an equalizer of m'_1,m'_2. Hence m'_1 u_1 y'_1 = m'_2 u_2 y'_2 thus y'_1,y'_2 is an equalizer of n'_1,n'_2. Since n_1,n_2 and n'_1,n'_2 have a joint equalizer, ν(q) is a mge for n'_1,n'_2. 

Now we can proceed with the functionality decision procedure, see also Algorithm <ref>.

Assume that M is an effective mge monoid. Then the functionality of a real-time transducer T=Σ, M,Q,I,Δ,T is decidable.


We proceed by first constructing the trimmed squared automaton A and a valuation for A. Afterwards for each transition in the trimmed squared automaton A we check Condition 2 of Proposition <ref>. If the check fails, then T is not functional. Otherwise the transducer is functional iff for every final state f ∈ F^2 we have that ν(f)=e,e.





The constraint on the original transducer to be a real-time entails the following complexity concern. In case that the original transducer is not real-time, we should perform a ε-closure procedure in advance. Whereas, this would not increase the number of states of the transducer, in the worst case this may lead to a squared increase of the number of transitions, |Δ| ∼ |Σ||Q|^2. This may harm the construction of the squared automaton and cause it to produce as many as |Σ| |Q|^4 transitions, whereas the original (not)real-time transducer may have had only O(|Σ||Q|) transitions.  


The following proposition suggests a solution for the concern raised by Remark <ref>. 
We use the notation introduced in Definition <ref>.


Let T=Σ^∗× M,Q,I,Δ,F be a  monoidal finite-state transducer. Then


  * the monoidal automaton

    A_e^2    =    M× M,Q× Q,I× I,F× F,Δ^e_2,  where
    Δ^e_2    =   {p_1,p_2,m_1,m_2,q_1,q_2 | ∃ a∈ (Σ∪{ε}) (p_i,a,m_i,q_i∈Δ^ext for  i=1,2)}

is a squared output automaton for T.

  * the monoidal automaton:

    A^2    =    M× M,Q× Q,I× I,F× F,Δ_2,  where
    Δ_2     =    {p_1,p_2,m_1,m_2,q_1,q_2 | ∃ a∈Σ (p_i,a,m_i,q_i∈Δ for  i=1,2)}
          ∪{p_1,p_2,e,m_2,p_1,q_2 |  (p_2,ε,m_2,q_2∈Δ)}
          ∪{p_1,p_2,m_1,e,q_1,p_2 |  (p_1,ε,m_1,q_1∈Δ)}

is a squared output automaton for T.



The first part is straightforward. For the second we prove Δ_2^*= (Δ_2^e)^*.
Let p_i,ε,m_i,q_i∈Δ^e. Then 

    p_1,p_2,e,m_2,p_1,q_2   ∈   Δ_2
    p_1,q_2,m_1,e,q_1,q_2   ∈   Δ_2.

Summing up we have that
p_1,p_2,m_1,m_2,q_1,q_2∈Δ_2^*.
Therefore Δ_2^e⊆Δ_2^*.
Since, obviously Δ_2⊆Δ_2^e, we get Δ_2^*=(Δ_2^e)^*. From the definition of a squared output automaton and Part 1 it follows that A^2 is a squared output automaton for T.
Thus applying the functional test to A^2 yields a functional test algorithm for arbitrary transducer T.




We can analyze the number of transitions in the modified squared automaton A^2 as follows.
Let

    Δ_a   =   {p,a,m,q∈Δ} for  a∈Σ∪{ε}

Then the number of transitions in the modified A^2 is bounded by:

    |Δ_2| ≤∑_a∈Σ |Δ_a|^2 + 2|Q| |Δ_ε|.

Thus, we get at most a squared increase of the number of transitions. This is an especially desired bound
in the case where the transducer is constructed from a regular expression. In this case we can apply ε-constructions for union, concatenation and iteration. Specifically, we arrive at a transducer with a linear number of transitions and states in terms of the original regular expression. This shows that the upper bound for |Δ_2| in this case would be only the square of the original regular expression. This compares favourably to the worst case scenario described in Remark <ref>.





§ BIMACHINE CONSTRUCTION BASED ON THE EQUALIZER ACCUMULATION PRINCIPLE


Let T=Σ^*× M,Q,I,Δ,F denote a functional transducer
with output in the effective mge monoid M=(M,∘,e). Without loss of generality we assume that η(e,e)=e,e. Further we  assume that ε,e∈ L( T) (cf. Remark <ref>).

In this section we show how to construct a bimachine with at most 2^|Q|+1 states that is equivalent to T.
Specifically, we prove:

If T is a functional real-time transducer, then there is a bimachine B= M, A_L, A_R,ψ such that A_L has at most 2^|Q| and A_R has at most 2^|Q| states and O_ B  = O_ T.


If T is an arbitrary functional transducer, then there is a bimachine B= M, A_L, A_R,ψ such that A_L has at most 2^|Q| and A_R has at most 2^|Q| states and O_ B  = O_ T.

In both cases, the left deterministic automaton A_L results from the determinization of the underlying automaton for T, whereas the right deterministic automaton A_R results from the determinization of the reversed underlying automaton for T. Of course, in the second case we adopt ε-power-set construction. The subtle part of the 
construction is the definition of the output function, ψ. It is in this part where the squared automaton, A^2, and the notion of mge's come into play.

We present our algorithm stepwise. First, we consider a special case and use it to informally describe our intuition and motivation for the construction. Sections <ref> and <ref> present the proof of Theorem <ref>. In Section <ref> we give the formal construction and we prove its correctness in Section <ref>. In Section <ref> we show that very subtle and natural amendments of our
construction yield the proof of Theorem <ref>.



 §.§ High-level description

To illustrate the idea of our algorithm, we consider an example where T is a functional real-time transducer with outputs in ℝ_≥ 0=(ℝ_≥ 0,+,0).

Let u=a_1… a_n be in the domain of T and consider

the ordinary, i.e. left-to-right, traversal of u in T, see Figure <ref>. It starts from the set of initial states, L_0=I, and gradually extends L_i to L_i+1 by following all the outgoing transitions from L_i labelled with input character a_i+1. Similarly, the reverse, i.e. right-to-left, traversal of u in T starts from R_n=F and stepwise turns back from R_i+1 to R_i by following all the incoming transitions in R_i+1 that are labelled with a_i+1. Jointly, L_i 
and R_i express that the successful paths traverse exactly the states S_i=L_i∩ R_i before scanning the character a_i+1. At 
the time step when a_i+1 is scanned, all these paths depart from S_i, follow a transition labelled a_i+1, and arrive in S_i
+1=L_i+1∩ R_i+1, see Figure <ref>.

Let us assume that S_i={p_1,p_2,p_3} and each of the states, p_j, is reached by a path π_j for j∈{1,2,3} labeled with a_1… a_i on the input. Assume that the path π_j produces an output c_j=cost(π_j). Let M_i=max(c_1,c_2,c_3) be the maximum over all the outputs c_j. We shall maintain the following invariant. By time step i, we will emit exactly the maximum, M_i. 

Our construction relies on the following observation.
Since each state p_j ∈ S_i lies on a successful path labeled with a_1… a_n for j∈{1,2,3} we can consider a path P_j with input label  a_i+1… a_n starting from p_j and terminating in a final state. Since the transducer T is functional, the outputs produced along these paths must coincide, i.e.:

    cost(π_j) +cost(P_j) =cost(π_k)+cost(P_k)  for all j,k∈{1,2,3}.   (†)

 
This implies that each state p_j∈ S_i can (precompute and) store its imbalance:

    v_S_i(p_j)=max(c_1,c_2,c_3)-c_j=M_i-c_j.

Note that the imbalances depend only on the set S_i and do not depend on the specific input a_1 … a_i. 
This follows from the equations (†) and the fact that the paths P_j do not depend on a_1 … a_i.
A similar argument applies to the set S_i+1. In our example S_i+1={q_1,q_2,q_3,q_4}. Thus, if four paths, π_1',π_2',π_3',π_4' reach q_1,q_2,q_3,q_4, respectively, with the same input, then for their costs, c_j'=cost(π_j') it holds that:

    v_S_i+1(q_j)=M_i+1-c'_j.





Now we select an arbitrary transition t_i=p,a_i+1,m_i+1,q∈Δ with p=p_j∈ S_i and q=q_k ∈ S_i+1. The path following π_j  through t_i has cost:

    c_k'=c_j+m_i+1 =M_i - (M_i-c_j)+m_i+1=M_i - v_S_i(p_j) +m_i+1
 
On the other hand:

    M_i+1=c_k'+v_S_i+1(q_k)=M_i - v_S_i(p_j)+m_i+1+v_S_i+1(q_k).

Hence:

    M_i+1-M_i=m_i+1+v_S_i+1(q_k) - v_S_i(p_j).

The right hand side of this expression does not depend on the specific transition we take from S_i to S_i+1 and can be expressed only locally in terms of the structure of T and the precomputed imbalances, v_S_i(p_j) and v_S_i+1(q_k) .

Using the above observation we construct the bimachine by first computing the left and right deterministic automata applying the standard determinization procedure to the underlying and the reversed underlying automaton. Then the output function is defined by setting ψ(L_i,a,R_i+1) = M_i+1-M_i.



 §.§ Formal construction

As before let T be a functional real-time transducer with outputs in the effective mge monoid 
M=(M,∘,e). Let η denote a function that computes a mge for each equalizable pair of M.   
The construction of the bimachine B for T uses five steps. 

Step 1.  We compute 
the squared output automaton 

    A^2 =  M× M,Q × Q,I × I,Δ_2,F × F

for T and a valuation ρ,ν for A^2 as described in 
Proposition <ref>, see the left part of Algorithm <ref>.

Step 2.  We compute the left and right deterministic automata for the bimachine, see Algorithm <ref>.
The left deterministic automaton is defined as the result 

    A_L = Σ, Q_L, s_L, Q_L, δ_L

when applying the standard determinization procedure[By the “standard” construction we mean the one that generates only the accessible states in the deterministic automaton.] to the underlying automaton of T. This means that Q_L ⊆ 2^Q, s_L = I and the transition function is defined as
δ_L(L,a) := q'∃ q ∈ L, m ∈ M : q,a,m,q'∈Δ.

The right deterministic automaton is defined as the result 

    A_R = Σ, Q_R, s_R, Q_R, δ_R
 when applying the standard 
determinization procedure to the reversed underlying automaton of  T. We have Q_R ⊆ 2^Q, s_R = F and
the transition function is defined as δ_R(R,a) := q∃ q' ∈ R, m ∈ M : q,a,m,q'∈Δ.

Step 3 (mge accumulation, see also Algorithm <ref>).  
Let 

    S ={L∩ R≠∅ |  L∈ Q_L, R∈ Q_R}
 




For each S∈ S we define a (partial) function ϕ_S: S→ M that represents a mge for S: 
fix any enumeration ⟨ p_1,p_2,…,p_k⟩ of the elements of S. Then

    ϕ_S(p_i)= γ_i^(k)(ν(p_1,p_2),…,ν(p_k-1,p_k))

where γ^(k):(M× M)^k-1→ M^k is the mge accumulation function introduced in  Corollary <ref>.  

Step 4.  
With these notions we now define the output function ψ:Q_L×Σ× Q_R→ M, see Algorithm <ref>. To define ψ(L,a,R') we proceed as follows: 


  * Let L' :=δ_L(L,a) and R := δ_R(R',a). If L∩ R=∅, 
      then ψ(L,a,R') is undefined. Otherwise

  * Let S=L∩ R and S'=L'∩ R'. 

  *  Let t=p,a,m,p'∈Δ be arbitrary with p∈ S and p'∈ S'. 

  * We define ψ(L,a,R'):=c, where c is the unique solution of the equation ϕ_S(p) ∘ c = m∘ϕ_S'(p') (cf. Corollary <ref>).



Step 5.  Finally, we define B := M, A_L, A_R,ψ.
















 §.§ Correctness for real-time functional transducers

We first show that Step 4 unambiguously defines the domain and the values of the output the function, ψ. 
Formally, we have the following proposition. 



Let A^2, A_L, and A_R be defined as in Steps 1 and 2 above. Assume that L,L'∈ Q_L, R,R'∈ Q_R and a∈Σ satisfy

    L'=δ_L(L,a)  and  R=δ_R(R',a)

and let S=L∩ R and S'=L'∩ R'. If S ≠∅, then:


  * for each state p∈ S there exists a transition t=p,a,m,p' with p'∈ S'.

  * c=ψ(L,a,R') is well-defined and for every transition τ=p_τ,a,m_τ,p'_τ with p_τ∈ S and p'_τ∈ S' it holds:

    ϕ_S(p_τ) c=m_τϕ_S'(p'_τ) .







1. Let p∈ S. Since S=L∩ R, and R=δ_R(R',a) by the determinization construction of A_R there is a transition  t=p,a,m,p'∈Δ with p'∈ R'. Since p∈ L from the determinization construction of A_L we get that p'∈δ_L(L,a)=L'. Therefore p'∈ L'∩ R'=S' as required.

2. Let u be such that L=δ_L^∗(s_L,u). Let S={p_1,…,p_k}. Then there exist s_1,…,s_k ∈ I and n_1,…,n_k ∈ M such that s_j,u,n_j,p_j∈Δ^∗ for each 1 ≤ j ≤ k. Using Point 1, for each j≤ k we fix a transition t_j=p_j,a,m_j,p'_j∈Δ such that p'_j ∈ S'. Let τ=p_τ,a,m_τ,p'_τ with p_τ∈ S and p'_τ∈ S'  be arbitrary. In particular, p_τ=p_i for some i≤ k.

Let v be such that R'=δ_R^∗(s_R,v^rev). Then there exist f_1,…,f_k,f_τ∈ F and n'_1,…,n'_k,n'_τ∈ M such that p'_j, v,n'_j,f_j∈Δ^∗ for 1 ≤ j ≤ k and p'_τ,v,n'_τ,f_τ∈Δ^*. Since the transducer is functional we have that n_1 m_1 n'_1 = … = n_k m_k n'_k=n_i m_τ n'_τ. Therefore n_1 m_1,…,n_k m _k,n_i m_τ and n_1,…,n_i are equalizable. From Lemma <ref> we get that ν(p_j,p_j+1) is a mge for n_j,n_j+1. Thus, if x_j=ϕ_S(p_j) for j≤ k by Corollary <ref> we get that ϕ_S=x_1,…,x_k is a mge of n_1,…,n_k. Similarly, if y_j=ϕ_S'(p_j') and y_τ=ϕ_S'(p'_τ) we get
that y_1,…,y_k,y_τ is an equalizer for n_1m_1,…,n_km_k,n_i m_τ. Hence, m_1y_1,…,m_ky_k,m_τ y_τ is an equalizer for n_1,…,n_k,n_i. Therefore there exists c∈ M such that x_j c =m_j y_j for j≤ k and
further x_i c=m_τ y_τ. Recalling that x_j=ϕ_S(p_j), y_j=ϕ_S'(p_j') and y_τ=ϕ_S'(p'_τ) we get:

    ϕ_S(p_j) c = m_j ϕ_S'(p'_j)  for  j ≤ k  and ϕ_S(p_τ) c =m_τϕ_S'(p'_τ).

By the discussion above we know that this system has a solution. Hence each of the equations has an unique solution (cf. Lemma <ref>) and therefore the solution is uniquely defined by any of the equations. Hence, ψ(L,a,R') is well defined.
  




 Let 𝒯 and B be as above and u=a_1… a_n∈Σ^+. Then:
 
 
  * if u,m∈ L( T), then O_ B(u)=m.
 
  * O_ B=O_ T.
 
 
 
 
 
  * Since u,m∈ L( T) there is a successful path:
 
    p_0,a_1,m_1,p_1…p_n-1,a_n,m_n,p_n in  T.

 In particular, p_0∈ I, p_n∈ F, and m=m_1∘ m_2…∘ m_n.
 Let L_i=δ_L^*(s_L,a_1… a_i) and R_i=δ^*_R(s_R,a_n… a_i+1).
By the power-set determinization construction of A_L and A_R it follows
that p_i∈ L_i and p_i∈ R_i. Let S_i=L_i∩ R_i. Hence S_i≠∅ for
all i≤ n. By Proposition <ref>, Point 2, it follows that:

    c_i+1   =   ψ(L_i,a_i+1,R_i+1)  is well-defined and 
    ϕ_S_i(p_i) c_i+1    =    m_i+1ϕ_S_i+1(p_i+1).

Now a straightforward computation shows that:


    ϕ_S_0(p_0) c_1 c_2 … c_n = m_1 ϕ_S_1(p_1) c_2 c_3 … c_n = ⋯ = m_1 m_2… m_n ϕ_S_n(p_n).


Since S_0⊆ I, we have that for all p_0',p_0”∈ S_0, ν(p_0',p_0”)=e,e. Therefore, since
η(e,e)=e,e by Remark <ref>, we get ϕ_S_0(p_0)=e for all p_0∈ S_0. Similarly, since S_n⊆ F all the states in S_n are final. By the functionality test we have that ν(p_n',p_n”)=e,e for all p_n',p_n”∈ S_n. Again, since η(e,e)=e,e, by Remark <ref> ϕ_S_n(p_n)=e.
Therefore:

    O_ B(u)=c_1 … c_n=m_1 … m_n=m.


  * First, O_ B(ε)=ε=O_ T(ε) by our convention in the beginning of the section. By the first part, we have that O_ T⊆ O_ B. Conversely, if u∈( B) and u∈Σ^+ it follows that δ^*_L(s_L,u)∩ s_R≠∅. By the power-set construction of A_L and since s_R=F this means that there is a successful path labelled by u in T. Hence,
u∈( T). 
 


Since by Step 2 of the construction, A_L and A_R have at most 2^|Q| states,
the result follows by Theorem <ref>. 



 §.§ Non-real-time functional transducers

Next, we turn our attention to the general case, where the functional transducers is not necessarily real-time.
The main issue to be addressed are the ε,m-transitions. Nevertheless, very natural amendments
to the construction from Section <ref> yield the result of Theorem <ref>.
We start with the following verbatim modification:

Step 1-ε.  See Step 1. For the construction of a squared automaton in this case
we apply Propostion <ref>.

Step 2-ε.  See Step 2. The only difference here is that we apply a ε-power-set determinization to obtain:

    A_L = Σ, Q_L, s_L, Q_L, δ_L
     A_R = Σ, Q_R, s_R, Q_R, δ_R

Specifically, Q_L⊆ 2^Q contains only accessible states, s_L=I, and for all L∈ Q_L and a∈Σ:

    δ_L(L,a) := q'∃ q ∈ L, m ∈ M : q,a,m,q'∈Δ^*.

Similarly, Q_R⊆ 2^Q contains only accessible states, s_R=F, and for all R∈ Q_R and a∈Σ:

    δ_R(R,a) := q'∃ q ∈ R, m ∈ M : q',a,m,q∈Δ^*.

Step 3-ε.  See Step 3.

Step 4-ε.  See Step 4. 

Step 5-ε.  Finally, we define B := M, A_L, A_R,ψ.

With these changes we can prove the following modification of Proposition <ref>:

Let A^2, A_L, A_R and ϕ be defined as in Steps 1-ε, 2-ε and 3-ε above. Assume that L,L'∈ Q_L, R,R'∈ Q_R and a∈Σ satisfy

    L'=δ_L(L,a)  and  R=δ_R(R',a)

and let S=L∩ R and S'=L'∩ R'. If S ≠∅, then:


  * for each state p∈ S there is a generalized transition t=p,a,m,p'∈Δ^* with p'∈ S'.

  * there is c∈ M such that for every generalized transition τ=q,a,λ,q'∈Δ^* with q∈ S and q'∈ S':

    ϕ_S(q) c=λϕ_S'(q').




See the proof of Proposition <ref>. 

However, Proposition <ref> is not enough to establish the correctness of Theorem <ref>.
The problem is that in Step 4, and thus in Step 4-ε, we select an ordinary transition t=p,a,m,p'∈Δ and not a generalized p,a,m,p'∈Δ^* as in Proposition <ref>.
The following lemma shows that we can select an ordinary transition in Step 4-ε. 


Let L be a state in A_L, R' be a state in A_R, and a∈Σ.
If R=δ_R(R',a) and L'=δ_L(L,a) are such that, S=R∩ L≠∅
and S'=L'∩ R', then there exists a transition t=p,a,m,p'∈Δ such that p ∈ S and p'∈ S'.


Let q∈ S=R∩ L. Then there is a state q'∈ R' with q,a,m',q'∈Δ^*.
Since q∈ L it follows that q'∈ L'. Hence q'∈ L'∩ R'=S'. Fix a path π form q to q'
with label a,m'. Let t=p,a,m,p' be the unique transition on π with input
label a∈Σ. It follows that q,ε,m_1,p∈Δ^* and p',ε,m_2,q'∈Δ^*. Since q∈ L, we get that p∈ L. Since q'∈ R' we obtain that p'∈ R'. Now the transition
t with p'∈ R' shows that p∈ R=δ_R'(R',a), and thus p∈ L∩ R=S. Similarly, since p∈ L
the transition t witnesses that p'∈ L'=δ_L'(L,a) and therefore p'∈ L'∩ R'. 

 
O_ B'=O_ T.


If u=ε, then by convention we have that O_ B'(ε)=e=O_ T(ε).
For u∈Σ^+, we can repeat the proof of Theorem <ref> where we use Proposition <ref>
and Lemma <ref> instead of Proposition <ref>. We omit the details.


By construction, A_L and A_R have at most 2^|Q| states. Now the result follows by Theorem <ref>.



§ COMPARISON TO PREVIOUS BIMACHINE CONSTRUCTIONS


In this section we show that our construction outperforms previous methods for building bimachines from functional transducers.
After a brief discussion of the standard bimachine construction in <cit.> we introduce a class of real-time functional transducers with n+2 states for which the standard bimachine construction generates a bimachine with at least Θ(n!) states. 
The present construction based on the equalizer accumulation principle leads to 
2^n + n +3 states. 



 §.§ Classical Construction

A comprehensive outline of the standard bimachine construction can be found elsewhere, <cit.>.
Here we follow <cit.> and provide only the basic ideas, stressing the main properties of the construction that are relevant for our discussion.

The classical construction of bimachines <cit.> refers to the special case where M=Ω^*,∘,ε is the free monoid generated by an alphabet Ω. As described in <cit.>, but see also the proofs in <cit.>, it departs from a pseudo-deterministic transducer, i.e. a transducer T=Σ×Ω^*,Q,I,F,Δ that can be considered as a deterministic finite-state automaton over the new alphabet Σ×Ω^*. This means that I contains a single state i and Δ is a finite graph of a function Q× (Σ×Ω^*)→ Q. 

The next step is the core of the construction. The goal is to construct an unambiguous transducer T' with transition relation Δ' equivalent to T. This is achieved by specializing the standard determinization construction for finite-state automata: the sets generated by the determinization procedure are split into two parts, a single guessed positive state – this is our positive hypothesis for the successful path to be followed, and a set of negative states – these are the alternative hypotheses that must all fail in order for our positive hypothesis to be confirmed. Formally, the states in the resulting transducer are pairs p,N∈ Q× 2^Q. The initial state is i'=i,∅. The algorithm inductively defines transitions in Δ' and states in Q'. Let ≺_lex denote the lexicographic order on Ω^*. 
Let p,N be a generated state and p,a,v,p'∈Δ. 
Let 

    N' := {q' | ∃ q∈ N, ∃ v':q,a,v',q'∈Δ}∪{q  | ∃ v'≺_lex v:p,a,v',q∈Δ}.

If p' ∉N' we introduce a state p',N' and a transition  

    p,N,a,v,p',N'∈Δ'.








Intuitively, this transition makes a guess about the lexicographically smallest continuation of the output that can be followed to a final state f∈ F. Accordingly, all transitions that have the same input character, a, but lexicographically smaller output, are implicitly assumed to fail. 
To reflect this, we add those states to the set of negative hypotheses, N'. 
To maintain the previously accumulated 
 negative hypotheses along the path to p,N the a-successors of N are added to N'. Following these lines, the set of final states of T' is defined as:
 
    F'={f,N |  f∈ F  and  N∩ F=∅}.

 
Note that f,N becomes final only if f∈ F and there is no final state n∈ N 
 reached with smaller output on a parallel path.  
 It can be formally shown, <cit.>, that this construction indeed leads to an unambiguous transducer:
 
    T'=Σ×Ω^*,Q',{i'},F',Δ'

equivalent to T.

The final step is to convert the (trimmed part of) T' in an equivalent bimachine. This can be easily done by a determinization of A_L= A_ T',D and A_R= A_T'^rev_D and defining an appropriate output function ψ:Q_L×Σ× Q_R→Ω^*. 



 §.§ A special class of transducers


The following example introduces a class of transducers that demonstrates the advantages of the new bimachine 
construction. 


We consider the class of transducers, see also Figure <ref>:

    T_n := Σ^*_n×{1}^*,Q,{s},{f},Δ_n

where Σ_n  =  {a_1,a_2,…,a_n}, Q :=  {s,q_1,q_2,…,q_n,f} and 
the transition relation Δ_n :=  Δ_s,n∪Δ_Q_n∪Δ_f,n has three types of transitions: 

    Δ_s,n :=  {s,a_j,1^i-1,q_i |  i≤ n, j ≤ n}
 
are transitions from the start state 
s to the states in the “intermediate layer” Q_n:= {q_1,q_2,…,q_n}. 
Δ_Q_n is the graph of the function δ_Q_n:Q_n×Σ_n→ 1^* × Q_n defined as 

    δ_Q_n(q_i,a_j) = 1^n,q_i if  i∉{1,j}
    1^n+j-1,q_j if  i=1 
    1^n-j+1,q_1 if  i=j(≠ 1).

and describes transitions between states in the intermediate layer Q_n. 
Finally Δ_f,n is the graph of the function 

    δ_f,n(q_i,a_j)=1^2n-i+1,f if  j≤ i
    undefined, else

and describes transitions from the intermediate layer to the final state f. 
For a given input string each transducer T_n outputs a sequence of letters 1. 
See Figure <ref> for an illustration. 




Before we analyze the set of bimachine states obtained from the standard and the new construction method we first summarize some 
simple properties.


T_n is an ambiguous quasi-deterministic functional real-time transducer.


1. T_n is quasi-deterministic: Clearly, Δ_s,n is a graph of a function from s×Σ_n^*× 1^*. 
Furthermore the elements of Δ_s,n have first coordinate s, whereas all the entries in Δ_f,n∪Δ_Q_n
have first coordinate in Q_n. Thus, it remains to show Δ_f,n∪Δ_Q_n is a graph of a function δ:Q_n ×Σ_n × 1^* → Q_n∪{s,f}. 
However, Δ_f,n and Δ_Q_n are graphs of functions δ_f,n and δ_Q_n, respectively. Furthermore if q_i,a_j is in the domain of both functions, then

    δ_f,n(q_i,a_j)=1^2n-i+1,f and δ_Q_n(q_i,a_j)∈{1^n-i+1,q_1,1^n,q_i}.

Since 2n-i+1≥ n+1>n≥ n-i+1 we conclude that the first coordinates of the results of these two functions are distinct.
Therefore, T_n is quasi-deterministic. 

2. For every path s,α,1^k,q_i∈Δ^* we have

    α∈Σ_n^+  and  k=n (|α|-1) +i-1.

This follows by a straightforward induction on the length of the path. We easily conclude that 
T_n is a real-time quasi-deterministic functional transducer with language

    L( T_n)={α,1^n|α| | α∈Σ_n^*∖Σ_n}.

It is also clear that for each word in Σ_n^+ {a_1} there are n distinct successful paths in T_n, thus T_n is ambiguous. 


The next property is crucial for our analysis.


 For each permutation π:Q_n→ Q_n there
 is a word α_π∈ A^* such that for all q,q'∈ Q_n:
 
    q,α_π,.,q'∈Δ^*  q'=π(q).



For each j, the function δ_Q_n(q_i,a_j) induces a permutation on Q_n.
 Specifically, it maps each state q∉{q_1,q_j} to itself, and it transposes q_1 and q_j.
 Thus, we can identify the action of a_j on Q_n with the transposition σ_1,j:Q_n→ Q_n:

    σ_1,j(q_i)=
    q_i  if  i∉{1,j}
    
    q_j  if  i=1 
    
    q_1  if  i=j.

The transpositions σ_1,j generate the entire permutation group on Q_n. Therefore for each
permutation π:Q_n→ Q_n, there is a word α_π∈Σ_n^* such that for all q,q'∈ Q_n:

    q,α_π,.,q'∈Δ^* q'=π(q').



We first look at the number of states of the bimachine obtained from the new construction based on the equalizer accumulation principle.

For each n:


  * the determinization of the underlying automaton of T_n generates 3 states.

  * the determinization of the reversed underlying automaton of T_n generates 2^n+n states.



1. The first part is immediate - the states are given by the three sets {s}, Q_n, Q_n∪{f}.

2. As for the second, part, let N_i={q_1,…,q_i-1} for 1≤ i≤ n. We note that the reversed determinization constructs:


  * one initial state, {f},

  * n non-final states Q_n∖ N_i.

  * each state Q_n∖ N_i gives rise to the sets P∪{s} where P⊆ Q_n where |P|=n-i.

The first two claims are obvious. For the third claim, first notice that for each state q_i in the intermediate layer and each letter a_j we always come back to the start state s using a reverse transition. For the states of the intermediate layer Q_n, each letter a_j induces a permutation (s.a.). Hence, ignoring s, backward transitions always lead from a set with n-i states of Q_n to another set with n-i states of Q_n. Lemma <ref> shows that each subset of n-i states of Q_n is reached from Q_n∖ N_i using a series of backward transitions, which proves the third claim. 







We conclude that the number of states generated by the determinization of the reversed underlying automaton of T_n is

    1 + n + ∑_i=1^n nn-i=1+n+(2^n-1)=2^n + n.














































































































































The next proposition shows that the number of states of the bimachine obtained when using the classical construction for 
converting the transducers T_n is much larger than for the new construction. 



Let T'_n be the trimmed result of the specialized determinization of T_n described in Subsection <ref>. Then


  * T'_n has at least (2n+3)2^n-2 states.

  * The determinization of the underlying automaton of T_n' generates at least n!+2 states.

  * The determinization of the reversed underlying automaton of T_n' generates at least 2^n+n states.


The proof of Proposition <ref> is given in the Appendix. The reason for the large number of states obtained when using the specialized determinization of T_n is that it distinguishes words α that correspond to different permutations on Q_n. This circumstance forces the determinization of the underlying automaton of T'_n to generate states that correspond to all the permutations of Q_n. Meanwhile, the determinization of the reversed underlying automaton of T'_n behaves timidly and, combinatorically, it is equivalent to the reversed determinization of T_n that we analyzed in Lemma <ref>.


Similar arguments show that the bimachine construction introduced in Section 4 of  <cit.> shares the same lower bound of Θ(n!) for the number of states when used for the class of transducers T_n introduced in Example <ref>.



























Summing up results we obtain the following theorem:

For any positive integer n, on input T_n the standard bimachine construction generates at least (n!+2)+(2^n+n) states, whereas
the construction proposed in Section <ref> generates a bimachine with 3+(2^n+n) states. 




§ CONCLUSION


In this paper we introduced a new method for converting functional transducers into bimachines. 
The method can be applied to all functional transducers where the output monoid belongs to 
the class of mge monoids introduced in Section <ref>. From our point of view this class, which was shown to be closed under Cartesian products, deserves interest on its own. An effective functionality decision procedure is given for transducers with output in effective mge monoids.

Unlike other methods, the new bimachine construction does not try to imitate in a bimachine run a particular path of the transducer. Rather, the squared output transducer and the principle of equalizer accumulation are used to obtain a unified view on all 
parallel paths of the transducer for a particular input. The bimachine output for a partial input sequence corresponds to the maximal output across all the outputs obtained in the parallel transducer paths. 

The advantage of the new construction method is space economy. The number of states of the bimachine is bounded by 
2· 2^n where n is the number of transducer's states. In <cit.> it has been shown that the size of bimachines obtained when using other methods based on transducer path reconstruction is in O(n!). Further we showed that the standard construction can achieve a worst case complexity Θ(n!) on a class of transducers with n+2 states.
We are not aware of any known method with better space complexity. 

We additionally introduced a natural amendment of the construction that can be directly applied to arbitrary non-real-time functional transducers. This construction avoids the complexity increase caused by the blow-up of the number of transitions when 
first building a real-time transducer.

splncs03




§ APPENDIX


We prove Proposition <ref>. 


1. First, since s,∅ is the initial state of T'_n the initial transitions, a_j,1^i for any a_j ∈Σ_n
generate the pairs:

    P_i=q_i,N_i,  where  N_i={q_1,…,q_i-1}.

for each i≤ n. Furthermore, q_i has a transition with a_i to f whereas none of the states in N_i has a transition with a_i to f. Therefore P_i is also co-accessible in T'_n.

Let p∈ Q_n and S⊆ Q_n be arbitrary such that p∉S. Then |S|=i-1 for some i≤ n.
Therefore there is a permutation
π:Q_n→ Q_n such that π(q_i)=p and[If C⊆ Q_n, π(C) is the set of π(c) for c∈ C.] π(N_i)=S. Following Lemma <ref> let α_π be a word that realizes the permutation π. Hence, starting from P_i and following the word α_π the construction will define a state P_i,π such that:

    P_i,π=π(q_i),π(N_i)∪{f}=p,S∪{f} or  P_i,π=π(q_i),π(N_i)=p,S.

Let β be the word that corresponds to π^-1. Thus starting from P_i,π and following the word β the determinization of T_n must reach the state q_i,N_i or q_i,N_i∪{f}. Since f has no transitions,
we deduce that both of them are co-accessible implying that also P_i,π is co-accessible. 

Furthermore, if i>1, then α_πa_1 generates also the pair p,S∪{f} since a_1 corresponds to the identity on Q_n and every state has a transition with a_1 to f. On the other hand, if q_1∉S and l is the maximal index of a state q_l∈ S, then α_πa_la_l generates first p,(S∖{q_l})∪{q_1,f} and then p,S∖{f} because there is a transition from q_1 with a_l to q_l but (by the maximality of l) none of the states in S-q_l has a transition with a_l to f.

By the above discussion for each state p∈ Q_n and every set ∅⊂ S⊆ Q_n∖{q}, the pair p,S∪{f} is a state in T_n'. Clearly, there are n(2^n-1-1) such pairs. 
Next, we count the pairs p,S such that p∈ Q_n and S⊆ Q_n. First, if S≠∅, then p,S∪{f} is a state in T_n'. Now, assume that p=q_j and ∅≠ S⊆ N_j∖{q_1}. Let l me the maximal index of a state in S. Then the word a_la_l maps S∪{f} to S. For each j there are 2^j-2-1 sets ∅≠ S⊆ N_j∖{q_1}. Summing over j=2,3…,n we get

    ∑_j=2^n (2^j-2-1)=2^n-1 - 1 - (n-1)=2^n-1 - n.

Finally, each of the pairs q_j,∅ is also in T_n' and we have the initial state s,∅ and q_j,N_j for j>1 add up to:

    n(2^n-1-1) + 2^n-1 - n + 2n= (n+1)2^n-1

non-final states.

Finally, if S_j⊆ N_j is arbitrary there is an accessible state q_j,S_j' with S_j'∖{f}=S_j. Now a transition with a_j shows that f,S_j ∪{q_1} is final. Therefore for every set S⊆ N_n that contains q_1 there is final state f,S. Therefore T_n' has at least 2^n-2 final states. Summing up we see that T_n' has at least:

    (n+1)2^n-1 + 2^n-2=(2n+3)2^n-2

states.

2. For the second part, we prove that to different permutations π:Q_n→ Q_n we can assign different states in the left automaton A_L. To achieve this, let π:Q_n→ Q_n be some permutation. We consider the α_π as defined in Lemma <ref>. Without loss of generality we can assume that |α_π|≥ 1. First, it is easy to see that

    δ_L(s,∅,a_1)= {q_i,N_i |  i≤ n}.
 
Next, following the word α_π each state q_i,N_i will reach some non-final states and some final states.
The set of non-final states reached by q_i,N_i will be:

    ∅≠ P_i,π⊆{π(q_i),π(N_i), π(q_i),π(N_i)∪{f}}.

Hence, the states π(q_i),S_i∈ P_i,π have their first coordinate in Q_n, 
whereas their second coordinate, say S_i, has the property |S_i∩ Q_n|=i-1.
Meanwhile, the final states reached by q_i,N_i have a first coordinate f∉Q_n.

This analysis shows that for every π we have

    δ_L^*(s,∅,a_1α_π)=⋃_i=1^nP_i,π∪ F_π
  
where F_π≠∅ is some set of elements with first coordinate[The precise form F_π can be expressed in terms of the pairs P_i,π and the last character of α_π. Yet, it is not important for our analysis.] f. Now, we claim that if π'≠π” are two permutations, then

    L_π'=⋃_i=1^nP_i,π'∪ F_π' and  L_π”=⋃_i=1^nP_i,π”∪ F_π”

are distinct sets. Indeed, let j≤ n be such that π'(q_j)≠π”(q_j). By the above analysis there is a pair π'(q_j),S'_j∈ L_π' with |S'_j ∩ Q_n|=j-1. Now, if π'(q_j),S_j'∈ L_π”, then π'(q_j)=π”(q_i) for some i and again by the above analysis we conclude that |S_j'∩ Q_n| =i-1. Hence, i=j implying that π'(q_j)=π”(q_j). This is a contradiction.

Therefore, all the states L_π' are distinct states. All of them are final, since |a_1α_π|≥ 2, and the domain of
T_n contains all these words. Additionally, A_L must contain two more states, i.e. the initial state {s,∅} and also:

    δ_L({s,∅},a_1)={q_i,N_i |  i≤ n}.

Hence, in total, A_L contains at least n!+2 states. 

3. Let s_R=F' be the set of final states of T'_n. For j≤ n let R_j and R_j' be the sets:

    R_j = δ_R(s_R,a_j)  and  R_j'={q | ∃ S( q,S∈ R_j)}.

Then, we deduce that R_j consists of all the pairs q_i,S such that i≥ j, q_i,S is accessible in T'_n, S-f ⊆ N_j, and i≥ j. Therefore R_j'=Q_n∖ N_j since a_j∉ T_n.

Let π be an arbitrary permutation on Q_n, π:Q_n→ Q_n and let α_π that realizes π. Without loss of generality we may assume that |α|≥ 1. We consider the sets:

    R_j,π=δ_R^*(R_j,α_π)  and R'_j,π={q | ∃ S(q,S∈ R_j)}.

Now, since α^rev a_j ∈( T_n) we must have that s,∅∈ R_j,π and it should be clear that:

    R'_j,π={s}∪π(R_j').

Now since π was arbitrary, we deduce for any subset R'⊂ Q_n, R'≠∅, there is a state, some state
R in the right automaton A_R such that:

    R'={s}∪{q∈ Q_n | ∃ S (q,S∈ R)}.

Therefore there are at least 2^n-1 states R that all contain s,∅. Adding the initial state, s_R and the n states R_j for j≤ n, we conclude that the right automaton A_R has at least:

    1+n+(2^n -1)=2^n +n

states.
 
