A survey on decidable equivalence problems for tree transducers (Q2800413)

This survey discusses three main approaches to prove that equivalence is decidable for various classes of deterministic tree transducers. Tree transducers are formal models that compute relations on trees and functions from trees to trees in the deterministic case. The restriction to deterministic models is reasonable since for most nondeterministic tree transducers the equivalence problem is undecidable (by a straightforward lift of the corresponding result for string transducers). As expected, the equivalence problem asks whether two given transducers compute the same relation.NEWLINENEWLINEThe first approach is based on the bounded balance property, which was used to prove decidability of equivalence for deterministic top-down tree transducers by \textit{Z. Esik} [Acta Cybern. 5, 1--20 (1980; Zbl 0456.68098)]. The technique was borrowed from the string setting and the survey also quickly recalls the classical string setting and shows that equivalent string transducers have the property that the length difference of the partially produced outputs of both input devices is bounded. This translates rather directly into a corresponding property for the height difference of equivalent top-down tree transducers. An alternative method based on a normal form that outputs symbols as soon as possible is also presented. In this normal form, equivalent transducers become isomorphic after the identification of equivalent states. The second approach works for deterministic macro tree transducers that are linear size increase. Such a macro tree transducer is a top-down tree transducer that additionally might use accumulating parameters, and the restriction to linear size increase requires that each output is linearly bounded in the size of the corresponding input. It is first shown that the output string languages of certain finite-copying tree transducers under regular input tree languages are Parikh. A clever encoding of the tree transducers yields a language that contains words of the form \(a^nb^n\) if and only if the input transducers are not equivalent. Since the encoding is Parikh, it can be intersected with the language containing all words that contain an equal number of \(a\)s and \(b\)s. This intersection is empty if and only if the input transducers are equivalent, and the emptiness of semilinear sets can be decided. The final approach for monadic macro tree transducers, which are restricted to an input and output alphabet that contains only nullary and unary symbols, relies on a reduction to the sequence equivalence problem for HDT0L.NEWLINENEWLINEOverall, the survey is excellently written, contains many illustrative examples, high-level arguments, and references to the original results for reference. Some exposure to string and tree transducers is required to fully appreciate the details of the construction, but the survey provides ample resources to the relevant literature. Equivalence problems have been reinvigorated recently and the survey also quickly discusses the latest developments albeit in less detail. Finally, it also provides some complexity results and an interesting outlook.