Associative-commutative discrimination nets

Abstract

Use of discrimination nets for many-to-one pattern matching has been shown to dramatically improve the performance of the Knuth-Bendix completion procedure used in rewriting. Many important applications of rewriting require associative-commutative (AC) function symbols and it is therefore quite natural to expect performance gains by using similar techniques for AC-completion. In this paper we propose such a technique, called AC-discrimination net, that is a natural generalization of the standard discrimination net in the sense that if no AC-symbols are present in the pattern, it specializes to the standard discrimination net. Moreover we show how AC-discrimination nets can be augmented so as to further improve the performance of AC-matching on problems that are typically seen in practice.