Implementing term rewriting by jungle evaluation
Berthold Hoffmann, Detlef Plump · RAIRO - Theoretical Informatics and Applications · 1991
Jungles are acyclic hypergraphs which represent sets of terms such that common subterms can be shared. Term rewrite rules are translated into jungle evaluation rules which implement parallel term rewriting steps. By using additional hypergraph rules which "fold" equal subterms, even non-left-linear term rewriting systems can be implemented. As a side effect, these folding rules can speed up the evaluation process considerably. It is shown that terminating term rewriting systems result in terminating jungle evaluation systems which are capable to normalize every term. Moreover, confluent and terminating term rewriting systems give rise to confluent and terminating jungle evaluation systems, provided that the "garbage" produced by the evaluation steps is ignored. 1 Introduction Term rewriting is an interesting way of "computing by replacement" which is used in various areas of computing science: for the interpretation of functional and logical programming languages, for theorem...