Distributive rewriting calculus

Horatiu Cirstea 1 Clement Houtmann 1 Benjamin Wack 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The rewriting calculus has been introduced as a general formalism that uniformly integrates rewriting and lambda-calculus. In this calculus all the basic ingredients of rewriting such as rewrite rules, rule applications and results are first-class objects. The rewriting calculus has been originally designed and used for expressing the semantics of rule based as well as object oriented paradigms. We have previously shown that convergent term rewriting systems and classic strategies can be encoded naturally in the calculus. In this paper, we go a step further and we propose an extended version of the calculus that allows one to encode unrestricted term rewriting systems. This version of the calculus features a new evaluation rule describing the behavior of the result structures and a call-by-value evaluation strategy. We prove the confluence of the obtained calculus and the correctness and completeness of the proposed encoding.
Type de document :
Communication dans un congrès
Grit Denker and Carolyn L. Talcott. Sixth International Workshop on Reduction Strategies in Rewriting and Programming, Apr 2006, Vienna, Austria. Elsevier, 176(4), pp.95-111, 2007, Electronic Notes in Theoretical Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00110867
Contributeur : Horatiu Cirstea <>
Soumis le : jeudi 2 novembre 2006 - 10:52:35
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00110867, version 1

Collections

Citation

Horatiu Cirstea, Clement Houtmann, Benjamin Wack. Distributive rewriting calculus. Grit Denker and Carolyn L. Talcott. Sixth International Workshop on Reduction Strategies in Rewriting and Programming, Apr 2006, Vienna, Austria. Elsevier, 176(4), pp.95-111, 2007, Electronic Notes in Theoretical Computer Science. 〈inria-00110867〉

Partager

Métriques

Consultations de la notice

210