Simplification and Termination of Strategies in Rule-Based Languages

Olivier Fissore 1 Isabelle Gnaedig 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient criterion for ELAN-like strategies to terminate, only lying on rewrite rules involved in the strategy. We then give a simplification process of strategies, itself described by rewriting, to empower the previous criterion. This simplification can also make proofs of other program properties easier.
Type de document :
Communication dans un congrès
Proceedings of the Fifth International Conference on Principles and Practice of Declarative Programming - PPDP'2003, Aug 2003, Uppsala, Sweden, pp.124-135, 2003
Liste complète des métadonnées

https://hal.inria.fr/inria-00099655
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:39:49
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099655, version 1

Collections

Citation

Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner. Simplification and Termination of Strategies in Rule-Based Languages. Proceedings of the Fifth International Conference on Principles and Practice of Declarative Programming - PPDP'2003, Aug 2003, Uppsala, Sweden, pp.124-135, 2003. 〈inria-00099655〉

Partager

Métriques

Consultations de la notice

86