Synthesis of deterministic top-down tree transducers from automatic tree relations (Q515670): Difference between revisions

This contribution discusses the problem of extracting a deterministic top-down tree transducer, which computes a function, from an efficiently presented relation such that the function computed by the transducer is a subset of the given relation when restricted to the domain of the relation. This problem is also known as uniformization. Here, the relation is presented by a top-down tree automaton that accepts trees in a particular format that represent tree pairs. Such a tree pair is essentially encoded into a single tree by overlaying the two pairs adding a special empty symbol for positions that only exist in one of the trees. The authors distinguish two modes. Either the top-down tree transducer is required to compute a function that has the same domain as the relation or its outputs can be arbitrary on elements outside of the domain of the relation. The decision procedures for the uniformization problem discussed here assume the second mode in which the tree transducer can behave arbitrarily on inputs outside of the domain of the relation. The problem is first solved for top-down tree transducers with bounded delay, which means that the tree transducer can only use a bounded number of rules in sequence that consume part of the input but do not produce part of the output. The problem is reduced to a safety two-player game which is known to be decidable. For the case of unbounded delay, which is obtained by transducers that erase an input symbol and continue processing a single subtree of the input tree, an additional observation is necessary that shows which relations can be uniformized by such behavior. Finally, it remains to detect instances of this behavior, and then another reduction to a two-player game is presented that yields decidability. If the domain of the computed function needs to coincide with the domain of the relation, then the presented results do not carry over and a decidability result is only provided for a very particular kind of top-down tree transducers. Overall, the paper is very well written, but assumes some background in tree language and tree transducer theory. Pointers to the relevant literature are provided and proofs are presented in full detail, so the contribution should be understandable to any graduate computer science student with some effort.