受限正规树文法与基于正则表达式包含判定的类型检查

XML简单灵活的特性使得XML在网络服务、关系数据库以及形式化研究等领域得到应用。同时，XML处理的技术不断发展，近期的研究表明静态类型化的处理方式在XML处理的有关方面有重要的优势。静态类型化XML处理技术是将XML的模式语言作为程序语言的基本数据类型，在程序运行之前进行静态的类型检查，从而确保运行时的类型安全。目前大多数静态类型系统采用正则表达式类型作为基本类型，正则表达式类型与树自动机是一一对应的。 子类型关系判定是类型检查中的核心问题。语义子类型的方法在静态类型化XML处理中有很多优点。在这种子类型判定方法中，类型被看成是值的集合，子类型关系判定转化为集合的包含判定。目前广泛应用的XML的模式语言如DTD、XML Schema等都是正规树语言的子类。正规树语言的包含问题是可判定的。在类型检查中，正则表达式类型的实现是基于树自动机的，子类型关系判定转化为树自动机的包含判定，效率较低。 本文提出了一种基于正则表达式包含判定的类型检查方法。由于DTD是目前使用最普遍的XML模式语言，因此本文首先提出针对DTD的类型检查方法，然后在此基础上进行扩展，提出了产生式不相交的正规树文法的概念以及针对该受限树文法的类型检查方法。DTD以及XML Schema等常用的XML模式语言均可由该树文法直接描述。在本文的方法中，子类型关系判定的过程不需要构造树自动机，而是根据类型表达式的树状结构自下而上地进行检查，每一层的检查基于正则表达式的包含判定，同时在判定过程中利用了树文法中的标号与类型之间的联系。该方法可以针对不同种类的正则表达式使用不同的包含判定算法。通过采用一种称为消除局部递归类型的策略，使得对并类型的子类型关系判定比基于树自动机的类型检查方法更加简单。本文实现了上述类型检查方法，并通过相应的实验说明该方法的可行性以及有效性。同时分析比较了已有的XML类型检查的方法与基于正则表达式包含判定的类型检查方法的优缺点。