XML查询和更新语言的正则表达式子类型
Regular Expression Subtyping for XML Query and Update Languages
摘要：
XML数据库查询语言（如XQuery）使用具有结构子类型的正则表达式类型。子类型系统通常有两种表现形式，它们应该是等价的：一种是声明性版本，其中包含规则可以在任何地方使用，另一种是算法版本，其中包含规则的使用受到限制，以便使类型检查语法导向和可判定。然而，XQuery标准类型系统通过对迭代构造使用不精确的类型规则并仅定义算法类型检查来规避这个问题，另一个现存的提议为迭代构造提供了更精确的类型，但忽略了子类型。在本文中，我们考虑一个核心的类XQuery语言的包容规则，并证明算法的类型检查的完整性，这是简单的XQuery正确的，但需要一些照顾更精确的迭代类型的纪律存在。我们将这一结果扩展到我们在早期工作中介绍的XML更新语言。
英文摘要：
XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be equivalent: a declarative version in which the subsumption rule may be used anywhere, and an algorithmic version in which the use of subsumption is limited in order to make typechecking syntax-directed and decidable. However, the XQuery standard type system circumvents this issue by using imprecise typing rules for iteration constructs and defining only algorithmic typechecking, and another extant proposal provides more precise types for iteration constructs but ignores subtyping. In this paper, we consider a core XQuery-like language with a subsumption rule and prove the completeness of algorithmic typechecking; this is straightforward for XQuery proper but requires some care in the presence of more precise iteration typing disciplines. We extend this result to an XML update language we have introduced in earlier work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
