Term Rewriting with Type-safe Traversal Functions

Mark G. J. Van den Brand 1 Paul Klint J.J. Vinju
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Term rewriting is an appealing technique for performing program analysis and program transformation. Tree (term) traversal is frequently used but is not supported by standard term rewriting. In this paper, many-sorted first-order term rewriting is extended with automatic tree traversal by adding two primitive tree traversal strategies and complementing them with three types of traversals. These so-called traversal functions can be either top-down or bottom-up. They can be sort preserving, mapping to a single sort, or a combination of these two. Traversal functiona have a simple design, their application is type-safe in a first-order many-sorted setting and can be implemented efficiently. We describe the operational semantics of traversal functions and discuss applications.
keyword : term rewriting réécriture de limite
Type de document :
Communication dans un congrès
2nd International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2002, Jul 2002, Copenhagen, Denmark, 18 p, 2002
Liste complète des métadonnées
https://hal.inria.fr/inria-00101030
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:53:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00101030, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Mark G. J. Van den Brand, Paul Klint, J.J. Vinju. Term Rewriting with Type-safe Traversal Functions. 2nd International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2002, Jul 2002, Copenhagen, Denmark, 18 p, 2002. 〈inria-00101030〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

105

Contact


archive-ouverte@inria.fr