×

Forward and backward application of symbolic tree transducers. (English) Zbl 1307.68047

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 [M. Veanes and 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 [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 [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 [G. Rozenberg (ed.) and A. Salomaa (ed.), Handbook of formal languages. Vol. 1–3. Berlin: Springer (1997; Zbl 0866.68057)].

MSC:

68Q45 Formal languages and automata
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alon, N., Milo, T., Neven, F., Suciu, D., Vianu, V.: XML with data values: typechecking revisited. J. Comput. Syst. Sci. 66(4), 688-727 (2003) · Zbl 1054.68035
[2] Baker, B.S.: Composition of top-down and bottom-up tree transductions. Inform. Control 41(2), 186-213 (1979) · Zbl 0408.68053 · doi:10.1016/S0019-9958(79)90561-8
[3] Barrero, A.: Unranked tree languages. Pattern Recognit. 24, 9-18 (1991) · doi:10.1016/0031-3203(91)90112-I
[4] Brambilla, M., Ceri, S., Comai, S., Fraternali, P., Manolescu, I.: Specification and design of workflow-driven hypertexts. J. Web Eng. 2, 163-182 (2003)
[5] Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In Proceedings of 16th International Symposium on Fundamentals of Computation Theory (FCT’07), volume 4639 of Lecture Notes in Comput. Sci., pp. 1-22. Springer (2007) · Zbl 1135.68467
[6] Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. Theoret. Comput. Sci. 295, 85-106 (2003) · Zbl 1053.68060 · doi:10.1016/S0304-3975(02)00397-3
[7] Brüggemann-Klein, A., Murata, M., Wood, D.: Regular tree and regular hedge languages over unranked alphabets: Version 1, April 2001. Technical Report HKUST-TCSC-2001-0. The Hongkong University of, Science and Technology (2001)
[8] Brainerd, W.S.: Tree generating regular systems. Inform. Control 14, 217-231 (1969) · Zbl 0169.31601 · doi:10.1016/S0019-9958(69)90065-5
[9] Brüggemann-Klein, A., Wood, D.: Regular tree languages over non-ranked alphabets. http://citeseer.ist.psu.edu/br98regular.html (1998) · Zbl 0912.68112
[10] Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata (1997) · Zbl 0169.31601
[11] David, C., Libkin, L., Tan, T.: Efficient reasoning about trees via integer linear programming. ACM Trans. Database Syst. 37(3), 19 (2012) · doi:10.1145/2338626.2338632
[12] Doner, J.: Tree acceptors and some of their applications. J. Comput. Syst. Sci. 4, 406-451 (1970) · Zbl 0212.02901 · doi:10.1016/S0022-0000(70)80041-1
[13] Engelfriet, J., Maneth, S.: A comparison of pebble tree transducers with macro tree transducers. Acta Inform. 39(9), 613-698 (2003) · Zbl 1060.68062 · doi:10.1007/s00236-003-0120-0
[14] Engelfriet, J.: Bottom-up and top-down tree transformations—a comparison. Math. Syst. Theory 9(3), 198-231 (1975) · Zbl 0335.68061 · doi:10.1007/BF01704020
[15] Fülöp, Z., Vogler, H.: Syntax-Directed Semantics—Formal Models Based on Tree Transducers. Monogr. Theoret. Comput. Sci. EATCS Ser. Springer (1998) · Zbl 0913.68127
[16] Grumberg, O.; Kupferman, O.; Sheinvald, S.; Martin-Vide, C. (ed.); Dediu, A-H (ed.); Fernau, H. (ed.), Variable automata over infinite alphabets, 561-572 (2010), NY · Zbl 1284.68352
[17] Gécseg, F., Steinby, M.: Tree Automata. Akadémiai Kiadó, Budapest (1984) · Zbl 0537.68056
[18] Gécseg, F.; Steinby, M.; Rozenberg, G. (ed.); Salomaa, A. (ed.), Tree languages, 1-68 (1997), Berlin · doi:10.1007/978-3-642-59126-6_1
[19] Kaminski, M.; Tan, T.; Avron, A. (ed.); etal., Tree automata over infinite alphabets, 386-423 (2008), Berlin · Zbl 1133.68364
[20] Maneth, S., Berlea, A., Perst, T., Seidl, H.: XML type checking with macro tree transducers. In: Proceedings of 24th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2005), pp. 283-294. ACM Press (2005) · Zbl 0408.68053
[21] Mens, I.-E., Rahonis, G.: Variable tree automata over infinite ranked alphabets. In: Winkler, F. (ed.) 4th International Conference on Algebraic Informatics (CAI 2011), volume 6742 of Lecture Notes in Compter Science, pp. 247-260. Springer (2011) · Zbl 1339.68152
[22] Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. J. Comput. Syst. Sci. 66, 688-727 (2003) · Zbl 1054.68035 · doi:10.1016/S0022-0000(02)00030-2
[23] Murata, M.: Forest-regular languages and tree-regular languages. Unpublished notes (1995)
[24] Rounds, W.C.: Mappings and grammars on trees. Math. Syst. Theory 4(3), 257-287 (1970) · Zbl 0203.30103 · doi:10.1007/BF01695769
[25] Tan, T.: An automata model for trees with ordered data values. In: Proceedings of 27th Annual IEEE/ACM Symposium on Logic in Computer Science Pages (LICS), pp. 586-595 (2012) · Zbl 1361.68124
[26] Thatcher, J.W.: Characterizing derivation trees of context-free grammars through a generalization of finite automata theory. J. Comput. Syst. Sci. 1(4), 317-322 (1967) · Zbl 0155.01802 · doi:10.1016/S0022-0000(67)80022-9
[27] Thatcher, J.W.: Generalized \[^22\] sequential machine maps. J. Comput. Syst. Sci. 4(4), 339-367 (1970) · Zbl 0198.03303 · doi:10.1016/S0022-0000(70)80017-4
[28] Veanes, M., Bjorner, N.: Foundations of finite symbolic tree transducers. Bull. EATCS 105, 141-173 (2011) · Zbl 1257.68100
[29] Veanes, M., Bjorner, N.: Symbolic tree transducers. In: Proceedings of Perspectives of System Informatics (PSI 11), volume 7162 of LNCS, pp. 371-387. Springer (2011) · Zbl 1257.68100
[30] Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite transducers: algorithms and applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12), pp. 137-150. ACM SIGPLAN (2012) · Zbl 1321.68341
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.