zbMATH — the first resource for mathematics

Rewriting strategies and strategic rewrite programs. (English) Zbl 1321.68331
Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 380-403 (2015).
Summary: This survey aims at providing unified definitions of strategies, strategic rewriting and strategic programs. It gives examples of main constructs and languages used to write strategies. It also explores some properties of strategic rewriting and operational semantics of strategic programs. Current research topics are identified.
For the entire collection see [Zbl 1319.68011].

68Q42 Grammars and rewriting systems
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI
[1] Alpuente, M., Escobar, S., Lucas, S.: Correct and complete (positive) strategy annotations for OBJ. In: Proceedings of the 5th International Workshop on Rewriting Logic and its Applications (WRLA) , vol. 71, Elecronic Notes in Theoretical Computer Science, pp. 70–89 (2004) · Zbl 1272.68071 · doi:10.1016/S1571-0661(05)82529-0
[2] Andrei, O., Fernandez, M., Kirchner, H., Melançon, G., Namet, O., Pinaud, B.: PORGY: strategy-driven interactive transformation of graphs. In: Echahed, R. (ed.) TERMGRAPH, 6th International Workshop on Computing with Terms and Graphs, vol. 48, Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 54–68 (2011) · doi:10.4204/EPTCS.48.7
[3] Andrei, O., Kirchner, H.: A port graph calculus for autonomic computing and invariant verification. Electron. Notes Theor. Comput. Sci. 253(4), 17–38 (2009) · Zbl 1291.68241 · doi:10.1016/j.entcs.2009.10.015
[4] Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006) · Zbl 1107.68091 · doi:10.1016/j.jal.2005.10.002
[5] Antoy, S., Middeldorp, A.: A sequential reduction strategy. Theor. Comput. Sci. 165(1), 75–95 (1996) · Zbl 0872.68080 · doi:10.1016/0304-3975(96)00041-2
[6] Augustsson, L.: A compiler for lazy ML. In: Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, LFP 1984, pp. 218–227, New York, NY, USA. ACM (1984) · doi:10.1145/800055.802038
[7] Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: piggybacking rewriting on java. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 36–47. Springer, Heidelberg (2007) · Zbl 05222802 · doi:10.1007/978-3-540-73449-9_5
[8] Balland, E., Moreau, P.-E., Reilles, A.: Effective strategic programming for java developers. Softw. Pract. Exp. 44(2), 129–162 (2012) · doi:10.1002/spe.2159
[9] Barendregt, H.: The Lambda-calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, Second edition. Elsevier Science Publishers B. V. (North-Holland), Amsterdam (1984) · Zbl 0551.03007
[10] Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)
[11] Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285(2), 155–185 (2002) · Zbl 1001.68057 · doi:10.1016/S0304-3975(01)00358-9
[12] Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C.: An overview of ELAN. Electr. Notes Theor. Comput. Sci. 15, 55–70 (1998) · Zbl 0917.68022 · doi:10.1016/S1571-0661(05)82552-6
[13] Borovanský, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. Int. J. Found. Comput. Sci. 12(1), 69–98 (2001) · Zbl 1319.68125 · doi:10.1142/S0129054101000412
[14] Bourdier, T., Cirstea, H., Dougherty, D.J., Kirchner, H.: Extensional and intensional strategies. In: Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, vol. 15, Electronic Proceedings in Theoretical Computer Science, pp. 1–19 (2009)
[15] Castro, C.: Building constraint satisfaction problem solvers using rewrite rules and strategies. Fundamenta Informaticae 34(3), 263–293 (1998) · Zbl 0943.68095
[16] Cirstea, H., Kirchner, C., Liquori, L., Wack, B.: Rewrite strategies in the rewriting calculus. In: Gramlich, B., Lucas, S. (eds.) Electronic Notes in Theoretical Computer Science, vol. 86. Elsevier (2003) · Zbl 1270.68122 · doi:10.1016/S1571-0661(05)82613-1
[17] Cirstea, H., Kirchner, C.: The rewriting calculus - Part I and II. Logic J. Interest Gr. Pure Appl. Logics 9(3), 427–498 (2001) · Zbl 0986.03027
[18] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. Programming and Software Engineering, vol. 4350. Springer, Heidelberg (2007) · Zbl 1115.68046
[19] de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15–44. Springer, Heidelberg (2013) · Zbl 1383.68084 · doi:10.1007/978-3-642-36675-8_2
[20] Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000) · Zbl 0988.68584 · doi:10.1007/3-540-44404-1_7
[21] Dijkstra, E.W.: Selected Writings on Computing - A Personal Perspective. Texts and Monographs in Computer Science. Springer, New York (1982) · doi:10.1007/978-1-4612-5695-3
[22] Dougherty, D.J.: Rewriting strategies and game strategies. Internal report, August 2008
[23] Ermel, C., Rudolf, M., Taentzer, G.: The AGG approach: language and environment. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformations: Applications, Languages, and Tools, pp. 551–603. World Scientific, Singapore (1997)
[24] Fernández, M., Kirchner, H., Namet, O.: A strategy language for graph rewriting. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 173–188. Springer, Heidelberg (2012) · Zbl 1239.68008 · doi:10.1007/978-3-642-29344-3
[25] Fernández, M., Kirchner, H., Namet, O.: Strategic portgraph rewriting: an interactive modelling and analysis framework. In: Lafuente, A.L., Bosnacki, D., Edelkamp, S., Wij, A. (eds.) Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014), Grenoble, France, 5th April 2014, vol. 159, Electronic Proceedings in Theoretical Computer Science, pp. 15–29 (2014)
[26] Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Reid, B. (ed.) Proceedings 12th ACM Symposium on Principles of Programming Languages, pp. 52–66. ACM Press (1985) · doi:10.1145/318593.318610
[27] Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: a fast SPO-based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 383–397. Springer, Heidelberg (2006) · Zbl 1156.68427 · doi:10.1007/11841883_27
[28] Giesl, J., Middeldorp, A.: Innermost termination of context-sensitive rewriting. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol. 2450, pp. 231–244. Springer, Heidelberg (2003) · Zbl 1015.68106 · doi:10.1007/3-540-45005-X_20
[29] Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7:1–7:39 (2011) · doi:10.1145/1890028.1890030
[30] Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Trans. Comput. Logic 10(2), 1–52 (2009) · Zbl 1351.68129 · doi:10.1145/1462179.1462182
[31] Goguen, J., Malcolm, G. (eds.): Software Engineering with OBJ: Algebraic Specification in Action. Advances in Formal Methods. Kluwer Academic Publishers, Boston (2000). ISBN 0-7923-7757-5
[32] Gordon, M., Milner, R., Morris, L., Newey, M., Wadsworth, C.: A metalanguage for interactive proof in LCF. In: Proceedings of 5th ACM Symposium on Principles of Programming Languages, pp. 119–130. ACM Press, January 1978 · doi:10.1145/512760.512773
[33] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. LNCS, vol. 2500. Springer, Heidelberg (2002)
[34] Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comput. Sci. 11(5), 637–688 (2001) · Zbl 0987.18005 · doi:10.1017/S0960129501003425
[35] Habel, A., Plump, D.: Computational completeness of programming languages based on graph transformation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 230–245. Springer, Heidelberg (2001) · Zbl 0978.68028 · doi:10.1007/3-540-45315-6_15
[36] Hanus, M.: Curry: a multi-paradigm declarative language (system description). In: Twelfth Workshop Logic Programming (WLP 1997), Munich (1997)
[37] Huet, G., Lévy, J.-J.: Computations in non-ambiguous linear term rewriting systems. Technical report, INRIA Laboria (1979)
[38] Huet, G., Lévy, J.-J..: Computations in orthogonal rewriting systems, I and II. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, chapter 11, 12, pp. 395–414. MIT press (1991)
[39] Jones, S.L.P.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003) · Zbl 1067.68041
[40] Kechri, A.S.: Classical Descriptive Set Theory. Graduate Texts in Mathematics, vol. 156. Springer, New York (1995) · doi:10.1007/978-1-4612-4190-4
[41] Kirchner, C., Kirchner, F., Kirchner, H.: Strategic computations and deductions. In: Benzmüller, C., Brown, C.E.., Siekmann, J., Statman, R. (eds.) Reasoning in Simple Type Theory. Festchrift in Honour of Peter B. Andrews on His 70th Birthday, vol. 17, Studies in Logic and the Foundations of Mathematics, pp. 339–364. College Publications (2008) · Zbl 1226.03027
[42] Kirchner, C., Kirchner, F., Kirchner, H.: Constraint based strategies. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol. 5979, pp. 13–26. Springer, Heidelberg (2010) · Zbl 1274.68410 · doi:10.1007/978-3-642-11999-6_2
[43] Kirchner, C., Kirchner, H., Vittek, M.: Implementing computational systems with constraints. In: Principles and Practice of Constraint Programming, pp. 156–165 (1993)
[44] Kirchner, C., Kirchner, H., Vittek, M.: Designing constraint logic programming languages using computational systems. In: Van Hentenryck, P., Saraswat, V. (eds.) Principles and Practice of Constraint Programming. The Newport Papers, chapter 8, pp. 131–158. The MIT Press (1995)
[45] Kirchner., H.: A rewriting point of view on strategies. In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Proceedings 1st International Workshop on Strategic Reasoning(SR 2013), Rome, Italy, March 16–17, vol. 112, Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 99–105 (2013)
[46] Letichevsky, A.: Development of rewriting strategies. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714. Springer, Heidelberg (1993) · Zbl 0794.68077
[47] Lévy, J.-J.: Optimal reductions in the lambda-calculus. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 159–191. Academic Press, New York (1980)
[48] Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Func. Logic Program. 1, 1–61 (1998) · Zbl 0924.68106
[49] Lucas, S.: Termination of on-demand rewriting and termination of OBJ programs. In: Sondergaard, H. (ed.) Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pp. 82–93, Firenze, Italy, September 2001. ACM Press, New York (2001) · doi:10.1145/773184.773194
[50] Lucas, S.: Termination of rewriting with strategy annotations. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 669–684. Springer, Heidelberg (2001) · Zbl 1275.68084 · doi:10.1007/3-540-45653-8_46
[51] Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446–453 (2015) · Zbl 1185.68374 · doi:10.1016/j.ipl.2005.05.002
[52] Lucas, S., Meseguer, J.: Strong and weak operational termination of order-sorted rewrite theories. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 178–194. Springer, Heidelberg (2014) · Zbl 1367.68144 · doi:10.1007/978-3-319-12904-4_10
[53] Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Meseguer, J. (ed.) Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier Science Publishers (2000) · Zbl 0912.68096
[54] Martí-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for maude. In: Martí-Oliet, N. (ed.) Proceedings Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Barcelona, Spain, March 27 - April 4, vol. 117, Electronic Notes in Theoretical Computer Science, pp. 417–441. Elsevier Science Publishers B. V. (North-Holland) (2005) · doi:10.1016/j.entcs.2004.06.020
[55] Martí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electron. Notes Theor. Comput. Sci. 238(3), 227–247 (2008) · Zbl 1347.68199 · doi:10.1016/j.entcs.2009.05.022
[56] McCune, W.: Semantic guidance for saturation provers. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 18–24. Springer, Heidelberg (2006) · Zbl 1156.68570 · doi:10.1007/11856290_4
[57] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[58] Nickel, U., Niere, J., Zündorf, A.: The FUJABA environment. In: ICSE, pp. 742–745 (2000) · doi:10.1145/337180.337620
[59] O’Donnell, M.J. (ed.): Computing in Systems Described by Equations. LNCS. Springer, Heidelberg (1977)
[60] Okamoto, K., Sakai, M., Nishida, N., Sakabe, T.: Weakly-innermost strategy and its completeness on terminating right-linear TRSs. In: Proceedings 5th International Workshop on Reduction Strategies in Rewriting and Programming April 22: Nara, p. 2005. ENTCS, Japan (2005)
[61] Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
[62] Plasmeijer, M.J., van Eekelen, M.C.J.D.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Boston (1993) · Zbl 0788.68023
[63] Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)
[64] Plump, D.: The graph programming language GP. In: Bozapalidis, S., Rahonis, G. (eds.) CAI 2009. LNCS, vol. 5725, pp. 99–122. Springer, Heidelberg (2009) · Zbl 1256.68023 · doi:10.1007/978-3-642-03564-7_6
[65] Plump, D., Steinert, S.: The semantics of graph programs. In: Mackie, L., Moreira, A.M. (eds.) Proceedings Tenth International Workshop on Rule-Based Programming (RULE 2009), Brasília, Brazil, 28th June 2009, vol. 21, Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 27–38 (2009)
[66] Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004) · doi:10.1007/978-3-540-25959-6_40
[67] Schürr, A., Winter, A.J., Zündorf, A.: The PROGRES approach: language and environment. In: Ehrig, H., Engels, G., Kreowski, H-J., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformations, Vol. 2, Applications, Languages, and Tools, pp. 479–546. World Scientific (1997)
[68] Van de Pol, J.: Just-in-time: on strategy annotations. In: Proceedings of WRS 2001, 1st International Workshop on Reduction Strategies in Rewriting and Programming, vol. 57, Elecronic Notes in Theoretical Computer Science, pp. 41–63 (2001) · Zbl 1268.68104 · doi:10.1016/S1571-0661(04)00267-1
[69] van Oostrom, V., de Vrijer, R.: Term Rewriting Systems, vol. 2, Cambridge Tracts in Theoretical Computer Science, chapter 9: Strategies. Cambridge University Press (2003)
[70] Visser, E.: Stratego: a language for program transformation based on rewriting strategies system description of stratego 0.5. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001) · Zbl 0981.68679 · doi:10.1007/3-540-45127-7_27
[71] Visser, E.: A survey of strategies in rule-based program transformation systems. J. Symbolic Comput. 40(1), 831–873 (2005) · Zbl 1129.68043 · doi:10.1016/j.jsc.2004.12.011
[72] Walukiewicz, L.: A landscape with games in the background. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 356–366 (2004) · doi:10.1109/LICS.2004.1319630
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.