XML type checking with macro tree transducers

ABSTRACT

MSO logic on unranked trees has been identified as a convenient theoretical framework for reasoning about expressiveness and implementations of practical XML query languages. As a corresponding theoretical foundation of XML transformation languages, the "transformation language" TL is proposed. This language is based on the "document transformation language" DTL of Maneth and Neven which incorporates full MSO pattern matching, arbitrary navigation in the input tree using also MSO patterns, and named procedures. The new language generalizes DTL by additionally allowing procedures to accumulate intermediate results in parameters. It is proved that TL -- and thus in particular DTL - despite their expressiveness still allow for effective inverse type inference. This result is obtained by means of a translation of TL programs into compositions of top-down finite state tree transductions with parameters, also called (stay) macro tree transducers.

REFERENCES

• 1: S. Abiteboul, P. Buneman, and D. Suciu. Data on the Web. Morgan Kaufmann, 2000.
• 2: Véronique Benzaken , Giuseppe Castagna , Alain Frisch, CDuce: an XML-centric general-purpose language, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.51-63, August 25-29, 2003, Uppsala, Sweden
• 3: A. Berglund and S. Boag et. al., editors. XML Path Language (XPath) 2.0. W3C Working Draft, World Wide Web Consortium, November 2003. Available online http://www.w3.org/TR/xpath20.
• 4: A. Berlea and H. Seidl. fxt - A Transformation Language for XML Documents. Journal of Computing and Information Technology, 10(1):19--35, 2002.
• 5: Roderick Bloem , Joost Engelfriet, Monadic Second Order Logic and Node Relations on Graphs and Trees, Structures in Logic and Computer Science, A Selection of Essays in Honor of Andrzej Ehrenfeucht, p.144-161, January 1997
• 6: S. Boag and D. Chamberlin et. al., editors. XQuery 1.0: An XML Query Language. W3C Working Draft, World Wide Web Consortium, November 2003. Available online http://www.w3.org/TR/xquery/.
• 7: J. Clark and S. DeRose, editors. XML Path Language (XPath) 1.0. W3C Recommendation, World Wide Web Consortium, November 1999. Available online http://www.w3.org/TR/xpath.
• 8: J. Clark and M. Murata et al. RelaxNG Specification. OASIS. Available online http://www.oasis-open.org/committees/relax-ng.
• 9: J. Clark, editor. XSL Transformations (XSLT) 1.0. W3C Recommendation, World Wide Web Consortium, November 1999. Available online http://www.w3.org/TR/xslt.
• 10: Joost Engelfriet , Sebastian Maneth, Macro tree transducers, attribute grammars, and MSO definable tree translations, Information and Computation, v.154 n.1, p.34-91, Oct. 10, 1999 [doi>10.1006/inco.1999.2807]
• 11: J. Engelfriet and S. Maneth. A Comparison of Pebble Tree Transducers with Macro Tree Transducers. Acta Inf., 39:613--698, 2003.
• 12: J. Engelfriet and S. Maneth. Macro Tree Translations of Linear Size Increase are MSO Definable. SIAM J. Comput., 32:950--1006, 2003.
• 13: J. Engelfriet and B. Samwel. Personal communication (work in progress). 2004.
• 14: J. Engelfriet and H. Vogler. Macro Tree Transducers. J. of Comp. Syst. Sci., 31:71--146, 1985.
• 15: J Engelfriet , H Vogler, Pushdown machines for the macro tree transducer, Theoretical Computer Science, v.42 n.3, p.251-368, June 1986
• 16: D.C. Fallside, editor. XML Schema. W3C Recommendation, World Wide Web Consortium, 2 May 2001. Available online http://www.w3.org/TR/xmlschema-0/.
• 17: M.J. Fisher. Grammars with Macro-like Productions. PhD thesis, Harvard University, Massachusetts, 1968.
• 18: A. Frisch. Regular Tree Language Recognition with static Information, 2004. PLAN-X 2004.
• 19: Zoltan Fulop , H. Vogler, Syntax-Directed Semantics: Formal Models Based on Tree Transducers, Springer-Verlag New York, Inc., Secaucus, NJ, 1998
• 20: Haruo Hosoya , Benjamin C. Pierce, XDuce: A statically typed XML processing language, ACM Transactions on Internet Technology (TOIT), v.3 n.2, p.117-148, May 2003 [doi>10.1145/767193.767195]
• 21: M. Kay, editor. XSL Transformations (XSLT) 2.0. W3C Working Draft, World Wide Web Consortium, November 2003. Available online http://www.w3.org/TR/xslt20.
• 22: A. Kühnemann and H. Vogler. Synthesized and Inherited Functions. A new Computational Model for Syntax-Directed Semantics. Acta Inf., 31:431--477, 1994.
• 23: S. Maneth. The Macro Tree Transducer Hierarchy Collapses for Functions of Linear Size Increase. In Proc. FSTTCS'03, pages 326--337. LNCS 2914, Springer-Verlag, 2003.
• 24: Sebastian Maneth , Frank Neven, Structured Document Transformations Based on XSL, Revised Papers from the 7th International Workshop on Database Programming Languages: Research Issues in Structured and Semistructured Database Programming, p.80-98, September 01-03, 1999
• 25: Wim Martens , Frank Neven, Frontiers of tractability for typechecking simple XML transformations, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France [doi>10.1145/1055558.1055563]
• 26: E. Meijer and M. Shields. XML: A Functional Language for Constructing and Manipulating XML Documents. 1999. Available online http://www.cse.ogi.edu/~mbs/pub/xmlambda/.
• 27: Tova Milo , Dan Suciu , Victor Vianu, Typechecking for XML transformers, Journal of Computer and System Sciences, v.66 n.1, p.66-97, 01 February 2003 [doi>10.1016/S0022-0000(02)00030-2]
• 28: A. Møller and M. I. Schwartzbach. The Design Space of Type Checkers for XML Transformation Languages. In Proc. ICDT'05, 2005. To appear.
• 29: M. Murata, D. Lee, and M. Mani. Taxonomy of XML Schema Languages using Formal Language Theory. In Proc. Extreme Markup Languages 2000, 2000.
• 30: A. Neumann and A. Berlea. fxgrep 4.0. Source Code, 2004.
• 31: Frank Neven, Automata theory for XML researchers, ACM SIGMOD Record, v.31 n.3, September 2002 [doi>10.1145/601858.601869]
• 32: Thomas Perst , Helmut Seidl, Macro forest transducers, Information Processing Letters, v.89 n.3, p.141-149, 14 February 2004 [doi>10.1016/j.ipl.2003.05.001]
• 33: J. W. Thatcher and J. B. Wright. Generalized Finite Automata with an Application to a Decision Problem of Second Order Logic. Mathematical Systems Theory, 2:57--82, 1968.
• 34: Akihiko Tozawa, Towards static type checking for XSLT, Proceedings of the 2001 ACM Symposium on Document engineering, November 09-10, 2001, Atlanta, Georgia, USA [doi>10.1145/502187.502191]