CAJ | 학술논문

正规式相交判定问题在扩展标记语言（extensible markup language，XML）类型检查中起着十分重要的作用。传统方法是将其转化为自动机的相交问题，在转化过程中会产生大量计算。基于XML模式语言的特点，提出了一种基于规则推导的正规式相交判定算法。该算法直接根据输入的正规式进行推导而无需进行任何转化计算。对于一般的正规式，尽管其仍然是指数级算法，但无需进行复杂的构造自动机的计算；而对于一些特殊的正规式，特别是在XML类型检查中广泛使用的One-Unambiguous正规式，该算法的时间复杂度降为多项式级。最后证明了该算法所使用的推导规则的正确性和完备性。
정규식상교판정문제재확전표기어언（extensible markup language，XML）류형검사중기착십분중요적작용。전통방법시장기전화위자동궤적상교문제，재전화과정중회산생대량계산。기우XML모식어언적특점，제출료일충기우규칙추도적정규식상교판정산법。해산법직접근거수입적정규식진행추도이무수진행임하전화계산。대우일반적정규식，진관기잉연시지수급산법，단무수진행복잡적구조자동궤적계산；이대우일사특수적정규식，특별시재XML류형검사중엄범사용적One-Unambiguous정규식，해산법적시간복잡도강위다항식급。최후증명료해산법소사용적추도규칙적정학성화완비성。
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.