Forward and backward application of symbolic tree transducers (Q404011)

In several areas of computing, elements from infinite domains occur as labels in trees. The most popular such application is certainly XML where parsed character data can occur as leaf label. In the present contribution the authors essentially revisit [\textit{M. Veanes} and \textit{N. Bjørner}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 105, 141--173 (2011; Zbl 1257.68100)] and extend traditional finite-state models for tree languages (regular tree grammars and tree automata) and tree transformations (top-down tree transducers) to a setting in which infinitely many tree node labels are possible. Diverging from the title, this contribution considers the models obtained in this way, which are called ``symbolic'', and investigates their basic properties including the promised forward and backward application. The exposition starts with symbolic tree automata, which are essentially classical tree automata [\textit{J. W. Thatcher}, J. Comput. Syst. Sci. 1, 317--322 (1967; Zbl 0155.01802)], but instead of an input symbol in the rules those automata have a predicate over the (potentially) infinite label set. A classical rule is applicable when exactly the input symbol from the rule is encountered in the input tree (and the state behaviour matches as well). The new rules are similarly applicable (with the same result) whenever the currently considered input symbol in the input tree fulfills the predicate. To keep the manipulations of such automata effective, the predicates are required to be recursive with decidable emptiness problem. In effect, each new rule is a stand-in for the (potentially infinitely many) classical rules that are obtained by replacing the predicate by an input symbol that fulfills the predicate. The authors proceed by showing (a family of) simple tree languages over an infinite label set that cannot be recognized by those symbolic tree automata, and using this result, demonstrate that the classes of tree languages recognized by symbolic tree automata and variable tree automata are incomparable. Following the stand-in intuition mentioned above, the authors characterize the tree languages recognized by symbolic tree automata as the images of the traditional recognizable tree languages under special relabellings. This demonstrates that the algorithmic motor of symbolic tree automata remains that of a classical tree automaton, but it has additional freedom when interpreting the input symbols. These results are complemented with the expected normalization result for symbolic regular tree grammars, which, as in the non-symbolic case, can be transformed into an equivalent symbolic tree automaton. This is achieved by decomposing the rules containing more than one input predicate into several rules each containing a single predicate using the states to ensure that those newly formed rules are applied in the correct sequence. The second major model considered are symbolic tree transducers. This model extends the classical top-down tree transducer [\textit{W. C. Rounds}, Math. Syst. Theory 4, 257--287 (1970; Zbl 0203.30103)] using a variant of the symbolic approach already discussed. As in the case of automata, instead of the input symbol each rule of such a transducer now contains a predicate on the (potentially) infinite label set. However, on the output side, the output symbols are replaced by functions from the set of input labels to the set of output labels. An instance of such a rule is obtained in two steps: First we replace the predicate in the input side by an input symbol~\(\sigma\) that fulfills the predicate. Second, we replace the function symbols in the output side by the result of applying the corresponding functions to~\(\sigma\). Again, the rule of a symbolic tree transducer is a stand-in for all rules obtained in this manner. Consequently, the rules are applied in essentially the same manner as for traditional tree transducers, but instead of applying a rule directly we apply a suitable instance of it. The authors demonstrate this relationship to traditional top-down tree transducers, but the analogue to the relabelling result for symbolic tree automata is missing, although an analogous result probably holds when looking at a bimorphism representation. Additionally, composition results that correspond exactly to those for classical top-down tree transducers are presented and the promised results for forward and backward application are derived from them. Overall, the paper is well written but very technical. A good exposition to the classical devices is necessary to appreciate and understand the relevant constructions. A suitable introduction into the classical theory can be found in [\textit{G. Rozenberg} (ed.) and \textit{A. Salomaa} (ed.), Handbook of formal languages. Vol. 1--3. Berlin: Springer (1997; Zbl 0866.68057)].