Order-Sorted Generalization

María Alpuente, Santiago Escobar, José Meseguer, Pedro Ojeda

Research output: Contribution to journalArticlepeer-review


Generalization, also called anti-unification, is the dual of unification. Given terms t and t, a generalization 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 generalization (lgg). In this work, we extend the known untyped generalization algorithm to an order-sorted typed setting with sorts, subsorts, and subtype polymorphism. Unlike the untyped case, there is in general no single lgg. Instead, there is a finite, minimal set of lggs, so that any other generalization has at least one of them as an instance. Our generalization algorithm is expressed by means of an inference system for which we give a proof of correctness. This opens up new applications to partial evaluation, program synthesis, and theorem proving for typed reasoning systems and typed rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude.

Original languageEnglish (US)
Pages (from-to)27-38
Number of pages12
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Aug 3 2009


  • least general generalization
  • order-sorted reasoning
  • partial evaluation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Order-Sorted Generalization'. Together they form a unique fingerprint.

Cite this