Sciweavers

Share
RTA
2015
Springer

A faithful encoding of programmable strategies into term rewriting systems

3 years 6 months ago
A faithful encoding of programmable strategies into term rewriting systems
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 AProVE and TTT2...
Horatiu Cirstea, Sergueï Lenglet, Pierre-Etie
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where RTA
Authors Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau
Comments (0)
books