Document Open Access Logo

A faithful encoding of programmable strategies into term rewriting systems

Authors Horatiu Cirstea, Serguei Lenglet, Pierre-Etienne Moreau

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.74.pdf
  • Filesize: 0.56 MB
  • 15 pages

Document Identifiers

Author Details

Horatiu Cirstea
Serguei Lenglet
Pierre-Etienne Moreau

Cite AsGet BibTex

Horatiu Cirstea, Serguei Lenglet, and Pierre-Etienne Moreau. A faithful encoding of programmable strategies into term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 74-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.74

Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AAProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for Tom and performances comparable to the native Tom strategies have been observed.
Keywords
  • Programmable strategies
  • termination
  • term rewriting systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Beatriz Alarcón, Raúl Gutiérrez, and Salvador Lucas. Context-sensitive dependency pairs. Inf. Comput., 208(8):922-968, 2010. Google Scholar
  2. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1-2):133-178, 2000. Google Scholar
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  4. Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and Antoine Reilles. Tom: Piggybacking rewriting on java. In RTA'07, volume 4533 of LNCS, pages 36-47. Springer-Verlag, 2007. Google Scholar
  5. Emilie Balland, Pierre-Etienne Moreau, and Antoine Reilles. Effective strategic programming for Java developers. Software: Practice and Experience, 44(2):129-162, 2012. Google Scholar
  6. P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An overview of ELAN. In WRLA'98, volume 15. ENTCS, 1998. Google Scholar
  7. Horatiu Cirstea, Claude Kirchner, Radu Kopetz, and Pierre-Etienne Moreau. Anti-patterns for rule-based languages. Journal of Symbolic Computation, 45(5):523-550, 2010. Symbolic Computation in Software Science. Google Scholar
  8. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. The Maude 2.0 System. In RTA'03, volume 2706 of LNCS, pages 76-87. Springer-Verlag, 2003. Google Scholar
  9. Jörg Endrullis and Dimitri Hendriks. From outermost to context-sensitive rewriting. In RTA'09, volume 5595 of LNCS, pages 305-319. Springer, 2009. Google Scholar
  10. Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In ICFP'01, pages 26-37. ACM Press, 2001. Google Scholar
  11. Olivier Fissore, Isabelle Gnaedig, and Hélène Kirchner. Simplification and termination of strategies in rule-based languages. In PPDP'03, pages 124-135. ACM, 2003. Google Scholar
  12. Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, and Stephan Swiderski. Proving termination by dependency pairs and inductive theorem proving. Journal of Automated Reasoning, 47(2):133-160, 2011. Google Scholar
  13. Jürgen Giesl and Aart Middeldorp. Innermost termination of context-sensitive rewriting. In DLT'02, volume 2450 of LNCS, pages 231-244. Springer, 2002. Google Scholar
  14. Jürgen Giesl and Aart Middeldorp. Transformation techniques for context-sensitive rewrite systems. J. Funct. Program., 14(4):379-427, 2004. Google Scholar
  15. Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann. Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst., 33(2):7, 2011. Google Scholar
  16. Jürgen Giesl, René Thiemann, and Stephan Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37:2006, 2006. Google Scholar
  17. Isabelle Gnaedig and Hélène Kirchner. Termination of rewriting under strategies. ACM Trans. Comput. Log., 10(2), 2009. Google Scholar
  18. Albert Gräf. Left-to-right tree pattern matching. In RTA'91, volume 488 of LNCS, pages 323-334. Springer-Verlag, April 1991. Google Scholar
  19. Nao Hirokawa and Aart Middeldorp. Automating the dependency pair method. Information and Computation, 199(1-2):172-199, 2005. Google Scholar
  20. J.-P. Jouannaud and Claude Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257-321. The MIT press, 1991. Google Scholar
  21. Markus Kaiser and Ralf Lämmel. An Isabelle/HOL-based model of stratego-like traversal strategies. In PPDP'09, pages 93-104. ACM, 2009. Google Scholar
  22. Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In RTA'09, volume 5595 of LNCS, pages 295-304. Springer-Verlag, 2009. Google Scholar
  23. Ralf Lämmel, Simon J. Thompson, and Markus Kaiser. Programming errors in traversal programs over structured data. Sci. Comput. Program., 78(10):1770-1808, 2013. Google Scholar
  24. José Meseguer and Christiano Braga. Modular rewriting semantics of programming languages. In Algebraic Methodology and Software Technology, volume 3116 of LNCS, pages 364-378. Springer Berlin Heidelberg, 2004. Google Scholar
  25. Pierre-Etienne Moreau, Christophe Ringeissen, and Marian Vittek. A Pattern Matching Compiler for Multiple Target Languages. In CC'03, volume 2622 of LNCS, pages 61-76. Springer-Verlag, 2003. Google Scholar
  26. Matthias Raffelsieper and Hans Zantema. A transformational approach to prove outermost termination automatically. ENTCS, 237:3-21, 2009. Google Scholar
  27. Terese. Term Rewriting Systems. Cambridge University Press, 2003. M. Bezem, J. W. Klop and R. de Vrijer, eds. Google Scholar
  28. René Thiemann. From outermost termination to innermost termination. In SOFSEM'09, volume 5404 of LNCS, pages 533-545. Springer, 2009. Google Scholar
  29. René Thiemann and Aart Middeldorp. Innermost termination of rewrite systems by labeling. ENTCS, 204:3-19, 2008. Google Scholar
  30. Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. System description of Stratego 0.5. In RTA'01, volume 2051 of LNCS, pages 357-361. Springer-Verlag, 2001. Google Scholar
  31. Eelco Visser, Zine-el-Abidine Benaissa, and Andrew Tolmach. Building program optimizers with rewriting strategies. In ICFP'98, pages 13-26. ACM Press, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact