×

A partial evaluation framework for order-sorted equational programs modulo axioms. (English) Zbl 07161321

Summary: 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
08A70 Applications of universal algebra in computer science
68Q42 Grammars and rewriting systems

Software:

ACUOS2; Maude; ChC 3; Curry; GLINTS
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Albert, E.; Alpuente, M.; Falaschi, M.; Julián, P.; Vidal, G., Improving control in functional logic program specialization, (Proc. of SAS ’98. Proc. of SAS ’98, LNCS, vol. 1503 (1998), Springer), 262-277 · Zbl 0911.68036
[2] Albert, E.; Alpuente, M.; Hanus, M.; Vidal, G., A partial evaluation framework for curry programs, (Ganzinger, H.; McAllester, D. A.; Voronkov, A., Proc. Logic Programming and Automated Reasoning, 6th International Conference. Proc. Logic Programming and Automated Reasoning, 6th International Conference, LPAR’99. Proc. Logic Programming and Automated Reasoning, 6th International Conference. Proc. Logic Programming and Automated Reasoning, 6th International Conference, LPAR’99, Lecture Notes in Computer Science, vol. 1705 (1999), Springer), 376-395
[3] Albert, E.; Hanus, M.; Vidal, G., A practical partial evaluation scheme for multi-paradigm declarative languages, J. Funct. Logic Program., 2002 (2002) · Zbl 1037.68011
[4] Alpuente, M.; Ballis, D.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., ACUOS^2: a high-performance system for modular ACU generalization with subtyping and inheritance, (Calimeri, F.; Leone, N.; Manna, M., Logics in Artificial Intelligence - 16th European Conference. Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings. Logics in Artificial Intelligence - 16th European Conference. Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11468 (2019), Springer), 171-181
[5] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Partial evaluation of order-sorted equational programs modulo axioms, (Proc. of 26th Int’l Symposium on Logic-Based Program Synthesis and Transformation. Proc. of 26th Int’l Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016. Proc. of 26th Int’l Symposium on Logic-Based Program Synthesis and Transformation. Proc. of 26th Int’l Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, LNCS, vol. 10184 (2017), Springer), 3-20 · Zbl 1485.68050
[6] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Homeomorphic embedding modulo combinations of associativity and commutativity axioms, (Mesnard, F.; Stuckey, P. J., Logic-Based Program Synthesis and Transformation - 28th International Symposium. Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. Logic-Based Program Synthesis and Transformation - 28th International Symposium. Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers, Lecture Notes in Computer Science, vol. 11408 (2018), Springer), 38-55
[7] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Order-sorted homeomorphic embedding modulo combinations of associativity and/or commutativity axioms, Fundam. Inform. (2019), in press
[8] Alpuente, M.; Escobar, S.; Espert, J.; Meseguer, J., A modular order-sorted equational generalization algorithm, Inf. Comput., 235, 98-136 (2014) · Zbl 1314.68169
[9] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., Order-sorted generalization, Electron. Notes Theor. Comput. Sci., 246, 27-38 (2009) · Zbl 1347.68193
[10] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., A modular equational generalization algorithm, (Hanus, M., Logic-Based Program Synthesis and Transformation - 18th International Symposium. Logic-Based Program Synthesis and Transformation - 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers. Logic-Based Program Synthesis and Transformation - 18th International Symposium. Logic-Based Program Synthesis and Transformation - 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5438 (2009), Springer), 24-39 · Zbl 1185.68219
[11] Alpuente, M.; Escobar, S.; Sapiña, J.; Cuenca-Ortega, A., Inspecting Maude variants with GLINTS, Theory Pract. Log. Program., 17, 5-6, 689-707 (2017)
[12] Alpuente, M.; Falaschi, M.; Julián, P.; Vidal, G., Specialization of lazy functional logic programs, (Proc. of the ACM SIGPLAN Conf. on Partial Evaluation and Semantics-Based Program Manipulation. Proc. of the ACM SIGPLAN Conf. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM’97 (1997), ACM: ACM New York), 151-162
[13] Alpuente, M.; Falaschi, M.; Vidal, G., Narrowing-driven partial evaluation of functional logic programs, (Nielson, H. R., Proc. of the 6th European Symp. on Programming. Proc. of the 6th European Symp. on Programming, ESOP’96. Proc. of the 6th European Symp. on Programming. Proc. of the 6th European Symp. on Programming, ESOP’96, LNCS, vol. 1058 (1996), Springer), 45-61
[14] Alpuente, M.; Falaschi, M.; Vidal, G., Partial evaluation of functional logic programs, ACM Trans. Program. Lang. Syst., 20, 4, 768-844 (1998)
[15] Alpuente, M.; Falaschi, M.; Vidal, G., A unifying view of functional and logic program specialization, ACM Comput. Surv., 30, 3 (1998), pp. 9 · Zbl 0911.68036
[16] Baader, F.; Snyder, W., Unification theory, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 445-532, (in 2 volumes) · Zbl 1011.68126
[17] Bol, R., Loop checking in partial deduction, J. Log. Program., 16, 1-2, 25-46 (1993) · Zbl 0780.68012
[18] Bouchard, C.; Gero, K. A.; Lynch, C.; Narendran, P., On forward closure and the finite variant property, (Proc. of the 9th Int’l Symposium on Frontiers of Combining Systems. Proc. of the 9th Int’l Symposium on Frontiers of Combining Systems, FroCos 2013. Proc. of the 9th Int’l Symposium on Frontiers of Combining Systems. Proc. of the 9th Int’l Symposium on Frontiers of Combining Systems, FroCos 2013, Lecture Notes in Computer Science, vol. 8152 (2013), Springer-Verlag: Springer-Verlag Berlin), 327-342 · Zbl 1398.68271
[19] Bruynooghe, M.; De Schreye, D.; Martens, B., A general criterion for avoiding infinite unfolding during partial deduction of logic programs, (Saraswat, V.; Ueda, K., Proc. 1991 Int’l Symp. on Logic Programming (1991)), 117-131
[20] Bürckert, H.; Herold, A.; Schmidt-Schauß, M., On equational theories, unification, and (un)decidability, J. Symb. Comput., 8, 1-2, 3-49 (1989) · Zbl 0684.03004
[21] Burstall, R.; Darlington, J., A transformation system for developing recursive programs, J. ACM, 24, 1, 44-67 (1977) · Zbl 0343.68014
[22] Cadar, C.; Sen, K., Symbolic execution for software testing: three decades later, Commun. ACM, 56, 2, 82-90 (Feb. 2013)
[23] Cholewa, A.; Meseguer, J.; Escobar, S., Variants of Variants and the Finite Variant Property (February 2014), CS Dept. University of Illinois at Urbana-Champaign, Technical report
[24] Christensen, N. H.; Glück, R., Offline partial evaluation can be as accurate as online partial evaluation, ACM Trans. Program. Lang. Syst., 26, 1, 191-220 (2004)
[25] Comon-Lundh, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Giesl, J., RTA. RTA, Lecture Notes in Computer Science, vol. 3467 (2005), Springer), 294-307 · Zbl 1078.68059
[26] Cook, W. R.; Lämmel, R., Tutorial on online partial evaluation, (Danvy, O.; Shan, C., Proc. IFIP Working Conference on Domain-Specific Languages. Proc. IFIP Working Conference on Domain-Specific Languages, DSL 2011. Proc. IFIP Working Conference on Domain-Specific Languages. Proc. IFIP Working Conference on Domain-Specific Languages, DSL 2011, EPTCS, vol. 66 (2011)), 168-180
[27] (Danvy, O.; Glück, R.; Thiemann, P., Partial Evaluation, Int’l Seminar. Partial Evaluation, Int’l Seminar, Dagstuhl Castle, Germany. Partial Evaluation, Int’l Seminar. Partial Evaluation, Int’l Seminar, Dagstuhl Castle, Germany, LNCS, vol. 1110 (1996), Springer)
[28] Darlington, J.; Guo, Y.; Pull, H., Constraints Unify Functional and Logic Programming (1991), Department of Computing, Imperial College: Department of Computing, Imperial College London, Technical report
[29] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics (1990), Elsevier: Elsevier Amsterdam), 243-320 · Zbl 0900.68283
[30] Dershowitz, N.; Jouannaud, J.-P., Notations for rewriting, Bull. Eur. Assoc. Theor. Comput. Sci., 43, 162-172 (1991) · Zbl 0745.68115
[31] Durán, F.; Eker, S.; Escobar, S.; Martí-Oliet, N.; Meseguer, J.; Rubio, R.; Talcott, C., Programming and symbolic computation in Maude, J. Log. Algebraic Methods Program., 110, Article 100497 pp. (2020), in this issue
[32] Durán, F.; Eker, S.; Escobar, S.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., Associative unification and symbolic reasoning modulo associativity in Maude, (Rusu, V., Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11152 (2018), Springer), 98-114
[33] Durán, F.; Meseguer, J., A Maude coherence checker tool for conditional order-sorted rewrite theories, (Ölveczky, P. C., WRLA. WRLA, Lecture Notes in Computer Science, vol. 6381 (2010), Springer), 86-103 · Zbl 1306.68066
[34] Eker, S., Associative-commutative rewriting on large terms, (Nieuwenhuis, R., Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Proceedings. Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706 (2003), Springer), 14-29 · Zbl 1038.68560
[35] Escobar, S.; Meseguer, J.; Sasse, R., Variant narrowing and equational unification, Electron. Notes Theor. Comput. Sci., 238, 3, 103-119 (2009) · Zbl 1347.68194
[36] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebraic Program., 81, 7-8, 898-928 (2012) · Zbl 1291.68217
[37] Fay, M., First order unification in an equational theory, (Proc of 4th Int’l Conf. on Automated Deduction. Proc of 4th Int’l Conf. on Automated Deduction, CADE’79 (1979)), 161-167
[38] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056
[39] Hanus, M., The integration of functions into logic programming: from theory to practice, J. Log. Program., 20, 583 (1994) · Zbl 0942.68526
[40] Hanus, M., Functional logic programming: from theory to curry, (Voronkov, A.; Weidenbach, C., Programming Logics - Essays in Memory of Harald Ganzinger. Programming Logics - Essays in Memory of Harald Ganzinger, Lecture Notes in Computer Science, vol. 7797 (2013), Springer), 123-168 · Zbl 1383.68017
[41] Hanus, M.; Peemöller, B., A partial evaluator for curry, (Proc. of 23rd International Workshop on Functional and (Constraint) Logic Programming. Proc. of 23rd International Workshop on Functional and (Constraint) Logic Programming, WFLP 2014 (2014), Universität Halle-Wittenberg), 55-71
[42] Jones, N.; Gomard, C.; Sestoft, P., Partial Evaluation and Automatic Program Generation (1993), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0875.68290
[43] Jørgensen, J.; Leuschel, M.; Martens, B., Conjunctive partial deduction in practice, (Proc. of LOPSTR’96. Proc. of LOPSTR’96, LNCS, vol. 1207 (1996), Springer), 59-82
[44] Jouannaud, J.-P.; Kirchner, C.; Kirchner, H., Incremental construction of unification algorithms in equational theories, (Proc. of 10th Colloquium on Automata, Languages and Programming. Proc. of 10th Colloquium on Automata, Languages and Programming, ICALP 1983. Proc. of 10th Colloquium on Automata, Languages and Programming. Proc. of 10th Colloquium on Automata, Languages and Programming, ICALP 1983, LNCS, vol. 154 (1983), Springer), 361-373
[45] Lafave, L.; Gallagher, J. P., Constraint-based partial evaluation of rewriting-based functional logic programs, (Fuchs, N. E., Proc. Logic Programming Synthesis and Transformation, 7th International Workshop, LOPSTR’97. Proc. Logic Programming Synthesis and Transformation, 7th International Workshop, LOPSTR’97, Lecture Notes in Computer Science, vol. 1463 (1998), Springer), 168-188
[46] Leuschel, M., Advanced Techniques for Logic Program Specialisation (1997), PhD thesis
[47] Leuschel, M., Improving homeomorphic embedding for online termination, (Flener, P., Proc. of 8th International Workshop on Logic Programming Synthesis and Transformation. Proc. of 8th International Workshop on Logic Programming Synthesis and Transformation, LOPSTR 1998. Proc. of 8th International Workshop on Logic Programming Synthesis and Transformation. Proc. of 8th International Workshop on Logic Programming Synthesis and Transformation, LOPSTR 1998, LNCS, vol. 1559 (1998), Springer), 199-218
[48] Leuschel, M.; Bruynooghe, M., Logic program specialisation through partial deduction: control issues, Theory Pract. Log. Program., 2, 4-5, 461-515 (2002) · Zbl 1105.68331
[49] Leuschel, M.; Craig, S.; Elphick, D., Supervising offline partial evaluation of logic programs using online techniques, (Puebla, G., Logic-Based Program Synthesis and Transformation, 16th International Symposium. Logic-Based Program Synthesis and Transformation, 16th International Symposium, LOPSTR 2006, Venice, Italy, July 12-14, 2006, Revised Selected Papers. Logic-Based Program Synthesis and Transformation, 16th International Symposium. Logic-Based Program Synthesis and Transformation, 16th International Symposium, LOPSTR 2006, Venice, Italy, July 12-14, 2006, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4407 (2007), Springer), 43-59 · Zbl 1196.68033
[50] Lloyd, J.; Shepherdson, J., Partial evaluation in logic programming, J. Log. Program., 11, 217-242 (1991) · Zbl 0741.68030
[51] Martens, B.; Gallagher, J., Ensuring global termination of partial deduction while allowing flexible polyvariance, (Sterling, L., Proc. of ICLP’95 (1995), MIT Press), 597-611
[52] Melliès, P., On a duality between Kruskal and Dershowitz theorem, (Larsen, K. G.; Skyum, S.; Winskel, G., ICALP. ICALP, Lecture Notes in Computer Science, vol. 1443 (1998), Springer), 518-529 · Zbl 0921.04001
[53] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[54] Meseguer, J., Membership algebra as a logical framework for equational specification, (Parisi-Presicce, F., Proc. of 12th International Workshop on Recent Trends in Algebraic Development Techniques. Proc. of 12th International Workshop on Recent Trends in Algebraic Development Techniques, WADT’97. Proc. of 12th International Workshop on Recent Trends in Algebraic Development Techniques. Proc. of 12th International Workshop on Recent Trends in Algebraic Development Techniques, WADT’97, LNCS, vol. 1376 (1997), Springer), 18-61 · Zbl 0903.08009
[55] Meseguer, J., Order-sorted rewriting and congruence closure, (Jacobs, B.; Löding, C., Foundations of Software Science and Computation Structures - 19th International Conference. Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016. Foundations of Software Science and Computation Structures - 19th International Conference. Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Lecture Notes in Computer Science, vol. 9634 (2016), Springer), 493-509 · Zbl 1475.68142
[56] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080
[57] Meseguer, J., Variant-based satisfiability in initial algebras, Sci. Comput. Program., 154, 3-41 (2018) · Zbl 1396.68074
[58] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symb. Comput., 20, 1-2, 123-160 (2007) · Zbl 1115.68079
[59] Plotkin, G., A note on inductive generalization, (Machine Intelligence, vol. 5 (1970), Edinburgh University Press), 153-163 · Zbl 0219.68045
[60] Rusu, V.; Lucanu, D.; Serbanuta, T.; Arusoaie, A.; Stefanescu, A.; Rosu, G., Language definitions as rewrite theories, J. Log. Algebraic Methods Program., 85, 1, 98-120 (2016) · Zbl 1356.68125
[61] Slagle, J., Automated theorem-proving for theories with simplifiers, commutativity and associativity, J. ACM, 21, 4, 622-642 (1974) · Zbl 0296.68092
[62] Thati, P.; Meseguer, J., Complete symbolic reachability analysis using back-and-forth narrowing, Theor. Comput. Sci., 366, 1-2, 163-179 (2006) · Zbl 1110.68058
[63] Viry, P., Equational rules for rewriting logic, Theor. Comput. Sci., 285, 2, 487-517 (2002) · Zbl 1001.68058
[64] Wadler, P., Deforestation: transforming programs to eliminate trees, Theor. Comput. Sci., 73, 231-248 (1990) · Zbl 0701.68013
[65] Weise, D.; Conybeare, R.; Ru, E.; Seligman, S., Automatic online partial evaluation, (Hughes, J., FPCA. FPCA, Lecture Notes in Computer Science, vol. 523 (1991), Springer), 165-191
[66] Würthinger, T.; Wimmer, C.; Humer, C.; Wöß, A.; Stadler, L.; Seaton, C.; Duboscq, G.; Simon, D.; Grimmer, M., Practical partial evaluation for high-performance dynamic language runtimes, (Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 (2017), ACM: ACM New York, NY, USA), 662-676
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.