无秩树结构数据和语义多态类型系统的研究

随着网络的发展，生产、消费与处理大量数据的应用不断增长，应用程序的安全性和设计、实现效率等问题也更加突出。XML可以简单、灵活地描述各种带结构的数据，成为数据交换的事实标准。因此，研究用XML表示的复杂结构数据的计算与编程的理论与技术问题，不仅对解决上述问题具有现实意义，而且对于未来的网络应用也不可缺少。对于XML的处理程序，类型是对付上述问题的一种有效手段。由于XML类型比传统编程语言里的类型在本质上复杂得多，研究上提出了新的挑战。本项目针对以XML表示的复杂结构数据，研究类型的表示与相关的可判定性问题的复杂度与算法，和语义类型系统的多态化问题。为加强程序的安全性和提高程序的设计、实现效率提供理论、算法的支持。同时，进行实验和实例研究，检验理论、算法研究结果。XML类型将可能和整数类型一样，成为软件的基本类型。因此，研究有关的理论和算法问题，对于软件性能的提高和类型系统的发展十分必要。

本项目针对以XML表示的复杂结构数据，研究类型的表示与相关的可判定性问题的复杂度与算法，和语义类型系统的多态化问题。本项目执行结果超额完成了研究计划，取得的主要进展和结果如下。.(1) 在类型表示的理论问题研究方面，1) 对XML 类型表示中极为重要的确定性和计数等问题进行了深入研究。2) 提出了XML Schema和DTD的表达式非确定性的诊断概念。3) 提出了受限的正规树文法RRTG，可表示常见的实用子类包括XML Schema和DTD. 4) 基于对实际数据的分析结果，提出了一类新的受限正则表达式Echare. 5) 提出一个通用的描述数据转换的模型，结合数据库的应用问题，研究了不同情况下完全信息无损以及部分信息无损判定问题的复杂度和相应的判定算法。.(2) 在实用子类的算法研究方面，1) 提出了基于原表达式、支持计数的表达式确定性判定算法，2) 提出了强确定性表达式的线性判定算法，3) 提出了可给出错误诊断信息的确定性表达式诊断算法，算法的时间复杂度是线性。4) 提出了RRTG 中区分确定性与不确定性表达式情况的包含判定算法，和判断给定树文法是否RRTG的算法，5) 提出了从句子集合中推断Echare的推断算法。.(3) 在多态类型系统研究方面，解决了为XML处理语言扩展参数多态化功能的问题，内容分为两个部分：多态语义子类型关系的定义和多态演算的定义。1) 定义了多态语义子类型关系。该定义是带类型变量的正则树类型的子类型关系的定义问题的第一个解决方案。我们引入了凸性属性，作为定义子类型关系的集合论解释的主要思想。基于集合论和凸性，我们提出了一个可靠的、完备的且可终止的子类型检测算法。2) 定义了一个带交类型的显式类型化lambda-演算。该演算是CDuce的多态版本。我们定义了一个类型匹配问题并提出一个可靠的、完备的且可终止的类型匹配算法。基于类型匹配算法，我们提出了多态演算的一个半可判定的局部推导算法。为了给多态演算提供一个执行模型，我们设计了从多态演算到单态演算（如Cduce的变体）的转化。.(4) 设计实现了上下文无关文法的句子生成工具，借助该工具进行了大量实验。.(5) 已发表和录用14篇研究论文。