A Modular Equational Generalization Algorithm?

Abstract. An important component for ensuring termination of many pro-gram manipulation techniques is the computation of least general generaliza-tions. In this paper, we present a modular equational generalization algorithm, where function symbols can have any combination of associativity, commu-tativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as program analizers, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.