A Compiler for Rewrite Programs in Associative-Commutative Theories

Pierre-Etienne Moreau 1 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 : We address the problem of term normalisation modulo Associative-Commutative (AC) theories, and describe several techniques for compiling many-to-one AC matching and reduced term construction. The proposed matching method is based on the construction of compact bipartite graphs, and is designed for working very efficiently on specific classes of AC patterns. We show how to refine this algorithm to work in an eager way. General patterns are handled through a program transformation process. Variable instantiation resulting from the matching phase and construction of the resulting term are also addressed. %To improve efficiency of %term normalisation modulo \AC, we propose a few solutions %to share parts of terms thanks to a suitable term representation, %or to avoid useless constructions in matching. Our experimental results with the system ELAN provide strong evidence that compilation of many-to-one AC normalisation using the combination of these few techniques is crucial for improving the performance of algebraic programming languages.
Type de document :
Communication dans un congrès
ALP/PLILP: Principles of Declarative Programming, 1998, Pisa, Italy, 1490, pp.230-249, 1998, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098451
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:01:37
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098451, version 1

Collections

Citation

Pierre-Etienne Moreau, Hélène Kirchner. A Compiler for Rewrite Programs in Associative-Commutative Theories. ALP/PLILP: Principles of Declarative Programming, 1998, Pisa, Italy, 1490, pp.230-249, 1998, Lecture Notes in Computer Science. 〈inria-00098451〉

Partager

Métriques

Consultations de la notice

127