Optimization of rewrite theories by equational partial evaluation.(English)Zbl 1477.68136

Summary: In this paper, we develop an automated optimization framework for rewrite theories that supports sorts, subsort overloading, equations and algebraic axioms with free/non-free constructors, and rewrite rules modeling concurrent system transitions whose state structure is defined by means of the equations. The main idea of the framework is to make the system computations more efficient by partially evaluating the equations to the specific calls that are required by the transition rules. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary and costly computations involving pattern matching and/or unification modulo equations and axioms. The transformation is based on a suitable unfolding operator parameter that relies on the symbolic operational engine of Maude’s equational theories, called folding variant narrowing, together with a generic abstraction operator. Depending on the properties of the rewrite theory, the unfolding and abstraction operators must be fine-tuned to achieve the biggest optimization possible while ensuring termination and total correctness of the transformation. We formalize two instances of our scheme for the case when the rewrite theory either has an infinite number of most general variants or a finite number of most general variants. Finally, we discuss some experimental results which demonstrate that the proposed optimization technique pays off in practice.

MSC:

 68Q42 Grammars and rewriting systems 68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

GLINTS; MTT; ACUOS2; Maude-NPA; Maude; ECCE
Full Text:

References:

 [1] Albert, E.; Alpuente, M.; Falaschi, M.; Julián, P.; Vidal, G., Improving control in functional logic program specialization, (Proceedings of the 5th International Symposium on Static Analysis. Proceedings of the 5th International Symposium on Static Analysis, SAS 1998. Proceedings of the 5th International Symposium on Static Analysis. Proceedings of the 5th International Symposium on Static Analysis, SAS 1998, Lecture Notes in Computer Science, vol. 1503 (1998), Springer), 262-277 · Zbl 0911.68036 [2] Albert, E.; Hanus, M.; Vidal, G., A practical partial evaluation scheme for multi-paradigm declarative languages, J. Funct. Logic Program., 2002, 1-34 (2002) · Zbl 1037.68011 [3] 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, (Proceedings of the 16th European Conference on Logics in Artificial Intelligence. Proceedings of the 16th European Conference on Logics in Artificial Intelligence, JELIA 2019. Proceedings of the 16th European Conference on Logics in Artificial Intelligence. Proceedings of the 16th European Conference on Logics in Artificial Intelligence, JELIA 2019, Lecture Notes in Computer Science, vol. 11468 (2019), Springer), 171-181 · Zbl 07169105 [4] Alpuente, M.; Ballis, D.; Escobar, S.; Sapiña, J., Narrowing-based optimization of rewrite theories, (Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2020 (2020)), Extended version in Tech. Report DSIC-UPV, 2020. Available at: [5] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., A partial evaluation framework for order-sorted equational programs modulo axioms, J. Log. Algebraic Methods Program., 110, 1-36 (2020) · Zbl 07161321 [6] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Meseguer, J., Order-sorted homeomorphic embedding modulo combinations of associativity and/or commutativity axioms, Fundam. Inform., 177, 3-4, 297-329 (2020) · Zbl 07350035 [7] Alpuente, M.; Cuenca-Ortega, A.; Escobar, S.; Sapiña, J., Inspecting Maude variants with GLINTS, Theory Pract. Log. Program., 17, 5-6, 689-707 (2017) [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.; Espert, J.; Meseguer, J., ACUOS: a system for modular ACU generalization with subtyping and inheritance, (Proceedings of the 14th European Conference on Logics in Artificial Intelligence. Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014. Proceedings of the 14th European Conference on Logics in Artificial Intelligence. Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014, Lecture Notes in Computer Science, vol. 8761 (2014), Springer), 573-581 · Zbl 1432.68422 [10] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., A modular equational generalization algorithm, (Proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation. Proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2008. Proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation. Proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2008, Lecture Notes in Computer Science, vol. 5438 (2008), Springer), 24-39 · Zbl 1185.68219 [11] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., Order-sorted generalization, Electron. Notes Theor. Comput. Sci., 246, 27-38 (2009) · Zbl 1347.68193 [12] Alpuente, M.; Escobar, S.; Meseguer, J.; Sapiña, J., Order-sorted equational generalization algorithm revisited, Ann. Math. Artif. Intell. (2021) [13] Alpuente, M.; Falaschi, M.; Julián, P.; Vidal, G., Specialization of lazy functional logic programs, (Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1997 (1997), Association for Computing Machinery), 151-162 [14] Alpuente, M.; Falaschi, M.; Moreno, G.; Vidal, G., Safe folding/unfolding with conditional narrowing, (Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming. Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, ALP 1997. Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming. Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, ALP 1997, Lecture Notes in Computer Science, vol. 1298 (1997), Springer), 1-15 · Zbl 0886.68033 [15] Alpuente, M.; Falaschi, M.; Vidal, G., Partial evaluation of functional logic programs, ACM Trans. Program. Lang. Syst., 20, 4, 768-844 (1998) [16] Alpuente, M.; Lucas, S.; Hanus, M.; Vidal, G., Specialization of functional logic programs based on needed narrowing, Theory Pract. Log. Program., 5, 3, 273-303 (2005) · Zbl 1092.68018 [17] Bae, K.; Escobar, S.; Meseguer, J., Abstract logical model checking of infinite-state systems using narrowing, (Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013. Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Leibniz International Proceedings in Informatics (LIPIcs), vol. 21 (2013), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 81-96 · Zbl 1356.68140 [18] Bouchard, C.; Gero, K. A.; Lynch, C.; Narendran, P., On forward closure and the finite variant property, (Proceedings of the 9th International Symposium on Frontiers of Combining Systems. Proceedings of the 9th International Symposium on Frontiers of Combining Systems, FroCos 2013. Proceedings of the 9th International Symposium on Frontiers of Combining Systems. Proceedings of the 9th International Symposium on Frontiers of Combining Systems, FroCos 2013, Lecture Notes in Computer Science, vol. 8152 (2013), Springer), 327-342 · Zbl 1398.68271 [19] Burstall, R. M.; Darlington, J., A transformation system for developing recursive programs, J. ACM, 24, 1, 44-67 (1977) · Zbl 0343.68014 [20] Clavel, M.; Durán, F.; Eker, S.; Escobar, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Rubio, R.; Talcott, C., Maude Manual (Version 3.0) (2020), SRI International Computer Science Laboratory, Available at: [21] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude: A High-Performance Logical Framework (2007), Springer · Zbl 1115.68046 [22] Comon-Lundh, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Proceedings of the 16th International Conference on Rewriting Techniques and Applications. Proceedings of the 16th International Conference on Rewriting Techniques and Applications, RTA 2005. Proceedings of the 16th International Conference on Rewriting Techniques and Applications. Proceedings of the 16th International Conference on Rewriting Techniques and Applications, RTA 2005, Lecture Notes in Computer Science, vol. 3467 (2005), Springer), 294-307 · Zbl 1078.68059 [23] De Schreye, D.; Glück, R.; Jørgensen, J.; Leuschel, M.; Martens, B.; Sørensen, M. H., Conjunctive partial deduction: foundations, control, algorithms, and experiments, J. Log. Program., 41, 2-3, 231-277 (1999) · Zbl 0944.68025 [24] Durán, F.; Eker, S.; Escobar, S.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., Associative unification and symbolic reasoning modulo associativity in Maude, (Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications. Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications, WRLA 2018. Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications. Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications, WRLA 2018, Lecture Notes in Computer Science, vol. 11152 (2018), Springer), 98-114 [25] Durán, F.; Lucas, S.; Meseguer, J., MTT: the Maude termination tool (system description), (Proceedings of the 4th International Joint Conference on Automated Reasoning. Proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR 2008. Proceedings of the 4th International Joint Conference on Automated Reasoning. Proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Lecture Notes in Computer Science, vol. 5195 (2008), Springer), 313-319 · Zbl 1165.68360 [26] Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Foundations of Security Analysis and Design V. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Foundations of Security Analysis and Design V. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, vol. 5705 (2009), Springer), 1-50 · Zbl 1252.94061 [27] Escobar, S.; Meseguer, J., Symbolic model checking of infinite-state systems using narrowing, (Proceedings of the 18th International Conference on Term Rewriting and Applications. Proceedings of the 18th International Conference on Term Rewriting and Applications, RTA 2007. Proceedings of the 18th International Conference on Term Rewriting and Applications. Proceedings of the 18th International Conference on Term Rewriting and Applications, RTA 2007, Lecture Notes in Computer Science, vol. 4533 (2007), Springer), 153-168 · Zbl 1203.68097 [28] Escobar, S.; Meseguer, J.; Sasse, R., Variant narrowing and equational unification, Electron. Notes Theor. Comput. Sci., 238, 3, 103-119 (2009) · Zbl 1347.68194 [29] 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 [30] Fay, M., First order unification in an equational theory, (Proceedings of the 4th International Conference on Automated Deduction. Proceedings of the 4th International Conference on Automated Deduction, CADE 1979 (1979), Academic Press, Inc.), 161-167 [31] Hanus, M.; Peemöller, B., A partial evaluator for curry, (Proceedings of the 28th International Workshop on (Constraint) Logic Programming. Proceedings of the 28th International Workshop on (Constraint) Logic Programming, WLP 2014, vol. 1335 (2014)), 155-171, CEUR-WS.org [32] Jones, N. D.; Gomard, C. K.; Sestoft, P., Partial Evaluation and Automatic Program Generation (1993), Prentice-Hall · Zbl 0875.68290 [33] Leuschel, M., Improving homeomorphic embedding for online termination, (Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation. Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation, LOPSTR 1998. Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation. Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation, LOPSTR 1998, Lecture Notes in Computer Science, vol. 1559 (1998), Springer), 199-218 [34] Lloyd, J. W.; Shepherdson, J. C., Partial evaluation in logic programming, J. Log. Program., 11, 3-4, 217-242 (1991) · Zbl 0741.68030 [35] Martens, B.; Gallagher, J., Ensuring global termination of partial deduction while allowing flexible polyvariance, (Proceedings of the 12th International Conference on Logic Programming. Proceedings of the 12th International Conference on Logic Programming, ICLP 1995 (1995), The MIT Press), 597-611 [36] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043 [37] Meseguer, J., Variant-based satisfiability in initial algebras, (Proceedings of the 4th International Workshop for Safety-Critical Systems. Proceedings of the 4th International Workshop for Safety-Critical Systems, FTSCS 2015. Proceedings of the 4th International Workshop for Safety-Critical Systems. Proceedings of the 4th International Workshop for Safety-Critical Systems, FTSCS 2015, Communications in Computer and Information Science, vol. 596 (2015), Springer), 3-34 · Zbl 1396.68074 [38] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080 [39] Meseguer, J., Generalized rewrite theories, coherence completion, and symbolic methods, J. Log. Algebraic Methods Program., 110 (2020) · Zbl 07161316 [40] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Equational abstractions, Theor. Comput. Sci., 403, 2-3, 239-264 (2008) · Zbl 1155.68050 [41] 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 [42] Middeldorp, A.; Hamoen, E., Counterexamples to completeness results for basic narrowing, (Proceedings of the 3rd International Conference on Algebraic and Logic Programming. Proceedings of the 3rd International Conference on Algebraic and Logic Programming, ALP 1992. Proceedings of the 3rd International Conference on Algebraic and Logic Programming. Proceedings of the 3rd International Conference on Algebraic and Logic Programming, ALP 1992, Lecture Notes in Computer Science, vol. 632 (1992), Springer), 244-258 [43] Ölveczky, P. C.; Meseguer, J., The real-time Maude tool, (Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2008. Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2008, Lecture Notes in Computer Science, vol. 4963 (2008), Springer), 332-336 [44] Peemöller, B., Normalization and partial evaluation of functional logic programs (2017), University of Kiel: University of Kiel Germany, PhD thesis [45] The Presto Website (2020), Available at: [46] Roşu, G., $$\mathbb{K}$$: a semantic framework for programming languages and formal analysis tools, (Dependable Software Systems Engineering. Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 50 (2017), IOS Press), 186-206 [47] Rodríguez, A.; Durán, F.; Rutle, A.; Kristensen, L. M., Executing multilevel domain-specific models in Maude, J. Object Technol., 18, 2, 1-21 (2019) [48] Skeirik, S.; Meseguer, J., Metalevel algorithms for variant satisfiability, J. Log. Algebraic Methods Program., 96, 81-110 (2018) · Zbl 1430.68423 [49] Slagle, J. R., Automated theorem-proving for theories with simplifiers, commutativity, and associativity, J. ACM, 21, 4, 622-642 (1974) · Zbl 0296.68092 [50] Viry, P., Equational rules for rewriting logic, Theor. Comput. Sci., 285, 2, 487-517 (2002) · Zbl 1001.68058
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.