Partial Evaluation of Rewriting Logic Theories
Angel Cuenca Ortega · 2019
Partial evaluation is a powerful and general program optimization technique that preserves pro-gram 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 foundations of equational order sorted partial evaluation and illustrates the key concepts 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 order-sorted 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. ResumenLa 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.Resum 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.Acknowledgement Many people have contributed at this stage of my life, without them I would not have been able to finish this thesis.First of all I would like to thank my supervisors, María and Santiago, for their guidance and dedication during all these years.Without a doubt, I think there are no better supervisors than them.They always find a space in their busy schedules to help their students and share their knowledge.Their passion for research makes them an example for many young researchers.In truth, I feel very happy and fortunate to have been part of the ELP Group and, much more, to have done my thesis under the supervision of María and Santiago.I am very grateful to José Meseguer with whom I have had the pleasure to collaborate these years.