Implementing term rewriting by jungle evaluation

Abstract

Jungles are acyclic hypergraphs that represent sets of terms so that common subterms can be shared. Term rewrite rules are translated to jungle evaluation rules which implement parallel term rewriting steps. By 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.