Algorithmic and Foundational Aspects of Rewriting

点击翻译按钮获取中文摘要

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.