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.