M. Widera and C. Beierle. A Term Rewriting Scheme for Function Symbols with Variable Arity. Informatik Berichte 280, FernUniversität Hagen, Januar 2001.
Term rewriting is used for programming tasks consisting of transformations of terms to simpler equivalent terms. In this context associative and commutative functions appear quite often. However, their transformations may be hard to understand when associativity and commutativity are not explicit in the transformation rules but coded into an additional set of equations. In this paper we present a notation for rewriting rules that makes associativity and commutativity explicit in the rewriting rules. As they are widely used in functional programming languages we allow the use of functions with variable number of arguments. Furthermore, our concept supports the commutative choice of certain arguments in a function call.