Efficient Type Checking for a Subclass of Regular Expression Types

Type checking is an important problem in statically typed XML processing languages. Most type systems are implemented based on tree automata for the tree structure of XML documents and schemas. It is known that the complexity of inclusion problem for tree automata is in EXPTIME. In fact, most definitions in XML Schema are actually DTDs. The inclusion problem of DTDs can be reduced to inclusion of one-unambiguous regular expressions in DTDs. We have developed a method for type checking that works for regular expression types which are DTDs. The method is based onone-unambiguous regular expressions together with using the information of labels in DTDs, which can work in top-down or bottom-up manner. Although our method supports DTDs only now, it is general and can support more general schemas by integrating with the conventional method of type checking. The experiments show that our method is more efficient in practice.