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.