A faithful encoding of programmable strategies into term rewriting systems

Horatiu Cirstea 1 Sergueï Lenglet 1 Pierre-Etienne Moreau 1
1 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 AProVE 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. 1998 ACM Subject Classification F.4 Mathematical Logic and Formal Languages
Type de document :
Communication dans un congrès
Rewriting Techniques and Application 2015, Jun 2015, Warsaw, Poland. pp.15, 〈10.4230/LIPIcs.RTA.2015.74〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01168956
Contributeur : Sergueï Lenglet <>
Soumis le : vendredi 26 juin 2015 - 17:23:46
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
Document(s) archivé(s) le : vendredi 9 octobre 2015 - 19:00:21

Fichier

10.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau. A faithful encoding of programmable strategies into term rewriting systems. Rewriting Techniques and Application 2015, Jun 2015, Warsaw, Poland. pp.15, 〈10.4230/LIPIcs.RTA.2015.74〉. 〈hal-01168956〉

Partager

Métriques

Consultations de la notice

264

Téléchargements de fichiers

46