ABSTRACT Recently, much attention has been drawn on exact typechecking for non-Turing-complete XML transformation languages, such as XSLT and XML-QL. Milo, Suciu, and Vianu proposed a notion of k-pebble tree transducers, a powerful and general framework that can express most of transformations in such languages, and showed that its exact typechecking is decidable in time hyper-exponential to the number,k of pebbles. Although the problem is intractable in theoretical point of view, it remains unclear that its practical e‐ciency is so. In this work, we investigate, through experiments, the practical e‐ciency of their method with respect to XSLT through experiments. Our typechecker consists of: (1) a converter from XSLT programs to k-pebble tree transducers, and (2) a typechecker for k-pebble tree transducers. As their method,relies on decidability of WSkS (weak second-order monadic,logic with k successors), we use MONA, an e‐cient implementation of WSkS solver, in (2). We show and discuss the results from our experiments using, as inputs, several XSLT programs that are actually used. 論文要旨 近年、特に,XSLT や XML-QL などのチューリング・マシンより表現力の低い,XML 変換言語の
分享
引用
