关键词: XML类型检查, 正规式, 相交判定, 推导规则

Abstract: Decision problem of intersection checking for regular expressions plays an important role in the extensible markup language (XML) type checking. The typical technique converts the problem of intersection checking into the problem of automata intersection, which may generate a lot of redundant computing during the conversion. According to the features of XML schema languages, this paper proposes a new intersection checking algorithm based on inference system for regular expressions. This algorithm is derived directly based on regular expressions without any conversion. For general regular expressions, this algorithm is an exponential time algorithm, but without constructing automata, and for some special cases, especially for the One-Unambiguous regular expression used in XML type checking, it is the polynomial time algorithm. Finally, this paper proves the correctness and completeness of the inference rules.

Key words: XML type checking, regular expression, intersection checking, inference rule