Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems

Horatiu Cirstea 1 Sergueï Lenglet 2 Pierre-Etienne Moreau 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
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 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. We show that the encoding of strategies into term rewriting systems can be easily adapted to handle many-sorted signatures and we use a meta-level representation of terms to reduce the size of the encodings. 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; experiments in Tom show that applying our encoding leads to performances comparable to the native Tom strategies.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (4), pp.1-54. 〈10.23638/LMCS-13(4:16)2017〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01479030
Contributeur : Sergueï Lenglet <>
Soumis le : lundi 15 janvier 2018 - 15:30:26
Dernière modification le : mercredi 16 mai 2018 - 11:24:14
Document(s) archivé(s) le : lundi 7 mai 2018 - 06:37:40

Fichier

1705.08632v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Horatiu Cirstea, Sergueï Lenglet, Pierre-Etienne Moreau. Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (4), pp.1-54. 〈10.23638/LMCS-13(4:16)2017〉. 〈hal-01479030v2〉

Partager

Métriques

Consultations de la notice

293

Téléchargements de fichiers

25