Equivalence of finite-valued tree transducers is decidable

A bottom-up finite state tree transducer (FST) M is called k-valued iff for every input tree there are at most k different output trees. M is called finite-valued iff it is k-valued for some k. We show that it is decidable for every k whether or not a given FST M is k-valued. We give an effective characterization of all finite-valued FSTs and derive a (sharp) upper bound for the valuedness provided it is finite. We decompose a finite-valued FST M into a finite number of single-valued FSTs. This enables us to prove: it is decidable whether or not the translation of an FST M is included in the translation of a finite-valued FST M'. We also consider these questions for size-valuedness.