TY - JOUR

T1 - Order-Sorted Generalization

AU - Alpuente, María

AU - Escobar, Santiago

AU - Meseguer, José

AU - Ojeda, Pedro

N1 - Funding Information:
1 Email: alpuente@dsic.upv.es 2 Email: sescobar@dsic.upv.es 3 Email: meseguer@cs.uiuc.edu 4 Email: pojeda@dsic.upv.es 5 This work has been partially supported by the EU (FEDER) and the Spanish MEC TIN2007-68093-C02-02 project, UPV PAID-06-07 project, and Generalitat Valenciana GV06/285 and BFPI/2007/076 grants.

PY - 2009/8/3

Y1 - 2009/8/3

N2 - 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.

AB - 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.

KW - least general generalization

KW - order-sorted reasoning

KW - partial evaluation

UR - http://www.scopus.com/inward/record.url?scp=67849124738&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=67849124738&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2009.07.013

DO - 10.1016/j.entcs.2009.07.013

M3 - Article

AN - SCOPUS:67849124738

VL - 246

SP - 27

EP - 38

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -