Algorithmic and Foundational Aspects of Rewriting

归一化，即根据一组称为重写系统的规则简化表达式，是几乎在所有符号计算和计算机代数系统中都可以找到的基本计算步骤。该操作的应用包括函数式、方程式和逻辑编程语言、抽象数据类型说明和验证、自动演绎、代码生成、类型推理和计算机代数。本提案解决了符号计算和计算机代数中这一重要问题的算法和基础方面。该项目涉及使用预处理和静态分析对静态规则进行匹配和规范化的算法的开发，以及用于对动态规则集进行匹配和规范化的增量算法。从其历史中有效学习的算法将被设计为针对几种重要且有用的重写系统进行规范化。我们的算法的实际性能将被研究。给出了非线性重写系统和条件重写系统重要的唯一范式性质的技术和充分条件。摘要研究改写模方程理论的分层组合的Church-Rosser性质。推广了普通系统和条件重写系统非线性层次组合的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.