Jungle evaluation for efficient term rewriting

Abstract

Jungles are acyclic hypergraphs that represent sets of terms over a signature so that equal subterms can be shared. Term rewrite rules can be translated into jungle evaluation rules having the property that each evaluation step performs several term rewrite steps simultaneously. It is shown that the translation preserves termination. Confluent and terminating term rewriting systems are translated into confluent and terminating jungle evaluation systems which are complete in the sense that each term normal form is represented by some jungle normal form. Moreover, jungle evaluation can be speeded up by additional hypergraph rules that fold equal terms without loosing termination and confluence. Using these folding rules, even non-linear term rewriting systems can be modelled.