Rewriting in Practice*

摘要

The field of rewriting is broadly concerned with manipulating representations of objects so that we go from a larger representation to a smaller representation. The field of rewriting has contributed some fundamental results within the computer science discipline. This extended abstract explores a few impactful applications of rewriting in the areas of (a) design of algorithms, (b) formal modeling and analysis, and (c) term rewriting and theorem proving. The theory of rewriting can be used as a basis to study the design and analysis of algorithms in at least two distinct ways. First, an algorithm can often be viewed as a set of rewrite rules. A rewrite-based description of algorithms cleanly separates the logical part of an algorithm from the implementation details. This applies to large class of algorithms including graph algorithms, sorting algorithms, and combinatorial algorithms. Second, rewriting provides a general paradigm for the design of algorithms. The (abstract) critical-pair