Single-valuedness of tree transducers is decidable in polynomial time

A bottom-up finite-state tree transducer (FST) A is called single-valued iff for every input tree there is at most one output tree. We give a polynomial-time algorithm which decides whether or not a given FST is single-valued. The algorithm is based on: • the freedom of the submonoid of trees which contain at least one occurrence of one variable *; • the succinct representation of trees by graphs; • a sequence of normalizing transformations of the given transducer; and • a polynomially decidable characterization of pairs of equivalent output functions. We apply these methods to show that finite-valuedness is decidable in polynomial time as well.