- -

Partial Evaluation of Rewriting Logic Theories

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Partial Evaluation of Rewriting Logic Theories

Show simple item record

Files in this item

dc.contributor.advisor Alpuente Frasnedo, María es_ES
dc.contributor.advisor Escobar Román, Santiago es_ES
dc.contributor.author Cuenca Ortega, Ángel Eduardo es_ES
dc.date.accessioned 2019-11-04T15:27:28Z
dc.date.available 2019-11-04T15:27:28Z
dc.date.created 2019-09-27
dc.date.issued 2019-11-04 es_ES
dc.identifier.uri http://hdl.handle.net/10251/130206
dc.description.abstract [ES] La evaluación parcial de programas es una técnica general y potente de optimización de programas que preserva su semántica y tiene muchas aplicaciones relevantes. La optimización se consigue al especializar programas con respecto a una parte de sus datos de entrada, lo que produce un nuevo programa llamado residual o programa especializado tal que, al ejecutarlo con los datos de entrada restantes, producirá el mismo resultado que produce el programa original con todos sus datos de entrada. Los esquemas de evaluación parcial existentes no son aplicables a lenguajes expresivos basados en reglas como Maude, CafeOBJ, OBJ, ASF+SDF y ELAN, los cuales soportan: 1) sofisticados tipos estructurados con subtipos y sobrecarga de operadores; y 2) teorías ecuacionales modulo varias combinaciones de axiomas tales como asociatividad, conmutatividad e identidad. Esta tesis desarrolla las bases teóricas necesarias e ilustra los conceptos principales para su aplicación a programas expresivos escritos en el lenguaje Maude. El esquema de evaluación parcial presentado en esta tesis está basado en un algoritmo automático de desplegado que computa variantes de términos. Para asegurar la terminación del proceso de especialización se han diseñado algoritmos de alto rendimiento para la generalización ecuacional menos general con tipos ordenados y subsunción homeomórfica ecuacional con tipos ordenados. Se muestra que la técnica de evaluación parcial desarrollada es correcta y completa para teorías de reescritura convergentes que pueden contener varias combinaciones de axiomas de asociatividad, conmutatividad y/o identidad para diferentes operadores binarios. Finalmente se presenta Victoria, el primer evaluador parcial para teorías ecuacionales de tipos ordenados para el lenguaje Maude, y se demuestra la efectividad y el incremento en eficiencia ganado a través de experimentos realizados con ejemplos reales. es_ES
dc.description.abstract [CA] L'avaluació parcial de programes és una tècnica general i potent d'optimització de programes que preserva la seua semàntica i té moltes aplicacions rellevants. L'optimització s'aconseguix a l'especialitzar programes respecte a una part de les seues dades d'entrada, la qual cosa produïx un nou programa cridat residual o programa especialitzat tal que, a l'executar-ho amb les dades d'entrada restants, produirà el mateix resultat que produïx el programa original amb totes les seues dades d'entrada. Els esquemes d'avaluació parcial existents no són aplicables a llenguatges expressius basats en regles com Maude, CafeOBJ, OBJ, ASF+SDF i ELAN, els quals suporten: 1) sofisticats tipus estructurats amb subtipus i sobrecàrrega d'operadors; i 2) teories equacionals mòdul diverses combinacions d'axiomes com asociativitat, conmutativitat i identitat. Esta tesi desenrotlla les bases teòriques necessàries i il·lustra els conceptes principals per a la seua aplicació a programes expressius escrits en el llenguatge Maude. L'esquema d'avaluació parcial presentat en esta tesi està basat en un algoritme automàtic de desplegat que computa variants de termes. Per a assegurar la terminació del procés d'especialització s'han dissenyat algoritmes d'alt rendiment per a la generalització ecuacional menys general amb subtipus ordenats i subsunción ecuacional homeomórfica amb subtipus ordenats. Es mostra que la tècnica d'avaluació parcial desenrotllada és correcta i completa per a teories de reescriptura convergents que poden contindre diverses combinacions d'axiomes d'asociativitat, conmutativitat i identitat per a diferents operadors binaris. Finalment es presenta Victoria, el primer avaluador parcial per a teories equacionals de tipus ordenats per al llenguatge Maude i es demostra l'efectivitat i l'increment en eficiència guanyat a través d'experiments realitzats amb exemples reals. es_ES
dc.description.abstract [EN] Partial evaluation is a powerful and general program optimization technique that preserves program semantics and has many successful applications. Optimization is achieved by specializing programs w.r.t. a part of their input data so that, when the residual or specialized program is executed on the remaining input data, it produces the same outcome than the original program with all of its input data. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts, and overloading; and 2) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity. This thesis develops the new foundations needed and illustrates the key concepts of equational order sorted partial evaluation by showing how they apply to the specialization of expressive programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on high-performance order-sorted equational least general generalization and ordersorted equational homeomorphic embedding algorithms for ensuring termination.We show that our partial evaluation technique is sound and complete for order-sorted equational theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. Finally, we present Victoria, the first partial evaluator for Maude's order-sorted equational theories, and demonstrate the effectiveness of our partial evaluation scheme on several examples where it shows significant speed-up. es_ES
dc.description.sponsorship Finally, I extend my thanks to SENESCYT for the support provided for my studies. Also, I thank the Universidad de Guayaquil that is my place of work. es_ES
dc.language Inglés es_ES
dc.publisher Universitat Politècnica de València es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Partial evaluation es_ES
dc.subject Evaluación parcial es_ES
dc.subject Maude es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Partial Evaluation of Rewriting Logic Theories es_ES
dc.type Tesis doctoral es_ES
dc.identifier.doi 10.4995/Thesis/10251/130206 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 Cuenca Ortega, ÁE. (2019). Partial Evaluation of Rewriting Logic Theories [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/130206 es_ES
dc.description.accrualMethod TESIS es_ES
dc.type.version info:eu-repo/semantics/acceptedVersion es_ES
dc.relation.pasarela TESIS\10597 es_ES
dc.contributor.funder Secretaría de Educación Superior, Ciencia, Tecnología e Innovación, Ecuador es_ES


This item appears in the following Collection(s)

Show simple item record