TY - JOUR

T1 - A modular order-sorted equational generalization algorithm

AU - Alpuente, María

AU - Escobar, Santiago

AU - Espert, Javier

AU - Meseguer, José

N1 - Funding Information:
M. Alpuente, S. Escobar, and J. Espert have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02 , and by Generalitat Valenciana PROMETEO2011/052 . J. Meseguer has been supported by NSF Grants CNS 09-04749 , and CCF 09-05584 .

PY - 2014/4

Y1 - 2014/4

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

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

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

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

U2 - 10.1016/j.ic.2014.01.006

DO - 10.1016/j.ic.2014.01.006

M3 - Article

AN - SCOPUS:84896401968

VL - 235

SP - 98

EP - 136

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

ER -