Skip to main content
SpringerLink
Log in
Book cover

Logic, Rewriting, and Concurrency pp 380–403Cite as

Rewriting Strategies and Strategic Rewrite Programs

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See http://www.logic.at/strategies.

  2. 2.

    http://users.dsic.upv.es/~wrs/.

  3. 3.

    See http://www.strategicreasoning.net/.

  4. 4.

    http://wrla2012.lcc.uma.es/.

  5. 5.

    http://rho.loria.fr/index.html.

  6. 6.

    http://elan.loria.fr/elan.html.

  7. 7.

    https://gforge.inria.fr/projects/tom/.

  8. 8.

    http://strategoxt.org/Stratego/WebHome.

  9. 9.

    http://maude.cs.uiuc.edu/.

  10. 10.

    http://tulip.labri.fr/TulipDrupal/?q=porgy.

  11. 11.

    Remark due to an external referee.

References

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  4. Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  5. Antoy, S., Middeldorp, A.: A sequential reduction strategy. Theor. Comput. Sci. 165(1), 75–95 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  8. Balland, E., Moreau, P.-E., Reilles, A.: Effective strategic programming for java developers. Softw. Pract. Exp. 44(2), 129–162 (2012)

    Article  Google Scholar 

  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)

    Google Scholar 

  10. Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  15. Castro, C.: Building constraint satisfaction problem solvers using rewrite rules and strategies. Fundamenta Informaticae 34(3), 263–293 (1998)

    MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  17. Cirstea, H., Kirchner, C.: The rewriting calculus - Part I and II. Logic J. Interest Gr. Pure Appl. Logics 9(3), 427–498 (2001)

    MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  21. Dijkstra, E.W.: Selected Writings on Computing - A Personal Perspective. Texts and Monographs in Computer Science. Springer, New York (1982)

    Book  MATH  Google Scholar 

  22. Dougherty, D.J.: Rewriting strategies and game strategies. Internal report, August 2008

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  30. Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Trans. Comput. Logic 10(2), 1–52 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

  34. Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comput. Sci. 11(5), 637–688 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  36. Hanus, M.: Curry: a multi-paradigm declarative language (system description). In: Twelfth Workshop Logic Programming (WLP 1997), Munich (1997)

    Google Scholar 

  37. Huet, G., Lévy, J.-J.: Computations in non-ambiguous linear term rewriting systems. Technical report, INRIA Laboria (1979)

    Google Scholar 

  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)

    Google Scholar 

  39. Jones, S.L.P.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  40. Kechri, A.S.: Classical Descriptive Set Theory. Graduate Texts in Mathematics, vol. 156. Springer, New York (1995)

    Book  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  43. Kirchner, C., Kirchner, H., Vittek, M.: Implementing computational systems with constraints. In: Principles and Practice of Constraint Programming, pp. 156–165 (1993)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  46. Letichevsky, A.: Development of rewriting strategies. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714. Springer, Heidelberg (1993)

    Google Scholar 

  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)

    Google Scholar 

  48. Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Func. Logic Program. 1, 1–61 (1998)

    MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  51. Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446–453 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  55. Martí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electron. Notes Theor. Comput. Sci. 238(3), 227–247 (2008)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  57. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  58. Nickel, U., Niere, J., Zündorf, A.: The FUJABA environment. In: ICSE, pp. 742–745 (2000)

    Google Scholar 

  59. O’Donnell, M.J. (ed.): Computing in Systems Described by Equations. LNCS. Springer, Heidelberg (1977)

    MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  62. Plasmeijer, M.J., van Eekelen, M.C.J.D.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Boston (1993)

    MATH  Google Scholar 

  63. Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)

    MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  71. Visser, E.: A survey of strategies in rule-based program transformation systems. J. Symbolic Comput. 40(1), 831–873 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

Download references

Acknowledgements

The results presented here are based on pioneer work in the Elan language designed in the Protheo team from 1990 to 2002. They rely on joint work with many people, in particular Marian Vittek and Peter Borovanský, Claude Kirchner and Florent Kirchner, Dan Dougherty, Horatiu Cirstea and Tony Bourdier, Oana Andrei, Maribel Fernandez and Olivier Namet. I am grateful to the members of the Protheo and the Porgy teams, for many inspiring discussions on the topics of this paper. I sincerely thank the reviewers for their careful reading and pertinent and constructive remarks. A special tribute is given to José Meseguer, for his inspiring works on rewriting logic and strategies, and this paper is dedicated to him.

Author information

Authors and Affiliations

  1. Inria, Domaine de Voluceau, BP 105, 78153, Rocquencourt, Le Chesnay Cedex, France

    Hélene Kirchner

Authors
  1. Hélene Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hélene Kirchner .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Kirchner, H. (2015). Rewriting Strategies and Strategic Rewrite Programs. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation