- -

A Modular Order-sorted Equational Generalization Algorithm

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

  • Estadisticas de Uso

A Modular Order-sorted Equational Generalization Algorithm

Show simple item record

Files in this item

dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Espert Real, Javier es_ES
dc.contributor.author Meseguer, José es_ES
dc.date.accessioned 2015-02-12T13:00:48Z
dc.date.available 2015-02-12T13:00:48Z
dc.date.issued 2014-04
dc.identifier.issn 0890-5401
dc.identifier.uri http://hdl.handle.net/10251/46953
dc.description.abstract 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 rulebased languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. © 2014 Elsevier Inc. All rights reserved. 1. es_ES
dc.description.sponsorship 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. en_EN
dc.language Inglés es_ES
dc.publisher Elsevier es_ES
dc.relation.ispartof Information and Computation es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Unification es_ES
dc.subject Logic es_ES
dc.subject Inheritance es_ES
dc.subject Semantics es_ES
dc.subject Programs es_ES
dc.subject Algebra es_ES
dc.subject Terms es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title A Modular Order-sorted Equational Generalization Algorithm es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1016/j.ic.2014.01.006
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0905584/US/TC: Medium: Collaborative Research: Rewriting Logic Foundations for Verification and Programming of Next-Generation Trustworthy Web-Based Systems/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/NSF//0904749/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Escobar Román, S.; Espert Real, J.; Meseguer, J. (2014). A Modular Order-sorted Equational Generalization Algorithm. Information and Computation. 235:98-136. https://doi.org/10.1016/j.ic.2014.01.006 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion http://dx.doi.org/10.1016/j.ic.2014.01.006 es_ES
dc.description.upvformatpinicio 98 es_ES
dc.description.upvformatpfin 136 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 235 es_ES
dc.relation.senia 261760
dc.contributor.funder Ministerio de Ciencia e Innovación es_ES
dc.contributor.funder National Science Foundation, EEUU es_ES
dc.contributor.funder Generalitat Valenciana es_ES


This item appears in the following Collection(s)

Show simple item record