License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.74
URN: urn:nbn:de:0030-drops-51908
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5190/
Go to the corresponding LIPIcs Volume Portal

Cirstea, Horatiu ; Lenglet, Serguei ; Moreau, Pierre-Etienne

A faithful encoding of programmable strategies into term rewriting systems

pdf-format:
10.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{cirstea_et_al:LIPIcs:2015:5190,
  author =	{Horatiu Cirstea and Serguei Lenglet and Pierre-Etienne Moreau},
  title =	{{A faithful encoding of programmable strategies into term rewriting systems}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{74--88},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5190},
  URN =		{urn:nbn:de:0030-drops-51908},
  doi =		{10.4230/LIPIcs.RTA.2015.74},
  annote =	{Keywords: Programmable strategies, termination, term rewriting systems}
}

Keywords: Programmable strategies, termination, term rewriting systems
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI