| Summary: | [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. === [CAT] 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. === [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. === 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. === 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 === TESIS
|
|---|
