XML type checking with macro tree transducers
XML type checking with macro tree transducers
复制标题
使用宏树转换器进行 XML 类型检查
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
H. Seidl
中科院分区：
文献类型：
--
作者：
S. Maneth;A. Berlea;T. Perst;H. Seidl
基于未排序树的MSO逻辑被认为是一个方便的理论框架，用于推理实用XML查询语言的表达能力和实现。作为XML转换语言的相应理论基础，提出了“转换语言”TL。这种语言基于Maneth和Neven的“文档转换语言”DTL，它包含了完整的MSO模式匹配，在输入树中使用MSO模式的任意导航，以及命名过程。新语言通过额外允许过程在参数中积累中间结果来推广DTL。事实证明，TL -因此，特别是DTL -尽管他们的表现力仍然允许有效的逆类型推理。这个结果是通过翻译TL程序到组合物的自上而下的有限状态树转导参数，也被称为（停留）宏树换能器。
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.