Term Rewriting

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 : This chapter introduces term rewriting and some of its applications from different points of view. Rewriting is first presented as an abstract relation on a set, and properties of such relations, mainly confluence and well-foundedness, are introduced. A more concrete notion of rewriting is then defined on first-order terms. Several examples of rewriting relations on terms or equivalence classes of terms are given, including rewriting modulo axioms and conditional rewriting. The rewriting logic is defined and is shown to be especially suited to describing concurrent computations. It also provides a logical framework in which other logics can be represented, and a semantic framework for the specification of languages and systems. The rest of the chapter is concerned with applications of rewriting to proofs of various program properties. It first addresses the issue of automatically building, for an equational theory, an equivalent convergent rewrite system, when one exists. This is solved via a completion process that turns equalities into rewrite rules, computes new derived equalities and reduces them. Several generalisations of this completion mechanism, based on superposition and simplification, are also surveyed. Then the completion technique is generalised in the context of order-sorted equational specifications. There, rewriting is used not only to evaluate but also to compute the types of terms during evaluation. Eventually, in the context of many-sorted conditional specifications, rewrite techniques are used to prove inductive properties in the initial model and completeness of function definitions.
Type de document :
Chapitre d'ouvrage
Astesiano, E. & Kreowski, H.J. & Krieg-Brückner, B. Algebraic Foundations of Systems Specifications, Springer, pp.273--320, 1999, IFIP State-of-the-Art Reports
Liste complète des métadonnées

https://hal.inria.fr/inria-00098978
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:40:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098978, version 1

Collections

Citation

Hélène Kirchner. Term Rewriting. Astesiano, E. & Kreowski, H.J. & Krieg-Brückner, B. Algebraic Foundations of Systems Specifications, Springer, pp.273--320, 1999, IFIP State-of-the-Art Reports. 〈inria-00098978〉

Partager

Métriques

Consultations de la notice

53