Mostrar el registro sencillo del ítem
dc.contributor.author | Lucas Alba, Salvador | es_ES |
dc.contributor.author | Meseguer, José | es_ES |
dc.date.accessioned | 2015-05-28T10:46:05Z | |
dc.date.available | 2015-05-28T10:46:05Z | |
dc.date.issued | 2014-11 | |
dc.identifier.issn | 0302-9743 | |
dc.identifier.uri | http://hdl.handle.net/10251/50899 | |
dc.description | The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-12904-4 10 | es_ES |
dc.description.abstract | This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems (CTRSs) as a special case. The results uncover some subtle issues about conditional termination. We first of all generalize a previous known result characterizing the operational termination of a CTRS by the quasi-decreasing ordering notion to a similar result for OSRTs. Second, we point out that the notions of *irreducible* term and of *normal form*, which coincide for unsorted rewriting are *totally different* for conditional rewriting and formally characterize that difference. We then define the notion of a *weakly operationally terminating* (or *weakly normalizing*) OSRT, give several evaluation mechanisms to compute normal forms in such theories, and investigate general conditions under which the rewriting-based operational semantics and the initial algebra semantics of a confluent OSRT coincide thanks to a notion of *canonical term algebra*. Finally, we investigate appropriate conditions and proof methods to ensure good executability properties of an OSRT for computing normal forms. | es_ES |
dc.description.sponsorship | Research partially supported by NSF grant CNS 13-19109. Salvador Lucas’ research was developed during a sabbatical year at the CS Dept. of the UIUC and was also partially supported by Spanish MECD grant PRX12/00214, MINECO project TIN2010-21062-C02-02, and GV grant BEST/2014/026 and project PROMETEO/2011/052. | es_ES |
dc.language | Inglés | es_ES |
dc.publisher | Springer Verlag (Germany) | es_ES |
dc.relation.ispartof | Rewriting Logic and Its Applications | es_ES |
dc.relation.ispartofseries | Lecture Notes in Computer Science;8663 | |
dc.rights | Reserva de todos los derechos | es_ES |
dc.subject | Conditional term rewriting | es_ES |
dc.subject | Strong and weak operational termination | es_ES |
dc.subject | Irreducible terms | es_ES |
dc.subject | Normalized terms | es_ES |
dc.subject | Rewriting logic | es_ES |
dc.subject | Maude | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Strong and weak operational termination of order-sorted rewrite theories | es_ES |
dc.type | Capítulo de libro | es_ES |
dc.identifier.doi | 10.1007/978-3-319-12904-4_10 | |
dc.relation.projectID | info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/MECD//PRX12%2F00214/ES/PRX12%2F00214/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GVA//BEST%2F2014%2F026/ | 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 | Lucas Alba, S.; Meseguer, J. (2014). Strong and weak operational termination of order-sorted rewrite theories. En Rewriting Logic and Its Applications. Springer Verlag (Germany). 178-194. https://doi.org/10.1007/978-3-319-12904-4_10 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.publisherversion | http://link.springer.com/chapter/10.1007/978-3-319-12904-4_10 | es_ES |
dc.description.upvformatpinicio | 178 | es_ES |
dc.description.upvformatpfin | 194 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.relation.senia | 276829 | |
dc.contributor.funder | National Science Foundation, EEUU | es_ES |
dc.contributor.funder | Ministerio de Educación, Cultura y Deporte | es_ES |
dc.contributor.funder | Generalitat Valenciana | es_ES |
dc.contributor.funder | Ministerio de Ciencia e Innovación | es_ES |