TY - JOUR
T1 - A partial evaluation framework for order-sorted equational programs modulo axioms
AU - Alpuente, M.
AU - Cuenca-Ortega, A.
AU - Escobar, S.
AU - Meseguer, J.
N1 - Publisher Copyright:
© 2019 Elsevier Inc.
PY - 2020/1
Y1 - 2020/1
N2 - Partial evaluation is a powerful and general program optimization technique with many successful applications. 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. In this paper, we develop the new foundations needed and illustrate the key concepts by showing how they apply to partial evaluation 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 convergent rewrite theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. We demonstrate the effectiveness of Maude's automatic partial evaluator, Victoria, on several examples where it shows significant speed-ups.
AB - Partial evaluation is a powerful and general program optimization technique with many successful applications. 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. In this paper, we develop the new foundations needed and illustrate the key concepts by showing how they apply to partial evaluation 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 convergent rewrite theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. We demonstrate the effectiveness of Maude's automatic partial evaluator, Victoria, on several examples where it shows significant speed-ups.
UR - http://www.scopus.com/inward/record.url?scp=85082004977&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85082004977&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2019.100501
DO - 10.1016/j.jlamp.2019.100501
M3 - Article
AN - SCOPUS:85082004977
SN - 2352-2208
VL - 110
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
M1 - 100501
ER -