Introduction

• An important component for ensuring termination of many program manipulation techniques is the computation of least general generalizations.
  In this work, we present:
  • A modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, 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.
    You can compute the ACU least generalizations in the ACU Lgg section.
     
  • We extend the known untyped generalization algorithm to an order-sorted typed setting with sorts, subsorts, and subtype polymorphism.
    You can compute the ACU order sorted least generalizations in the ACU Order Sorted Lgg section.
     
• Our 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.
   
• You can find a more detailed description of the tool here.