Búsqueda avanzada

Partial Evaluation of Order-sorted Equational Programs modulo Axioms (Trabajo de alto nivel)


Partial evaluation (PE) is a powerful and general program optimization
technique with many successful applications. However, it has never been investigated
in the context of expressive rule-based languages like Maude, CafeOBJ,
OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts
and overloading; and equational rewriting modulo axioms such as commutativity,
associativity–commutativity, and associativity–commutativity–identity. In
this paper, we illustrate the key concepts by showing how they apply to partial
evaluation of expressive rule-based programs written in Maude. Our partial evaluation
scheme is based on an automatic unfolding algorithm that computes term
variants and relies on equational least general generalization for ensuring global
termination. We demonstrate the use of the resulting partial evaluator for program
optimization on several examples where it shows significant speed-ups.

Palabras Clave:

Equational Rewriting modulo Axioms - Maude - Partial Evaluation - Rewriting Logic





Este artículo tiene una licencia de uso CreativeCommons Reconocimiento (by)

Descarga el artículo haciendo click aquí.