Abstract
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.
This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2015-69175-C4-1-R and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana under grant PROMETEOII/2015/013, and by NSF grant CNS-1319109. Angel Cuenca-Ortega has been supported by the SENESCYT, Ecuador (scholarship program 2013).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In Maude 2.7, only equations with the variant attribute are used by the folding variant narrowing strategy, which is the only narrowing strategy considered in this paper. We sometimes remove the variant attribute for saving space.
- 2.
We assume there are no two grammar productions of the form N -> E.M \(_1\) and N -> E.M \(_2\).
- 3.
We show narrowing steps in solid arrows and rewriting steps in dotted arrows.
- 4.
From now on, we attach a label to each equation.
- 5.
To ease reading, the arcs of the narrowing tree are decorated with the label of the corresponding equation applied at the narrowing step.
- 6.
Note that this is only true because pattern matching modulo ACU is used for testing closedness.
- 7.
The expression X : S represents an explicit definition of a variable X of sort S. It is worth noting that Maude automatically provides B-coherence completion of rules.
References
Albert, E., Hanus, M., Vidal, G.: A practical partial evaluation scheme for multi-paradigm declarative languages. J. Funct. Logic Programm. 2002 (2002)
Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98–136 (2014)
Alpuente, M., Falaschi, M., Vidal, G.: Partial evaluation of functional logic programs. ACM Trans. Program. Lang. Syst. 20(4), 768–844 (1998)
Alpuente, M., Falaschi, M., Vidal, G.: A unifying view of functional and logic program specialization. ACM Comput. Surv. 30(3es), 9es (1998)
Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (version 2.7), March 2015
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7–8), 898–928 (2012)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Jørgensen, J., Leuschel, M., Martens, B.: Conjunctive partial deduction in practice. In: Gallagher, J. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 59–82. Springer, Heidelberg (1997). doi:10.1007/3-540-62718-9_5
Leuschel, M.: Improving homeomorphic embedding for online termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 199–218. Springer, Heidelberg (1999). doi:10.1007/3-540-48958-4_11
Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity and associativity. J. ACM 21(4), 622–642 (1974)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J. (2017). Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-63139-4_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63138-7
Online ISBN: 978-3-319-63139-4
eBook Packages: Computer ScienceComputer Science (R0)