Algorithmic and Foundational Aspects of Rewriting

这项研究是关于以下方面的有效算法：(I)规范化，即使用规则(称为重写系统)简化表达式，以及(Ii)重写系统的基本性质。正在开发使用静态规则进行归一化分析的算法。使用动态规则的增量式归一化算法也在研究中。有效的列表算法的扩展正在研究中。休斯顿大学开发的快速重写试验台正在对算法的实际性能进行评估。人们正在研究几个基本性质的有效算法和下界，包括正规形的唯一性、合流性和可判定子类的字问题。正在利用资源受限削减的概念研究这些问题之间的密切关系。归一化是几乎所有符号计算和计算机代数系统中的基本操作。应用包括函数和等式逻辑编程、数据类型规范、形式验证、自动演绎、代码生成和类型推理。这项研究有望产生：(I)提高符号计算和计算机代数系统的效率和能力，(Ii)更好地理解所涉及操作的内在复杂性，以及(Iii)对重写系统的基本性质的新结果、新技术和新见解。更广泛的影响包括：培训本科生和研究生，包括代表性不足的少数群体，根据这项研究编写新的课程材料，以及传播为推广和使用而开发的软件。

This research is on efficient algorithms for: (i) normalization, i.e., simplification of expressions, using rules (called a rewrite system), and (ii) fundamental properties of rewrite systems. Algorithms that use analysis for normalization with static rules are being developed. Incremental algorithms for normalization with dynamic rules are also being investigated. Extensions of efficient tabling algorithms are being studied. Practical performance of algorithms is being evaluated in the Laboratory for Rapid Rewriting test bed developed at University of Houston. Efficient algorithms and lower bounds are being studied for several fundamental properties, including uniqueness of normal forms, confluence, and the word problem, for decidable subclasses. Tight relationships among these problems are being studied using the concept of resource-bounded reductions. Normalization is a fundamental operation found in virtually all symbolic computation and computer algebra systems. Applications include functional and equational logic programming, data type specification, formal verification, automated deduction, code generation, and type inferencing. This research is expected to yield: (i) enhanced efficiency and power of symbolic computing and computer algebra systems, (ii) better understanding of inherent complexities of the involved operations, and (iii) new results, techniques and insights into fundamental properties of rewrite systems. Broader impacts include: training of undergraduate and graduate students including underrepresented minorities, new course materials based on this research, and dissemination of software developed for extensions and use.