Compact Normalisation Trace via Lazy Rewriting

Quang-Huy Nguyen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Innermost strategy is usually used in compiling term rewriting systems (TRSs) because it allows to build efficiently the result term in a bottom-up fashion. However, the innermost strategy does not always give the shortest normalising derivation. In many cases, using an appropriate laziness annotation on the arguments of the function symbols, we evaluate the lazy arguments only if it is necessary and hence, get a shorter derivation to the normal form while avoiding the non-terminating reductions. We provide in this work a transformation of the annotated TRSs, that allows to compute the normal form using an innermost strategy and to extract a lazy derivation in the original TRS from the normalising derivation in the transformed TRS. We apply our result to improve the efficiency of equational reasoning in the {\Coq} proof assistant using {\ELAN} as an external rewriting engine.
Type de document :
Communication dans un congrès
Servicio de Publicaciones - Universidad Politécnica de Valencia. 1st International Workshop on Reduction Strategies in Rewriting and Programming - WRS'2001, 2001, Utrecht, Pays-Bas, 2359, pp.79-96, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00107874
Contributeur : Publications Loria <>
Soumis le : mercredi 17 janvier 2007 - 10:25:17
Dernière modification le : samedi 26 mai 2018 - 01:17:53
Document(s) archivé(s) le : mardi 6 avril 2010 - 18:21:24

Identifiants

  • HAL Id : inria-00107874, version 1

Citation

Quang-Huy Nguyen. Compact Normalisation Trace via Lazy Rewriting. Servicio de Publicaciones - Universidad Politécnica de Valencia. 1st International Workshop on Reduction Strategies in Rewriting and Programming - WRS'2001, 2001, Utrecht, Pays-Bas, 2359, pp.79-96, 2001. 〈inria-00107874〉

Partager

Métriques

Consultations de la notice

153

Téléchargements de fichiers

881