Compilation of pattern matching with associative-commutative functions

Abstract

This paper deals with the problem of compiling pattern-matching of associative-commutative function definitions in a functional-like language where the evaluation is performed by head-rewriting. We propose an effective algorithm (i.e which does not rely on some -unknown- procedure for computing complements of terms modulo AC-axioms) to compile the pattern-matching process. For this purpose, we introduce the concept of pattern trees. We also get for free a test of the completeness of such definitions (with respect to head-rewriting), provided some linearity condition is met. Our method will ensure an efficient pattern-matching process at evaluation time.