Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories
| Autor: | Hélène Kirchner, Pierre-Etienne Moreau |
|---|---|
| Přispěvatelé: | Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) |
| Rok vydání: | 2001 |
| Předmět: |
Theoretical computer science
Computer science [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences ac many-to-one matching Set (abstract data type) ac theories 0202 electrical engineering electronic engineering information engineering non-determinism filtrage many-to-one Functional programming système de réécriture Programming language non-déterminisme 020207 software engineering théories ac stratégies Term (logic) Data structure rewrite systems 010201 computation theory & mathematics Confluence compilation Compiler Rewriting computer Software Compile time |
| Zdroj: | Journal of Functional Programming Journal of Functional Programming, Cambridge University Press (CUP), 2001, 11 (3), pp.207-251 Journal of Functional Programming, 2001, 11 (3), pp.207-251 |
| ISSN: | 1469-7653 0956-7968 |
| DOI: | 10.1017/s0956796800003907 |
| Popis: | Article dans revue scientifique avec comité de lecture.; First-order languages based on rewrite rules share many features with functional languages. But one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming environments, compilation techniques for such languages based on rewriting have to be designed. This is the topic addressed in this paper. The proposed techniques are independent from the rewriting language and may be useful to build a compiler for any system using rewriting modulo associative and commutative (\AC) theories. An algorithm for many-to-one \AC\ matching is presented, that works efficiently for a restricted class of patterns. Other patterns are transformed to fit into this class. A refined data structure, namely compact bipartite graph, allows encoding all matching problems relative to a set of rewrite rules. A few optimisations concerning the construction of the substitution and of the reduced term are described. We also address the problem of non-determinism related to \AC\ rewriting and show how to handle it through the concept of strategies. We explain how an analysis of the determinism can be performed at compile time and we illustrate the benefits of this analysis for the performance of the compiled evaluation process. Then we briefly introduce the \ELAN\ system and its compiler, in order to give some experimental results and comparisons with other languages or rewrite engines. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|