Compact Normalisation Trace via Lazy Rewriting
Identifieur interne : 002E65 ( Crin/Corpus ); précédent : 002E64; suivant : 002E66Compact Normalisation Trace via Lazy Rewriting
Auteurs : Quang-Huy NguyenSource :
English descriptors
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.
Links to Exploration step
CRIN:nguyen01aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="352">Compact Normalisation Trace via Lazy Rewriting</title></titleStmt><publicationStmt><idno type="RBID">CRIN:nguyen01a</idno><date when="2001" year="2001">2001</date><idno type="wicri:Area/Crin/Corpus">002E65</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Compact Normalisation Trace via Lazy Rewriting</title><author><name sortKey="Nguyen, Quang Huy" sort="Nguyen, Quang Huy" uniqKey="Nguyen Q" first="Quang-Huy" last="Nguyen">Quang-Huy Nguyen</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>innermost rewriting</term><term>lazy rewriting</term><term>normalisation trace</term><term>trs transformation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4154">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.</div></front></TEI><BibTex type="inproceedings"><ref>nguyen01a</ref><crinnumber>A01-R-139</crinnumber><category>3</category><equipe>PROTHEO</equipe><author><e>Nguyen, Quang-Huy</e></author><title>Compact Normalisation Trace via Lazy Rewriting</title><booktitle>{1st International Workshop on Reduction Strategies in Rewriting and Programming - WRS'2001, Utrecht, Pays-Bas}</booktitle><year>2001</year><editor>Servicio de Publicaciones - Universidad Politécnica de Valencia</editor><volume>2359</volume><pages>79-96</pages><month>May</month><organization>S. Lucas and B. Gramlich</organization><url>http://www.loria.fr/publications/2001/A01-R-139/A01-R-139.ps</url><keywords><e>lazy rewriting</e><e>innermost rewriting</e><e>normalisation trace</e><e>trs transformation</e></keywords><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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002E65 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 002E65 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:nguyen01a
|texte= Compact Normalisation Trace via Lazy Rewriting
}}
| This area was generated with Dilib version V0.6.33. |  |