Systematic Development of a Pattern-Matching Algorithm Using Term Rewrite Systems

摘要

A term rewrite system is used to specify a pattern matcher in a code generator.The pattern matcher derived from the term rewrite system computes all the sequences of rewrite rules that will reduce a given expression tree to a given goal. While the number of sequences of rewrite rules that are generated is typically enormous, many sequences are in fact redundant. A theory and accompanying algorithms are developed that identify and remove these redundant rewrite sequences. These algorithms terminate if the term rewrite system is finite.