A modular order-sorted equational generalization algorithm

María Alpuente, Santiago Escobar, Javier Espert, José Meseguer

Research output: Contribution to journalArticlepeer-review


Generalization, also called anti-unification, is the dual of unification. Given terms t and t′, a generalizer is a term t″ of which t and t′ are substitution instances. The dual of a most general unifier (mgu) is that of least general generalizer (lgg). In this work, we extend the known untyped generalization algorithm to, first, an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; second, we extend it to work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and third, to the combination of both, which results in a modular, order-sorted equational generalization algorithm. Unlike the untyped case, there is in general no single lgg in our framework, due to order-sortedness or to the equational axioms. Instead, there is a finite, minimal and complete set of lggs, so that any other generalizer has at least one of them as an instance. Our generalization algorithms are expressed by means of inference systems for which we give proofs of correctness. This opens up new applications to partial evaluation, program synthesis, and theorem proving for typed equational reasoning systems and typed rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude.

Original languageEnglish (US)
Pages (from-to)98-136
Number of pages39
JournalInformation and Computation
StatePublished - Apr 2014

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics


Dive into the research topics of 'A modular order-sorted equational generalization algorithm'. Together they form a unique fingerprint.

Cite this