Algorithmic and Foundational Aspects of Rewriting

规格化，即关于称为重写系统的一组规则的表达式的简化，是几乎所有符号计算和计算机代数系统中的基本计算步骤。这种操作的应用包括函数式、方程式和逻辑编程语言、抽象数据类型规范和验证、自动演绎、代码生成、类型推理和计算机代数。这一建议解决了符号计算和计算机代数中这一重要问题的算法和基础方面。该项目涉及开发使用预处理和静态分析进行静态规则匹配和归一化的算法，以及用于动态规则集匹配和归一化的增量式算法。从历史中有效学习的算法将针对几类重要和有用的重写系统进行标准化设计。我们将研究我们的算法的实际性能。给出了非线性重写系统和条件重写系统的重要的唯一范式性质的技巧和充分条件。抽象的丘奇-罗瑟性质将被研究为重写模方程理论的分层组合。推广了一般重写系统和条件重写系统的非线性递阶组合的Church-Rosser性质的现有充分条件。层次结构组合是编写大多数规范和软件的方式。该项目预计将：(I)有助于提高符号计算和计算机代数系统的效率和能力，(Ii)提供对所涉及操作的内在/复杂性的理解，以及(Iii)产生新的结果、技术和对重写系统的两个基本问题的见解，即正规形的唯一性和Church-Rosser性质。

Normalization, i.e., the simplification of expressions with respect to a set of rules called a rewrite system, is a fundamental computational step found in virtually all symbolic computation and computer algebra systems. Applications of this operation include functional, equational and logic programming languages, abstract data type specification and verification, automated deduction, code generation, type inferencing, and computer algebra. This proposal addresses both algorithmic and foundational aspects of this important problem in symbolic computing and computer algebra. The project involves the development of algorithms which use preprocessing and static analysis for matching and normalization with respect to static rules, and incremental algorithms for matching and normalization with respect to dynamic rule sets. Algorithms which learn efficiently from their history will be designed for normalization with respect to several important and useful classes of rewrite systems. The practical performance of our algorithms will be investigated. Techniques and sufficient conditions for the important unique normal form property for nonlinear rewrite systems and conditional rewrite systems will be devised. Abstract Church-Rosser properties will be investigated for hierarchical combinations of rewriting modulo equational theories. Existing sufficient conditions for the Church-Rosser property of nonlinear hierarchical combinations of ordinary and conditional rewrite systems will be generalized. Hierarchical combinations are the way in which most specifications and software are written. The project is expected to: (i) be useful in enhancing the efficiency and power of symbolic computation and computer algebra systems, (ii) provide understanding of the inherent/complexities of the involved operations, and (iii) yield new results, techniques and insight into two fundamental issues of rewrite systems, viz., uniqueness of normal forms and the Church-Rosser property.