Transformation of XML Documents with Higher-Order Matching based on Higher-Order Rewrite Systems

本研究的目的是给出一个基于高阶重写系统的可表达的XML转换框架。我们的研究成果之一是提供了一类适合于XML转换的高阶重写系统，并研究了其类型论性质。我们发现，将上下文，即带有空洞的术语扩展为二阶项，适合于XML文档的高阶模式匹配。我们还引入了一种新的类型系统，称为不完全正则表达式类型，它是通过将上下文的概念适应于正则表达式类型而获得的。这种类型系统对于灵活类型的高阶模式匹配是必不可少的，因为在从XML术语提取模式和从模式合成XML术语时，不完整正则表达式类型中出现的漏洞可以用任意类型实例化。在上述术语和类型系统的基础上，我们设计了一类高阶项重写系统…并通过XML转换的例子说明了它的用处。我们还证明了该类型系统具有静态的重写规则类型检查能力。另一个研究成果是设计了一种针对二阶模式的XML文档术语表示的模式匹配算法，并研究了它的理论性质。我们设计了基于所谓的变换方法的算法，该方法定义了一组推理规则，用于变换表示模式匹配问题的方程序列。我们发现，二阶匹配的推理规则是由一阶匹配的自然推广而来的。研究了模式匹配算法的性质，证明了算法的可靠性和完备性，为研究具有重写技术的XML变换的性质提供了理论基础。由于重写技术适用于研究汇流和终止等性质，因此我们的研究结果有助于研究XML转换的这些性质。较少

The aim of the research is to give an expressive XML transformation framework based on higher-order rewrite systems.One of our research results is that we have provided a class of higher-order rewrite systems suitable for XML transformation and have investigated type-theoretic properties. We have found that regarding contexts, i.e., terms extended with holes, as second-order terms are suitable for higher-order pattern matching of XML documents. We have also introduced a novel type system called incomplete regular expression type, which is obtained by adapting the notion of contexts to regular expression types. This type system is indispensable for a flexible typed higher-order pattern matching because holes occurring in incomplete regular expression types can be instantiated with arbitrary types in extracting patterns from XML terms and in composing XML terms from patterns. Based on the terms and the type system mentioned above, we designed a class of higher-order term rewriting system … More and illustrated its usefulness by examples of XML transformations. We have also proved that the type system enjoys static type checking of rewrite rules.Another research result is that we have designed a pattern matching algorithm of term representations of XML documents against second-order patterns and have investigated its theoretical properties. We designed the algorithm based on so-called transformation method, which is defined with a set of inference rules that transform sequences of equations that represent pattern matching problems. We have found that inference rules for second-order matching are derived from the first-order matching as their natural extension. Investigating properties of the pattern matching algorithm, we have proved its soundness and completeness.The obtained research results give theoretical foundation for the investigation of properties of XML transformation with rewriting techniques. Because Rewriting techniques are suitable for studying properties such as confluence and termination, our research results are helpful in investigating such properties of XML transformation. Less