基于规则推导的正规式相交判定算法

ＩＳＳＮ　１６７３．９４１８　ＣｏＤＥＮ　ＪＫＹＴＡ８　Ｊｏｕｒｎａｌ　ｏｆ　Ｆｒｏｎｔｉｅｒｓ　ｏｆ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ　１６７３－９４１８／２０１５／０９（０１）－００４３－０８　ｄｏｉ：１０．３７７８￣．ｉｓｓｎ．１６７３－９４１８．１４０７０４２　Ｅ—ｍａｉｌ：ｆｃｓｔ＠ｖｉｐ．１６３．ｃｏｍ　ｈｔｔｐ：／／ｗｗｗ．ｃｅａｊ．ｏｒｇ　Ｔｅｌ：＋８６．．１０．－８９０５６０５６　基于规则推导的正规式相交判定算法　刘嘉　，廖湖声　北京．Ｙ－－，Ａｋ大学计算机学院，北京１００１２４　Ｉｎｔｅｒｓｅｃｔｉｏｎ　Ｃｈｅｃｋｉｎｇ　ｆｏｒ　Ｒｅｇｕｌａｒ　Ｅｘｐｒｅｓｓｉｏｎｓ　Ｂａｓｅｄ　ｏｎ　Ｉｎｆｅｒｅｎｃｅ　Ｓｙｓｔｅｍ　ＬＩＵ　Ｊｉａ￣，ＬＩＡＯ　Ｈｕｓｈｅｎｇ　Ｃｏｌｌｅｇｅ　ｏｆ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ，Ｂｅｉｊｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ｔｅｃｈｎｏｌｏｇｙ，Ｂｅｉｊｉｎｇ　１　００　１　２４，Ｃｈｉｎａ　＋Ｃｏｒｒｅｓｐｏｎｄｉｎｇ　ａｕｔｈｏｒ：Ｅ－ｍａｉｌ：ｊｅｒｏｍｅｌｉｕ＠ｅｍａｉｌｓ．ｂｊｕｔ．ｅｄｕ．ｃａ　ＬＩＵ　Ｊｉａ，ＬＩＡＯ　Ｈｕｓｈｅｎｇ．Ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ　ｆｏｒ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ　ｂａｓｅｄ　ｏｎ　ｉｎｆｅｒｅｎｃｅ　ｓｙｓｔｅｍ．Ｊｏｕｒｎａｌ　ｏｆ　Ｆｒｏｎｔｉｅｒｓ　ｏｆ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ，２０１５，９（１）：４３－５０．　Ａｂｓｔｒａｃｔ：Ｄｅｃｉｓｉｏｎ　ｐｒｏｂｌｅｍ　ｏｆ　ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ　ｆｏｒ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ　ｐｌａｙｓ　ａｎ　ｉｍｐｏｒｔａｎｔ　ｒｏｌｅ　ｉｎ　ｔｈｅ　ｅｘｔｅｎｓｉｂｌｅ　ｍａｒｋｕｐ　ｌａｎｇｕａｇｅ（ＸＭＬ）ｔｙｐｅ　ｃｈｅｃｋｉｎｇ．Ｔｈｅ　ｔｙｐｉｃａｌ　ｔｅｃｈｎｉｑｕｅ　ｃｏｎｖｅｒｔｓ　ｔｈｅ　ｐｒｏｂｌｅｍ　ｏｆ　ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ　ｉｎｔｏ　ｔｈｅ　ｐｒｏｂｌｅｍ　ｏｆ　ａｕｔｏｍａｔａ　ｉｎｔｅｒｓｅｃｔｉｏｎ，ｗｈｉｃｈ　ｍａｙ　ｇｅｎｅｒａｔｅ　ａ　ｌｏｔ　ｏｆ　ｒｅｄｕｎｄａｎｔ　ｃｏｍｐｕｔｉｎｇ　ｄｕｒｉｎｇ　ｔｈｅ　ｃｏｎｖｅｒｓｉｏｎ．　Ａｃｃｏｒｄｉｎｇ　ｔｏ　ｔｈｅ　ｆｅａｔｕｒｅｓ　ｏｆ　ＸＭＬ　ｓｃｈｅｍａ　ｌａｎｇｕａｇｅｓ，ｔｈｉｓ　ｐａｐｅｒ　ｐｒｏｐｏｓｅｓ　ａ　ｎｅｗ　ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ　ａｌｇｏｒｉｔｈｍ　ｂａｓｅｄ　ｏｎ　ｉｎｆｅｒｅｎｃｅ　ｓｙｓｔｅｍ　ｆｏｒ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ．Ｔｈｉｓ　ａｌｇｏｒｉｔｈｍ　ｉｓ　ｄｅｒｉｖｅｄ　ｄｉｒｅｃｔｌｙ　ｂａｓｅｄ　ｏｎ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ　ｗｉｔｈｏｕｔ　ａｎｙ　ｃｏｎｖｅｒｓｉｏｎ．Ｆｏｒ　ｇｅｎｅｒａｌ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ，ｔｈｉｓ　ａｌｇｏｒｉｔｈｍ　ｉｓ　ａｎ　ｅｘｐｏｎｅｎｔｉａｌ　ｔｉｍｅ　ａｌｇｏｒｉｔｈｍ，ｂｕｔ　ｗｉｈｏｕｔ　ｔｃｏｎｓｔｒｕｃｔｉｎｇ　ａｕｔｏｍａｔａ，ａｎｄ　ｆｏｒ　ｓｏｍｅ　ｓｐｅｃｉａｌ　ｃａｓｅｓ，ｅｓｐｅｃｉａｌｌｙ　ｆｏｒ　ｔｈｅ　Ｏｎｅ－Ｕｎａｍｂｉｕｏｕｓ　ｇｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎ　ｕｓｅｄ　ｉｎ　ＸＭＬ　ｔｙｐｅ　ｃｈｅｃｋｉｎｇ，ｉｔ　ｉｓ　ｔｈｅ　ｐｏｌｙｎｏｍｉａｌ　ｔｉｍｅ　ａｌｇｏｒｉｔｈｍ．Ｆｉｎａｌｌｙ，ｔｈｉｓ　ｐａｐｅｒ　ｐｒｏｖｅｓ　ｔｈｅ　ｃｏｒｒｅｃｔｎｅｓｓ　ａｎｄ　ｃｏｍｐｌｅｔｅｎｅｓｓ　ｏｆ　ｈｅ　ｉｎｆｅｒｅｎｃｅ　ｒｕｌｅｓ．ｔ　Ｋｅｙ　ｗｏｒｄｓ：ＸＭＬ　ｔｙｐｅ　ｃｈｅｃｋｉｎｇ；ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎ；ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ；ｉｎｆｅｒｅｎｃｅ　ｒｕｌｅ　摘要：正规式相交判定问题在扩展标记语言（ｅＸｔｅｎｓｉｂｌｅ　ｍａｒｋｕｐ　ｌｎｇａｕａｇｅ，ｘＭＬ）类型检查中起着十分重要的　作用。传统方法是将其转化为自动机的相交问题，在转化过程中会产生大量计算。基于ＸＭＬ模式语言的特　点，提出了一种基于规则推导的正规式相交判定算法。该算法直接根据输入的正规式进行推导而无需进行任　Ｔｈｅ　Ｎａｔｕｒａｌ　Ｓｃｉｅｎｃｅ　Ｆｏｕｎｄａｔｉｏｎ　ｏｆ　Ｂｅｉｊｉｎｇ　ｏｆ　Ｃｈｉｎａ　ｕｎｄｅｒ　Ｇｒａｎｔ　Ｎｏ．４０８２００３（北京市自然科学基金）．　Ｒｅｃｅｉｖｅｄ　２０１４・０６，Ａｃｃｅｐｔｅｄ　２０１４－０８．　ＣＮＫＩ网络优先出版：２０１４－０８—１８，ｈｔｔｐ：／／ｗｗｗ．ｃｎｋｉ．ｎｅｔ／ｋｃｍｓ／ｄｏｉ／１０．３７７８￣．ｉｓｓｎ．１６７３．９４１８．１４０７０４２．ｈｔｍｌ　４４　Ｊｏｕｒｎａｌ　ｏｆＦｒｏｎｔｉｅｒｓ　ｏｆＣｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ计算机科学与探索　何转化计算。对于一般的正规式，尽管其仍然是指数级算法，但无需进行复杂的构造自动机的计算；而对于一　些特殊的正规式，特别是在ＸＭＬ类型检查中广泛使用的Ｏｎｅ．Ｕｎａｍｂｉｇｕｏｕｓ正规式，该算法的时间复杂度降为　多项式级。最后证明了该算法所使用的推导规则的正确性和完备性。　关键词：ＸＭＬ类型检查；正规式；ｆｉｎ交判定；推导规则　文献标志码：Ａ　中图分类号：ＴＰ３１１　１　引言　在过去的几十年中，以关系理论ｎ　为核心的ＳＱＬ　（ｓｔｒｕｃｔｕｒｅｄ　ｑｕｅｒｙ　ｌａｎｇｕａｇｅ）数据库凭借其严谨的数学　基础、简单的结构化数据模型和非过程化的查询语　言等诸多优点，在企业信息管理领域一直占有主导地　位。然而，随着近年来以社交网络和电子商务为代表　的互联网技术的蓬勃发展，传统的ＳＱＬ数据库因其　难以表示和查询网络上大量的复杂类型数据，而愈　加不能满足当今大数据时代的企业信息管理需求，　海量的非结构化数据的到来及其持续增长已经是一　个不争的事实。扩展标记语言　（ｅｘｔｅｎｓｉｂｌｅ　ｍａｒｋｕｐ　ｌａｎｇｕａｇｅ，ＸＭＬ）的出现正是针对这一问题而提出的　解决方案。由于其具有数据表示灵活和互操作性强　等诸多ＳＱＬ数据库所不可比拟的优点，在企业数据　集成和互联网在线服务等领域得到了广泛的应用。　ＸＭＬ事实上已经成为数据交换的标准、ＳＯＡ（ｓｅｒｖｉｃｅ—　ｏｒｉｅｎｔｅｄ　ａｒｃｈｉｔｅｃｔｕｒｅ）架构的基石，并且在新兴的云计　算和物联网领域中扮演着越来越重要的角色。　正如ＳＱＬ数据库用ＤＤＬ（ｄａｔａ　ｄｅｆｉｎｉｔｉｏｎ　ｌａｎｇｕａｇｅ）　定义关系模式，ＸＭＬ文档同样需要某种语言定义ＸＭＬ　模式，使得符合该模式的ＸＭＬ文档满足相应的语法约　束。目前已基于正规树文法（ｒｅｇｕｌａｒ　ｔｒｅｅ　ｇｒａｍｍａｒ）ｔ　提　出了多种类型化ＸＭＬ模式语言，例如ＣＤｕｃｅｔ４１、ＸＭＬ　Ｓｃｈｅｍａｔ　、Ｘｔａｔｉｃｔ　、ＸＤｕｃｅｔ　、Ｒｅｌａｘ　Ｃｏｒｅｔ　和ＴＲＥＸｔ　等。ＸＭＬ类型检查问题就是通过确定或指派文档中　各元素的类型关系来检验该ＸＭＬ文档是否满足相应　的ＸＭＬ模式定义。一般地，不希望ＸＭＬ文档中的元　素在某个ＸＭＬ模式定义中具有二义性类型，即该元　素可以同时被指派两个或多个类型，因为这会极大　地增加ＸＭＬ类型检查的计算复杂度。根据正规树文　法，ＸＭＬ模式定义可以转化为一组包含产生式的表达　式，这些产生式由Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓｔ　ｌｉｅ规式所定义，　每个产生式唯一地对应ＸＭＬ文档中的某个元素类　型。若某个ＸＭＬ元素有二义性类型，则该元素同时　满足多个产生式，也就是说这些产生式包含的正规式　存在相交问题。　判定正规式是否相交的传统方法是先将两个正　规式转换为非确定性自动机（ｎｏｎ—ｄｅｔｅｒｍｉｎｉｓｔｉｃ　ｆｉｎｉｔｅ　ａｕｔｏｍａｔａ，ＮＦＡ），再转换为确定性自动机（ｄｅｔｅｒｍｉｎｉｓｔｉｃ　ｉｆｎｉｔｅ　ａｕｔｏｍａｔａ，ＤＦＡ），进一步求出这两个确定性自动　机的交集。对于一般的正规式，该算法的计算复杂　度是指数级的，同时还需要进行正规式与自动机的　转换。　本文针对ＸＭＬ模式语言提出了一种基于推导规　则的正规式相交判定算法。本文算法的优点为：　（１）具有广泛的适应性，对于一般的正规式，算　法复杂度是指数级的；当判定Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ正规　式相交时，算法的时间复杂度是多项式级的。　（２）对于某些特定的非Ｏｎｅ—Ｕｎａｍｂｉｕｇｏｕｓｉｅ规式，　算法的计算复杂度仍是多项式级。　（３）免去了两次转换运算，节约了计算时间。　２相关研究　关于正规式相交判定问题的理论基础来自于　Ｍｅｙｅｒ、Ｓｔｏｃｋｍｅｙｅ￣”　和Ｎｅｒｏｄｅ　上世纪六七十年代基　于自动机所做的工作。Ｍａｒｔｅｎｓ等人　对不同类型的正　规式包含和相交问题的算法复杂度进行了理论上的　分析。有关使用规则推导或公理系统解决正规式等　价等判定问题的工作最早见于Ｓａｌｏｍａａ的相关论文　，　这篇论文提出了两个用于证明正规式等价的公理系　统。Ｂｒｚｏｚｏｗｓｋｉｔ　。　首先提出了一套用于解决正规式　包含问题的推导规则。Ａｎｔｉｍｉｒｏｖｔ”　对Ｂｒｚｏｚｏｗｓｋｉ的　刘嘉等：基于规则推导的正规式相交判定算法　工作进行了改进。Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ正规式　伽是由　Ｂｒｉｉｇｇｅｍａｎｎ．Ｋｌｅｉｎ和Ｗｏｏｄ为定义标准通用标记语言　（ｓｔａｎｄａｒｄ　ｇｅｎｅｒａｌｉｚｅｄ　ｍａｒｋｕｐ　ｌａｎｇｕａｇｅ，ＳＧＭＬ）　的模　式语言ＤＴＤ（ｄｏｃｕｍｅｎｔ　ｔｙｐｅ　ｄｅｆｉｎｉｔｉｏｎ）而提出的，之　后亦广泛应用于各种ＸＭＬ模式语言。　与本文关系最为密切的是文献［１９．２０］。文献［１９１　为解决受限正规树文法　】中出现的正规式相交判定　问题，提出了一种基于自动机的相交判定算法。该算　法根据Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ正规式构建相应自动机来　判定两个自动机的交是否为空，其计算复杂度为多　项式时间ｏＧＥ。Ｉ×ｌＥ：ｌ×ｌＸ１Ｕ　Ｄ，其中Ｅ　和　：为算法　的输人正规式，二和二为巨和Ｅ的字符集。本文　与该文献所解决的问题相似，但是使用的解决方法不　同。本文提出的基于规则推导的方法省去了转换为　自动机的计算过程，同时具有更广泛的适用性，特别　是针对某些非Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ正规式，本文方法仍　可以在多项式时间内给出判定结果，这是文献［１９］所　做不到的。文献［２Ｏ］提出了一种基于规则推导的Ｏｎｅ—　Ｕｎａｍｂｉｇｕｏｕｓ正规式包含判定算法。本文与文献［２０１　所做工作的不同之处在于：首先，本文提出的推导规则　是针对相交判定问题而不是包含判定问题；其次，本　文提出的推导规则可以用于任何正规式，而文献［２０］　提出的推导规则基本上只能用于Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ　正规式，不能判定一般的正规式；最后，文献［２０］的每　一步推导过程都需要计算两个表达式的ｆｉｒｓｔ集和自　定义函数ｈｅａｄｅｒ，这极大增加了计算的时间开销，本　文方法无需计算ｆｉｒｓｔ集，同时也仅有一个计算复杂度　为ｏ（１）的自定义函数，因此更加高效。　３基本概念　下面先定义一些本文所用到的基本概念。首先　设　为一个有限字符集，ａ、ｂ和ｃ是属于　的字符，　，，，。，ｆ２…是定义在　上的字符变量。　定义１（正规式）字母表　上的正规式　归纳　定义为Ｒ　：＝　＋Ｒ　ｌ　・Ｒ　ＩＲ￣ＩＳ。符号“＋”表示若　有三１，Ｌ２ｃ２７＂，贝０Ｌ１＋　２＝｛ｗ１Ｕｗ２１ｗｌ∈Ｌ１，Ｗ２∈Ｌ２｝。类　似地，符号“・”表示若有　１，Ｌ２　ｃＸ　，则Ｌ１・Ｌ２＝｛ｗ１・Ｗ２　４５　Ｗ１∈Ｌ１，Ｗ２∈三，｝；符号“　则为Ｌ　的克林闭包（Ｋｌｅｅｎ　ｅｃｌｏｓｕｒｅ）。计算优先级为“　最高，“．”次之，“＋”最　低。为了防止二义性，可以将Ｒ　＋尺　和带“　的　・　子式加上括号，例如　＋　）和　・　）　，　并且在这种情况下，可以将符号“．”省略。下文中用　，　…表示正规式。本文与其他正规式定义（例　如文献［１９—２０１）的最大不同之处在于没有在归纳定　义中引入空字符“ｃ”。事实上，不带“Ｅ”的正规式定义　除了不能表示空正规式之外，表达能力上与带“Ｅ”的　正规式定义是等价的。而本文不考虑包含空正规式　的相交判定问题，因为根据下面的定义２其答案总是　不相交的，且加入“ｅ”会给推导增加不必要的复杂　性。但是在下面的推导中还是用到了符号“ｅ”，它仅　表示正规式的终止，因此只能出现在正规式的末尾。　注意不含“ｃ”的正规式定义仍然可以表示可空正规　式，除非它仅包含一个空串。　定义２（正规语言）正规式　所定义的正规语言　归纳定义为　＋　：ｌｌ＝ｌＩｒｌｌｌＵ　ｌＩ＇ｌＩｒ　・　：Ｉｌ＝ｌＩｒ　Ｉ，　ｌＩ＝Ｕ。　Ｉｌｒｌ　ｌ，最后对于　∈　有ｌｌａｌｌ＝｛口｝。正规式　相交判定问题就是对于任意正规式　和　，是否存　在非空字符串ｖ，使得１，∈ｌＩｒ　ｌｌ八１，∈ｌＩｒ，ＩＩ。　定义３（Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ　Ｗ规式）为了定义Ｏｎｅ－　Ｕｎａｍｂｉｇｕｏｕｓ正规式，先引入标记表达式的概念。对　于一个正规式，使用下标来依次标记其中出现的字符，　使得每个标记后的字符在表达式中仅出现一次，这样　的正规式称为标记表达式。用　表示　的标记表　达式，符号　表示标记的逆操作，即取消标记符号的　下标。例如（口１ｂ１）　２ｂ２　３＋６３）是正规式　６）　ａｂ（ａ＋ｂ）　的标记式。下面给出Ｏｎｅ—Ｕｎａｍｂｉｕｇｏｕｓ正规式的定　义。一个正规式　是Ｏｎｅ　Ｕｎａｍｂｉｇｕｏｕｓ的，当且仅当　对于任意两个句子ＵＸＶ，ｕｙｖ∈ｌ　ｒｍａｒｋｌｌ，其中　，Ｙ∈　，　若ｘｃｙ，则　（　≠　（　；如果一个正规语言可以用某　个Ｏｎｅ．Ｕｎａｍｂｉｇｕｏｕｓ正规式来表示，则也称该正规语　言是Ｏｎｅ－Ｕｎａｍｂｉｇｕｏｕｓ的。Ｏｎｅ—Ｕｎａｍｂｉｕｇｏｕｓ正规式　是由’Ｂｒｉｉｇｇｅｍａｎｎ．Ｋｌｅｉｎ和Ｗｏｏｄ为定义ＳＧＭＬ的模式　语言ＤＴＤ而提出的，之后亦广泛应用于各种ＸＭＬ模　４６　Ｊｏｕｒｎａｌ　ｏｆＦｒｏｎｔｉｅｒｓ　ｏｆＣｏｍｐｕ￣ｒ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ计算机科学与探索　２０１５，９（１）　式语言。Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ　ｉＥ规式是一种确定性正规　括号中的条件时，结论才成立。这７条规则按照优先　级分为３组，前５条规则优先级最高，规则＋次之，规　则，．ｃ最低。规则＋结论中的“ｖ”表示两个子式之间可　式，对于满足该正规式的字符串中的每一个符号，只　能唯一地匹配Ｏｎｅ－Ｕｎａｍｂｉｕｏｕｓ正规式中唯一的一　ｇ个位置而不需要向前看。根据文献［１０］，可以在线性　兼或的关系，在推导中这两个子式的计算关系没有约　时间内判定一个正规式是否是Ｏｎｅ—Ｕｎａｍｂｉｕｇｏｕｓ的。　４正规式相交判定推导规则　４．１推导规则　为了方便推导，在推导过程中出现的正规式后　面加上一个终止符Ｅ＝Ｅ　Ｉ　。终止符只起到标记的作　用，并不影响正规式的语义，即ＩＩｒ・Ｅ’Ｉｌ＝ｌｉｔ・Ｅｆｌｌ＝Ｍ。　在推导算法的输入正规式　。和，．　的末尾加上终止符　ｃ　，形成新的输入正规式ｒｌ　ｒ＝ｒ１・Ｅ’和ｒ２　ｒ＝　２・ｃ　。定　义ｔｏｃ　函数为ｔｏｅ　１　２…厂　・ｃ）＝　ｌ　２…　・ｃ　，ｔｏｅ　只是　将正规式末尾Ｅ　替换成［ｆ，同样不影响该正规式的　语义。推导中Ｆ的语义为根据从输人正规式ｒ　和，　到Ｆ的推导，不能找到字符串Ｓ，使得Ｓ∈Ｉ１＂　ｌｌ　ＡＳ∈　ｌｉｔ：Ｉｌ；反之，　的语义为根据从　和　到　的推导，必　能找到字符串Ｓ，使得　∈　Ｉ／ｋＳ∈ＩＩｒ：ＩＪ。下面是正　规式相交判定推导所使用的７个规则。　规则ｅ１：　［ｃ＝ｃ　ｏｒＥ　］　规则ｃ２：　［ｃ＝Ｅ　］　规则ｃ３：　［Ｃ：Ｃ１］　规　１：　［Ｉ１￣ｅｆ２］　规则１２：　ｌ１　￣ｒＩ＠　ｌ２￣ｒ２　［　］　：）删＋：　ｒ１　ｌ　Ｉ　ｒ２　ｒ４　‘　Ｖ　ｒ１　Ｉｒ３　ｒ４　Ｉ　。　删　：　首先对上面的推导规则进行必要的说明。每条　规则由横线分成上下两个部分，上半部分是该规则的　前提，下半部分是这条规则的结论。前５条右侧中括　号括起来的是前提的附加条件，只有当前提满足中　定。规则　结论中的“　”表示需先计算　ｎ　．　再计算　ｎ　，原因是结论中前子式的推导结果会对　后子式的推导产生影响。前子式的推导分支结果无　非有３种：第一是至少有一个　；第二是推导出的结果　全为Ｆ且不存在推出前提　ｎ　的分支；第三是推　导出的结果全为Ｆ但存在推出前提　ｎ　的分支。　最后一种情况推导出的　ｎｒ：　末尾可能是Ｅ　，则　ｎ　的末尾也需是ｃ　。话句话说，规则　要求先对　结论的前子式进行推导，若推导的结果改变了前提　ｎ　末尾的ｅ，则后子式继承改变后的前提　ｎｒ　的末尾Ｅ。　４．２推导规则的性质　定理１　４．１节的７个规则是正确的。　证明规则ｃｌ。因为，．　的ｆｉｒｓｔ集为，∈２７，所以　对于任一字符串Ｓ∈ｌＩｆ．，．１ｌ，其开头字符必为，。不妨　设输入正规式　＝　－ｅ和　＝　．，．，＋　”，则对于任　一Ｓ　∈　ｌｌＡＳ　∈　ｌｌ，都有ｓ　・ｓ∈ＩＩｒ２　・，・　ｌｌ＾Ｓ　・Ｓ仨　ＩＩｒ　．ｃｌＩ。由此可推出Ｆ。　规则Ｅ２。该规则的前提为ｃ　ｎｃ　。设输入正规　式为　＝　１ｔＦ２ｔ…，　・ｃ　和　２＝　１　２”…，＾　”・ｃ　，则从，．１　ｎ，２　到ｃ’ｎ　ｃ　的推导过程中必不使用规则『２，因为只有　使用规则ｆ２才可以将正规式末尾的Ｅ　通过ｔｏ￣　替换　为ｅ　。由此可得该推导过程都是使用规则　将　，　，．２　，…，　和，ｌ”，ｒ２”，…，ｒ　”消去，因此不能从输入正　规式　和　到ｃ’ｎＥ　的推导，找到字符串Ｓ，使得Ｓ∈　Ｉ＾　∈　ｌＩｏ由此可推出　。　规则ｅ３。该规则的前提为Ｅ　ｎｃ　，设输入正规式　为　１＝　ｌ　２　…　・Ｅ　和　２＝　１　２”…　ｍ　・Ｅ　，则从，１　ｎ　２　到ｃ　ｎ　的推导过程中至少使用过一次规则ｆ２，因　为只有使用规则ｆ２才可以将正规式末尾的ｃ　通过　ｔｏｅ　替换为ｃ　。则至少存在一个字符串ｕｌｖ，，∈　为　刘嘉等：基于规则推导的正规式相交判定算法　４７　推导中应用规则，２所消去的字符，，Ｕ，１，∈２７　为其他　的字符串，使得　，１，∈ＩＩｒｌｌｌ＾ｕｌｖ∈　ＩＩ。由此可推出　规则，１。该规则的前提为ｆ１．　ｎ，，．　，，，，≠１２。　使用反证法，若由该前提可推出　，则至少存在一个字　符串ｌｖ，１，∈　，使得ｌｖ∈ｌｉｔｌ－Ｆ１ＩＩ／ｋｌｖ∈Ｉｌｌ２・　，由此可　得，＝，１：，２，这与前提，１≠，２矛盾，因此由　１ｎ，２・　２，　对于任意正规式　和　，至少有一个推导规则的前提　满足　和　。根据正规式的定义，可以得出任意正规　式必属于下列４种情况之一：Ｅ，，　（　＋，．２）　。　其中，∈　，　∈Ｒ　，Ｅ只能出现在正规式的末尾。对　上述４种情况两两组合，可以得到以下ｌ０种情况：　ｃＮ　ｃ；ｃｎ，・，．；ｃＮ（ｒｌ＋　２）・，３；ｃＮ　２；，１・ｒ１ｎ，２・　２；　『１≠，，，只能推出　规则，２。该规则的前提为０　ｎ，　．　，ｆ１：１２，　也就是，．　ｎ，．ｒ　。若，．ｒ１　ｎ，．ｒ　成立，则至少存在　一个字符串ｌｖ，ｖ∈　，使得ｌｖ∈ｌＩｆ＿Ｆ１＿Ｊ＾ｌｖ∈ｌＩｆ．Ｆ２Ｉｌ，　由此可得Ｖ∈　Ｉ八　∈ＩＩｒ２ｌＩ，也就是ｒ　ｎ　：成立。又因　为根据ｔｏｃ　的定义ＩＩｆ（）ｃ　）ｌ『＝ＩＩｒｌＩ，所以ｔｏｃ　）Ａ　ｔｏ￣　２）　成立。　揪ＩＪ＋。该规则的前提为　１Ｎ（ｒ２＋　３）・　４。当　１＝ｃ　时，结论显然成立。当　≠ｃ时，若该前提成立，则至　少存在一个字符串ｌｖ，ｖ∈　，使得ｌｖ∈ＩＩｒ　ｌ１人ｌｖ∈　２＋　３）・　４ｆｌ。根据定义２可得ｌｖ∈ｌＩｒｌＩＩ＾ｌｖ∈ｑＩ　２・Ｆ４ｌＩＵ　＿ｌ，３・，．４ｌＤ，也　是ｌｖ∈ＩＩｒ１ｌｌ八ｌｖ∈ＩＩ，．２・Ｆ４　ｃ＿Ｖｌｖ∈ＪＩｒ１ｌｌ＾ｌｖ∈　・ｒ４　ＪＩ，因此得出ｒ１ｎ　２・，４ｖ　１ｎ，３・，４成立。　规则　。该规则的前提为　ｎ，；　。当　＝ｃ时，　结论显然成立。当　≠ｅ时，根据４．１节的分析得知，　前子式的推导分支结果有３种：第一是至少有一个　；　第二是推出的结果全为Ｆ且不存在推出前提　ｎ　的分支；第三是推出的结果全为Ｆ但存在推出前提　ｎ　ｒ　的分支。对于第一种情况，至少存在一个字　符串ｌｖ，ｖ∈　，使得ｌｖ∈ＩＩｒ１ｌｌ＾ｌｖ∈ｌｉｔｅｒ３ｌｌ，因此ｌｖ∈　日　人ｌｖ∈ＩＩｒ：・　；　ｌ　Ｊ　Ｖ　ｌＩｒｌｌＩ＾ｌｖ∈ＩＩｒ　ＩＤ也成立。对于第　二种情况，显然前提不能成立。对于第三种情况，若　前提　ｎ　的末尾为ｃ　，则结论前子式所推出的　ｒ　ｎ　末尾可能是ｃ　，因为结论的前子式为　ｎ，．　．　Ｆ２　Ｆ　，当　不是可空正规式时，只有通过规则，２消去　，而规则　会将ｃ　替换为Ｅｆ。这时需要将结论后　子式的末尾也变为ｃ　。综上所述，规则　成立。　口　定理２　４．１节的７个规则是完备的。　证明证明４．１节的规则是完备的也就是要证明　，・　１Ｎ（ｒ２＋　３）・　４；，・　１ｎ　：・　３；　１＋　２）－　３Ｎ（ｒ４＋ｒ５）・　６；　１＋，．２）・　３ｎ　：・，．５；　２ｎｒ；・，４。下面对这１０种　情况一一进行讨论。　情况１　ｃｎＥ。根据ｃ的定义，情况１又分为以下　３种子情况，即ｃ　Ｎ　ｃ　，Ｅ　ｎ　ｃ　和Ｅ　Ｎ　ｃ　。对于ｃ　ｎ　Ｅ　和ｅ　Ｃｌ　Ｅ　可以分别直接应用规则ｅ２和规则ｃ３得到Ｆ　和Ｌ而ｃ　ｎ　ｃ　在推导过程中是不可能出现的。因为　一方面，若出现Ｅ　，则在推导过程中必应用过至少一　次规则ｆ２，而规则１２的结论是ｔｏｅ　）ｎｔｏｃ　），即两　边的正规式都应用ｔｏ￣　函数，因此若ｃＮ　ｃ中有一边　是ｅ　，则另一边也一定是ｃ　。另一方面，因为没有一　条规则可以将正规式末尾的ｃ　替换为ｃ　，所以也不　可能通过Ｅ　Ｎ　Ｅ’得到Ｅ’Ｎｃ　。因此Ｅ　Ｎ　Ｅ　在推导过程　中是不可能出现的。　情况２　ＥＮ，．，＿满足规则Ｅ１，得ＮＦ。　情况３　ｃＮ（ｒ１＋　）・　３满足规则＋，推出ｃｎ　１・ｒ３　Ｖ　Ｅｎ，．２・　３。　情况４　ｃｎｒ　Ｆ２满足规则　，推出ｃｎ，．１・ｒ　ｒ２Ｖ　Ｅｎ　２。　情况５，１・ｒ１ｎ，２・　２。当，１≠，２时满足规则ｌｌ，推　出Ｆ；当，　＝，２时满足规则１２，推出ｔｏｃ　１）ｎｔｏｅ　２）。　情况６，・　１Ｎ（ｒ２＋　３）・ｒ４满足规则＋，推出，・　ｌｎ　・，．４Ｖ，・ｒ１ｎ　３・，．４。　情况７，・ｒ　ｎ　・　满足规则　，推出，・，．　ｎ　・　：・　３Ｖ，・ｒ１ｎｒ３。　情况８　１＋　２）・　３　Ｎ（ｒ４＋　５）・　６。应用两次规则＋，　推出，１・ｒ３ｎ，４・　６Ｖｒ２・ｒ３ｎｒ４・ｒ６Ｖｒｌ・　３ｎ　５・　６Ｖｒ２・　３ｎ　５・　６。　情况９（　１＋，２）・　３ｎ　・，５。应用规则＋，推出ｒ１・　４８　Ｊｏｕｒｎａｌ　ｏｆＦｒｏｎｔｉｅｒｓ　ｏｆＣｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ　ａｎｄ　Ｔｅｃｈｎｏｌｏｇｙ计算机科学与探索　，３ｎ　：・　５ｖ　ｒ２・ｒ３ｎ　：・，５；再应用规则　，推出　ｌ・ｒ３ｎ　ｒ４・ｒ４‘　　ｒ５ｖｒ１・Ｆ３ｎｒ６ｖ　Ｖ　。　Ｉ　ｌ　Ｖ　‘ｒ２・ｒ３ｎｒ４・Ｆ４　ｌ　ｌ　。　　ｒ５ｖｒ２・ｒ３ｎｒ５。Ｖ　’　ｌ　ｌ　ｏ　ｉｆ（ｒ　，ｒ４）　Ｓ　找到与（　，ｒ　）匹配的推导规则；　当规则的结论是　时　Ｒｅｔｕｍ“Ｙｅｓ”：　情况１０　．　：ｎｒ：．，一　。与规则８情况类似，两次　应用规则　即可，在此不再赘述。　口　４．３扩展规则　为了简化推导过程，根据４．１节的推导规则可以　当规则的结论是（，．　Ａｒ　）Ｖ…Ｖ（　ｎｒ　）时　ｐｕｓｈ（ｒ５，ｒ６），…，（ｒ　，，　）ｏｎ　；　得到以下扩展规则。　规则ｃ　：　规则　堋『Ｊｆ　规贝０＋＋：　１＋　２）・ｒ３Ｎ（ｒ４＋ｒ５）・　６　１・，３ｎｒ４・ｒ６Ｖ，．２・ｒ３ｎ　４・　６Ｖｒ１・　３ｎ　５・　６Ｖ，｜２・ｒ３ｎ　５・　６　定理３　４．３节的４个规则是正确的。　证明规则，＋、规则　和规则＋＋可参见定理２中　情况６～８的证明。下面主要讨论规则ｃ　，为此可将ｒ　分成５种情况：ｃ　、ｃ　、，・　、（　１＋ｒ２）－　３、　２。对于　Ｅ　，可由规则ｃ２推出Ｆ；对于ｃ　，已有定理２中的情况　１证明不可能在推导中出现。对于，．ｒ，可由规则ｃｌ　推出Ｆ；对于（　＋ｒ２）・，３和　，．２，亦可由４．１节的规则　展开成以ｃ　、ｃ　、，．ｒ子式组合的形式，由此可归结为　Ｅ　、Ｅ　、，．　的情况。无论　为哪种情况，ｃ　ｎ　都只　能推出Ｆ，因此规则Ｅ　是正确的。　口　５算法和举例　基于４．１节和４．３节的推导规则，可以给出一个　判定正规式相交问题的算法。　算法正规式相交判定算法　输入：正规式　和　。　输出：“Ｙｅｓ”或“Ｎｏ”。　初始化栈　和集合Ｓ为空；　ｐｕｓｈ（ｒ１，ｒ２）ｏｎ　；　ｗｈｉｌｅ　Ｔ不为空ｄｏ　ｐｏｐ（　，ｒ４）ｆｒｏｍ　；　当规则的结论是（　Ｎｒ　）　（ｒ　，ｒ　）时　ｐｕｓｈ（ｒ５，ｒＴ），（ｒ５　ｆＴｒ６）ＯＤ　；　ａｄｄ（ｒ３，ｒ４）ｔｏ　；　ｅｎｄ　ｉｆ（ｒ３，ｒ４）∈Ｓ　若（　，ｒ　）的末尾为［ｆ，则在　中找到与（　，ｒ　）等　价的正规式对（，　，ｒ９），若（ｒ　，ｒｇ）的末尾为Ｅ　，将　中（，　，ｒｇ）　上方所有正规式的末尾改为Ｅｆ；　ｅｎｄ　ｅｎｄ　ｒｅｔｕｒｎ“Ｎｏ”；　算法的输人为符合定义１的正规式，为了方便推　导，在输入正规式的末尾加上符号ｅ　。该算法的基　本思想是使用推导规则进行深度优先查找，当找到　第一个结论“　’时，说明已经找到一个非空字符串　都　满足正规式ｒ　和　，说明ｒ　和ｒ　存在交集，因此返　回“Ｙｅｓ”，整个推导过程结束。当推出为“Ｆ”的结论　时，说明在该推导分支没有找到非空字符串　都满足　正规式　和　，因此退回到最近的分支点沿着另一　条推导路径查找。若遍历整个查找空间都没有找到　结论“Ｆ”，说明　和　是不相交的，因此返回“Ｎｏ”。　根据文献［１　１］的结论，可知正规式相交判定问题　是一个ＰＳＰＡＣＥ．完全的问题。因此该算法对于一般　的正规式其时间复杂度是指数级的。但当两个正规　式都是Ｏｎｅ．Ｕｎａｍｂｉｇｕｏｕｓ正规式时，则其时间复杂度　降为多项式级　。关于Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ　规式相交　判定的例子可参见例１。前文提到比起其他工作ｎ　１，　本文方法具有更广泛的适用性，特别是针对某些二　义性正规式，仍可以在多项式时间内给出判定结　果。具体可见例２。　例１和例２分别是两个正规式相交判定的例子。　刘嘉等：基于规则推导的正规式相交判定算法　４９　例１　ａ＊ｂ　ｎ　＋６）　ｌ：ａ—ｂ　Ｅ　ｎ　＋６）　ｃ　１　ｌ：ａ　ｂ　Ｅ　ｎｂ（ａ＋ｂ）’（　：　（１１）Ｆ　１３：ｂ　ｃ　Ｎ　ｂ（ａ＋ｂ）　Ｅ　１４：６　ｃ　Ｎ６　＋　ｃ　（１２）１６：ｂ　ｃ　Ｎ（ａ＋６　ｃ　）１７：　Ｅ　ｎ　＋６）　＋６）　ｃ　ｖ　Ｆ　一．　１５：［ｆＮｂ（ａ＋　Ｅ　例２　ａｂｎ（ａ＋　＋ｃ）　ｃ（６＋ｃ）　＋ｃ）（６＋ｃ）　＋ｃ））６　１：ａｂｅ　ｎ（　＋（６＋ｃ）　ｃ（６＋ｃ）（６＋ｃ）（６＋ｃ）（６＋ｃ））６ｃ　ｅ　＊ｅ＊（＋）２　：　ａ　ｂＮａｂｆｆ２１３口ｂｎ（ｂ＋ｃ）　ｃ（６＋ｃ）　６Ｅ　ｒｖ４：————　———６结束语　本文针对ＸＭＬ类型检查提出了一种基于推导规　则的正规式相交判定算法，该算法根据输入的正规　式直接进行推导得出是否相交的结论，而无需进行确　：　Ｎ　、　例１为ａ＊ｂ　Ｎ（ａ＋　，因为两个输入的正规式中　都没有重复出现的字符，所以这两个正规式都是Ｏｎｅ—　定性自动机的构造。本文算法具有广泛的适应性，对　于一般的正规式，算法复杂度是指数级的；当判定在　ＸＭＬ类型检查中广泛使用的Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ正规　Ｕｎａｍｂｉｇｕｏｕｓ正规式。注意为了方便推导，在开始时　将输入正规式　和　的末尾都加上ｃ　，当计算到８　式时，算法的时间复杂度自动降为多项式级的。对于　某些特定的二义性正规式，例如　＋ｒ２）ｒ　这样的正　式时，由于推导结果与１式相同，因此将１式及其所　有下方正规式的末尾都改为Ｅ　。例中…表示限于篇　幅省略的一些简单推导过程。当推导到１９式时，由　规则，１推出，，程序返回“Ｙｅｓ”。　例２右部是一个非确定性正规式（ａ＋　规式，其中　１和，＾３为Ｏｎｅ—Ｕｎａｍｂｉｇｕｏｕｓ　ＴＩ＿规式，而，。　为二义性正规式，算法的计算复杂度仍可能为多项　式级。　Ｒｅｆｅｒｅｎｃｅｓ：　［１】Ｃｏｄｄ　Ｅ　Ｆ．Ａ　ｒｅｌａｔｉｏｎａｌ　ｍｏｄｅｌ　ｏｆ　ｄａｔａ　ｆｏｒ　ｌａｒｇｅ　ｓｈａｒｅｄ　ｄａｔａ　ｂａｎｋｓ［Ｊ］．Ｃｏｍｍｕｎｉｃａｉｔｏｎｓ　ｏｆｔｈｅＡＣＭ，１９７０，１３（６）：３７７—３８７．　（６＋　ｃ（ｂ＋ｃ）（６＋ｃ）（２）＋ｃ）（６＋ｃ））６，其中非确定性子式　为（６＋ｃ）　ｃ（ｂ＋ｃ）　＋ｃ）　＋ｃ）　＋Ｃ），表示倒数第五个　字符为Ｃ的字符串。若要构建正规式（６＋ｃ）　ｃ（６＋ｃ）　［２】Ｂｒａｙ　Ｔ，Ｐａｏｌｉ　Ｊ，Ｓｐｅｒｂｅｒｇ—ＭｃＱｕｅｅｎ　Ｃ　Ｍ，ｅｔ　ａ１．ＲＥＣ—ｘｍｌ－　１９９８０２１０　Ｅｘｔｅｎｓｉｂｌｅ　ｍａｒｋｕｐ　ｌａｎｇｕａｇｅ（ＸＭＬ）［Ｓ／ＯＬ］．Ｗｏｒｌｄ　Ｗｉｄｅ　Ｗｅｂ　Ｃｏｎｓｏｒｔｉｕｍ　Ｒｅｃｏｍｍｅｎｄａｔｉｏｎ．ｈｔｔｐ：ｌｌｗｗｗ．ｗ３．　ｏｒｇ／ＴＲ／１９９８／ＲＥＣ—ｘｍｌ－１９９８０２１０．　的确定性自动机，则该自动机包含的状态与Ｄ　）成　正比，即状态呈指数级增长。而例２的推导过程直接　将右部的非确定性子式忽略，从而节省了大量的计算　时间。由此可见，对于诸如（　＋　）　这样的正规式，　其中　和　为Ｏｎｅ－Ｕｎａｍｂｉｇｕｏｕｓ］￣规式，而，．２为二义　［３］Ｃｏｍｏｎ　Ｈ，Ｄａｕｃｈｅｔ　Ｍ，Ｇｉｌｌｅｒｏｎ　Ｒ，ｅｔ　ａ１．Ｔｒｅｅ　ａｕｔｏｍａｔａ　ｔｅｃｈ—　ｎｉｑｕｅｓ　ａｎｄ　ａｐｐｌｉｃａｔｉｏｎｓ［Ｍ／ＯＬ］．ｆ２００７）［２０１４—０４—１２］．ｈｔｔｐ：／／　ｗｗｗ．ｇｒａｐｐａ．ｕｎｉｖ－ｌｉｌｌｅ３．ｆｒ／ｔａｔａ．　性正规式，当从　，　推出Ｆ时，该算法可以自动忽略ｒ　，　由此整个推导过程的时间复杂度还能保持多项式级。　［４】Ｂｅｎｚａｋｅｎ　Ｖ　Ｃａｓｔａｇｎａ　Ｇ，Ｆｒｉｓｃｈ　Ａ．ＣＤｕｃｅ：ａｎ　ＸＭＬ　ｃｅｎ￣ｉｃ　ｇｅｎｅｒａｌ—ｐｕｒｐｏｓｅ　ｌａｎｇｕａｇｅ［Ｊ］．ＡＣＭ　ＳＩＧＰＬＡＮ　Ｎｏｔｉｃｅｓ，２００３，　５０　ＪｏｕｒｎａｌｏｆＦｒｏｎｔｉｅｒｓｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ计算机科学与探索　２０１５，９（１）　３８（９）：５１－６３．　ｏｆｔｈｅＡＣＭ，１９６４，１１（４）：４８１—４９４．　［１　６】Ｂｒｚｏｚｏｗｓｋｉ　Ｊ　Ａ。Ｒｏｏｔｓ　ｏｆ　ｓｔｒａ　ｅｖｅｎｔｓ［Ｃ］／／Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　７ｔｈ　Ａｎｎｕａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ｓｗｉｔｃｈｉｎｇ　ｎｄ　ａＡｕｔｏｍａｔａ　Ｔｈｅｏｒｙ．　Ｐｉｓｃａｔａｗａｙ，ＮＪ，ＵＳＡ：ＩＥＥＥ，１９６６：８８—９５．　［５】Ｔｈｏｍｐｓｏｎ　Ｈ　Ｓ．ＸＭＬ　ｓｃｈｅｍａ　ｐａｒｔ　１：ｓｔｒｕｃｔｕｒｅｓ　ｓｅｃｏｎｄ　ｅｄｉ—　ｉｆｏｎ［Ｓ／ＯＬ］．Ｗｏｒｌｄ　Ｗｉｄｅ　Ｗｅｂ　Ｃｏｎｓｏｒｔｉｕｍ．【２０１４－０４—１２］．ｈｔｔｐ：／／　、）ｉ　．ｗ３．ｏｒｇ／ＴＲ／２００４／ＲＥＣ－ｘｍｌｓｃｈｅｍａ－１－２００４１０２８．　［６】Ｇａｐｅｙｅｖ　Ｌｅｖｉｎ　Ｍ　Ｙ，Ｐｉｅｒｃｅ　Ｂ　Ｃ，ｅｔ　ａ１．Ｔｈｅ　Ｘｔａｔｉｃ　ｅｘｐｅｒｉ—　【１７】Ａｎｔｉｍｉｒｏｖ　Ｖ　Ｒｅｗｒｉｔｉｎｇ　ｒｅｇｕｌａｒ　ｉｎｅｑｕａｌｉｔｉｅｓ［Ｃ］／／ＬＮＣＳ　９６５：　Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　１０ｔｈ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｃｏｎｆｅｒｅｎｃｅ　ｏｎ　Ｆｕｎｄａ・　ｅｎｃｅ，ＭＳ－ＣＩＳ－０４・２４［Ｒ］．Ｕｎｉｖｅｒｓｉｔｙ　ｏｆＰｅｎｎｓｙｌｖａｎｉａ，２００４．　［７】Ｈｏｓｏｙａ　Ｈ，Ｐｉｅｒｃｅ　Ｂ　Ｃ．ＸＤｕｃｅ：ａ　ｓｔａｔｉｃａｌｌｙ　ｔｙｐｅｄ　ＸＭＬ　ｐｒｏ—　ｍｅｎｔａｌｓ　ｏｆ　Ｃｏｍｐｕｔａｔｉｏｎ　Ｔｈｅｏｒｙ（ＦＣＴ’９５），Ｄｒｅｓｄｅｎ，Ｇｅｒ－　ｍａｎｙ，Ａｕｇ　２２－２５，１９９５．Ｂｅｒｌｉｎ，Ｈｅｉｄｅｌｂｅｒｇ：Ｓｐｆｉｎｇｅ￣１９９５：　１　１６．１２５．　ｃｅｓｓｉｎｇ　ｌａｎｇｕａｇｅ［Ｊ］．ＡＣＭ　Ｔｒａｎｓａｃｔｉｏｎｓ　ｏｎ　Ｉｎｔｅｒｎｅｔ　Ｔｅｃｈ－　ｎｏｌｏｇｙ，２００３，３（２）：１１７－１４８．　［８］Ｖａｎ　ｄｅｒ　Ｖｌｉｓｔ　Ｅ．Ｒｅｌａｘ　ＮＧ［Ｍ］．Ｓｅｂａｓｔｏｐｏｌ，ＣＡ，ＵＳＡ：Ｏ’Ｒｅｉｌｌｙ　Ｍｅｄｉａ　Ｐｒｅｓｓ，２００３．　【１８】Ｇｏｌｄｆａｒｂ　Ｃ　Ｆ，ＲｕｂｉｎｓｋｙＹ　ｈｅ　ＴＳＧＭＬｈａｎｄｂｏｏｋ［Ｍ］．Ｏｘｆｏｒｄ，　ＵＫ：Ｏｘｆｏｒｄ　Ｕｎｉｖｅｒｓｉｔｙ　Ｐｒｅｓｓ，１９９０．　［９］Ｃｌａｒｋ　Ｊ．ＴＲＥＸ—ｔｒｅｅ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ　ｆｏｒ　ＸＭＬ［Ｒ］．　［２０１４—０４—１２］．ｈｔｔｐ：／／ｗｗｗ．ｔｈａｉｏｐｅｎｓｏｕｒｃｅ．ｃｏｍ／ｔｒｅｘ．　［１９】Ｎｉ　Ｘｉａｏｙｏｎｇ，Ｃｈｅｎ　Ｈａｉｍｉｎｇ．Ｉｎｔｅｒｓｅｃｔｉｏｎ　ｃｈｅｃｋｉｎｇ　ｏｆ　ｐｒｏ—　ｄｕｃｔｉｏｎ　ｒｕｌｅｓ　ｉｎ　ｒｅｇｕｌａｒ　ｔｒｅｅ　ｇｒａｍｍａｒ［Ｊ］．Ｃｏｍｐｕｔｅｒ　Ｅｎｇｉ－　ｎｅｅｒｉｎｇ　ａｎｄ　Ｄｅｓｉｇｎ，２０１２，３３（３）：１１９７—１２０２．　【１０】Ｂｒｉｉｇｇｅｍａｒｍ－Ｋｌｅｉｎ　Ａ，Ｗｏｏｄ　Ｄ．Ｏｎｅ—ｕｎａｍｂｉｇｕｏｕｓ　ｒｅｇｕｌａｒ　ｌａｎｇｕａｇｅｓ［Ｊ］．Ｉｎｆｏｒｍａｔｉｏｎ　ａｎｄ　Ｃｏｍｐｕｔａｔｉｏｎ，１９９８，１４０（２）：　２２９．２５３．　［２０］Ｈｏｖｌｎｄ　ａＤ．Ｔｈｅ　ｉｎｃｌｕｓｉｏｎ　ｐｒｏｂｌｅｍ　ｏｒｆ　ｒｅｇｕｌａｒ　ｅｘｐｒｅｓｓｉｏｎｓ［Ｊ］．　Ｊｏｕｒｎａｌ　ｏｆ　Ｃｏｍｐｕｔｅｒ　ａｎｄ　Ｓｙｓｔｅｍ　Ｓｃｉｅｎｃｅｓ，２０１２，７８（６）：　１７９５．１８１３．　［１１】Ｓｔｏｃｋｍｅｙｅｒ　Ｌ　Ｊ，Ｍｅｙｅｒ　Ａ　Ｒ．Ｗｏｒｄ　ｐｒｏｂｌｅｍｓ　ｒｅｑｕｉｒｉｎｇ　ｅｘｐｏ—　ｎｅｎｔｉａｌ　ｔｉｍｅ［Ｃ］／／Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　５ｔｈ　Ａｎｎｕａｌ　ＡＣＭ　Ｓｙｍ－　ｐｏｓｉｍ０１ｕ１Ｔｈｅｏｒｙ　ｏｆＣｏｍｐｕｔｉｎｇ（ＳＴＯＣ’７３）．ＮｅｗＹｏｒｋ，ＮＹ　ＵＳＡ：ＡＣＭ．１９７３：１－９．　［２１】Ｃｈｅｎ　Ｌｅｉ．Ｒｅｓｔｒｉｃｔｅｄ　ｒｅｇｕｌａｒｔｒｅｅ　ｒａｇｍｍａｒｓ　ｎｄｔａｙｐｅ　ｃｈｅｃｋｉｎｇ　ａｐｐｒｏａｃｈｅｓ　ｂａｓｅｄ　ｏｒ／ｃｈｅｃｋｉｎｇ　ｉｎｃｌｕｓｉｏｎ　ｂｅｔｗｅｅｎ　ｒｅｇｕｌａｒ　［１２】Ｎｅｒｏｄｅ　Ａ．Ｌｉｎｅａｒ　ａｕｔｏｍａｔｏｎ　ｔｒｎｓａｆｏｒｍａｔｉｏｎｓ［Ｊ］．Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆｔｈｅ　Ａｍｅｒｉｃａｎ　Ｍａｔｈｅｍａｔｉｃａｌ　Ｓｏｃｉｅｔｙ，１９５８，９（４）：５４１－５４４．　［１３】Ｍａｒｔｅｎｓ　ｗ　Ｎｅｖｅｎ　Ｓｃｈｗｅｎｔｉｃｋ　ｅｔ　ａ１．Ｅｘｐｒｅｓｓｉｖｅｎｅｓｓ　ｅｘｐｒｅｓｓｉｏｎｓ［Ｄ］．Ｂｅｉｊｉｎｇ：Ｉｎｓｔｉｔｕｔｅ　ｏｆ　Ｓｏｆｔｗａｒｅ，Ｃｈｉｎｅｓｅ　Ａｃａｄ－　ｅｍｙ　ｏｆ　Ｓｃｉｅｎｃｅｓ，２０１０．　ａｎｄ　ｃｏｍｐｌｅｘｉｙ　ｔｏｆ　ＸＭＬ　ｓｃｈｅｍａ［Ｊ］．ＡＣＭ　Ｔｒａｎｓａｃｔｉｏｎｓ　ｏｎ　Ｄａｔａｂａｓｅ　Ｓｙｓｔｅｍｓ，２００６，３１（３）：７７０—８１３．　［１４】Ｓａｌｏｍａａ　Ａ．Ｔｗｏ　ｃｏｍｐｌｅｔｅ　ａｘｉｏｍ　ｓｙｓｔｅｍｓ　ｆｏｒ　ｔｈｅ　ａｌｇｅｂｒａ　ｏｆ　附中文参考文献：　［１９］倪晓勇，陈海明．正规树文法的产生式相交判定［Ｊ］．计算　机工程与设计，２０１２，３３（３）：１１９７—１２０２．　［２１］陈雷．受限正规树文法与基于正则表达式包含判定的类　ｒｅｇｕｌｒ　ａｅｖｅｎｔｓ［Ｊ］．Ｊｏｕｒｎａｌ　ｏｆｔｈｅＡＣＭ，１９６６，１３（１）：１５８－１６９．　［１５］Ｂｒｚｏｚｏｗｓｋｉ　Ｊ　Ａ．Ｄｅｒｉｖａｔｉｖｅｓ　ｏｆｒｅｇｕｌｒ　ａｅｘｐｒｅｓｓｉｏｎｓ［Ｊ］．Ｊｏｕｒｎａｌ　型检查［Ｄ］．北京：中国科学院软件研究所，２０１０．　ＬＩＵ　Ｊｉａ　ｗａｓ　ｂｏｍ　ｉｎ　１９８４．Ｈｅ　ｉｓ　ａ　Ｐｈ．Ｄ．ｃａｎｄｉｄａｔｅ　ａｔ　Ｂｅｉｊｉｎｇ　Ｕｎｉｖｅｒｓｉｙｔ　ｏｆ　Ｔｅｃｈｎｏｌｏｇｙ．Ｈｉｓ　ｒｅｓｅａｒｃｈ　ｉｎｔｅｒｅｓｔｓ　ｎｃｌｉｕｄｅ　ｓｏｆｔｗａｒｅ　ｔｈｅｏｒｙ　ａｎｄ　ｄａｔａ　ｍａｎａｇｅｍｅｎｔ　ｆｏｒ　ＸＭＬ，ｅｔｃ．　刘嘉（１９８４一），男，北京人，北京工业大学博士研究生，主要研究领域为软件理论，ＸＭＬ数据管理等。　ＬＩＡＯ　Ｈｕｓｈｅｎｇ　ｗａｓ　ｂｏｒｎ　ｉｎ　１９５４．Ｈｅ　ｉｓ　ａ　ｐｒｏｆｅｓｓｏｒ　ａｎｄ　Ｐｈ．Ｄ．ｓｕｐｅｒｖｉｓｏｒ　ａｔ　Ｂｅｉｊｉｎｇ　Ｕｎｉｖｅｒｓｉｔｙ　ｏｆ　Ｔｅｃｈｎｏｌｏｇｙ．Ｈｉｓ　ｒｅｓｅａｒｃｈ　ｉｎｔｅｒｅｓｔｓ　ｉｎｃｌｕｄｅ　ｄａｔａｂａｓｅ　ｔｅｃｈｎｏｌｏｇｙ　ａｎｄ　ｔｈｅｏｒｙ，ｃｏｍｐｉｌｅｒ　ｔｅｃｈｎｏｌｏｇｙ　ａｎｄ　ｓｏｆｔｗａｒｅ　ｔｈｅｏｒｙ，ｅｔｃ．　廖湖声（１９５４一），男，北京人，北京工业大学计算机学院教授、博士生导师，主要研究领域为数据库技术和理　论，编译技术与程序理论等。