ERCIM News No.36 - January 1999
ERCIM News No.36 - January 1999
Programming with Rewrite Rules and Strategies
by Hélène Kirchner
ELAN is a language to express non-deterministic computations via rewrite rules and strategies. Strategies are the part of the program that specifies the way rule application is to be controlled. Compilation techniques are studied in this context for an efficient execution of these programs. ELAN is developed in the PROTHEO project common to CNRS, INRIA and Universities of Nancy.
Rules are present in many domains of Computer Science: let us mention for instance production rules, inference rules, grammar rules, transition rules, constraint simplification rules, program transformation rules, to cite a few. All of them are actually rewrite rules, ie schemas allowing to transform expressions. A set of rewrite rules is a program (or a theory) in rewriting logic. To execute such a program with a given query (the expression to rewrite), at each step one has to choose the rule to apply and the position in the expression where the rule is to be applied. This choice may be complex, even in a case that may look simple of simplification of arithmetic expressions.
Due to this inherent non-determinism, controlling rewrite rule application is an important issue for all kinds of rules. Control is expressed as search plans in theorem provers; action plans in scheduling; tactics or tacticals in logical frameworks; lazy evaluation in functional programming; or via constructs like cut in logic programming. In most programming languages the evaluation strategy is fixed, which avoids non-determinism, so that the evaluation process is then easier to implement. The counterpart of this option is that programs are dependent on this built-in evaluation strategy. Any control deviating from this has to be encoded via data or program structures.
The approach followed in the ELAN project is different. Programs are composed of rewrite rules and strategies whose purpose is to guide choices in non-deterministic situations, to select rules to be applied, or to cut useless branches in the computation tree. Strategies are terms with higher-order types that are applied to first-order terms.
Since rewriting is inherently non-deterministic, in ELAN, a computation may have several results. This aspect is taken into account by a backtracking capability, and choice strategy constructors (don’t know, don’t care, don’t care one) that allow specifying whether a strategy call returns several, at-least one, or only one result. Strategies can be sequentially composed and iterated. Elementary strategies are labelled rules. From them and the strategy constructors, more complex strategies can be expressed. In addition, the programmer can declare new strategy operators, define them by rewrite rules, and design rules to simplify strategy expressions.
The current version of ELAN includes an interpreter and a compiler written in C++ and JAVA. Both can interact via an exchange format (REF, for Reduced ELAN Format) which is a term representation of ELAN programs. This format appears to be a convenient way for to transform ELAN programs making use of ELAN itself, and is the key for the implementation of a reflection mechanism in ELAN.
Initially, the system was designed for specifying and prototyping theorem provers, constraint solvers and decision procedures, and for studying their combination. For instance COLETTE is a solver for constraint satisfaction problems designed in ELAN, where propagation and consistency techniques can be experimented with flexible definitions of strategies.
To deal with such applications, efficiency is crucial and motivates the development of the ELAN compiler. Compilation techniques for non-deterministic rewrite programs with strategies are based on efficient data structures such as matching automata and compact bipartite graphs, but also on a careful memory and backtracking management. For implementation of backtracking, two functions are usually required: the first one, to create a choice point and save the execution environment; the second one, to backtrack to the last created choice point and restore the saved environment. These functions are implemented in assembly language and may be useful in other contexts, for instance to implement backtracking in imperative languages.
A determinism analysis is performed in the ELAN compiler, where every rule and strategy in the program is annotated with its determinism mode which classifies the strategies according to the number of their expected results. In case of deterministic strategies with 0 or 1 result for instance, many choice points are dropped at run time. This approach considerably reduces the search space size, the memory usage, the number of necessary choice points, and the time spent in backtracking and memory management. The determinism analysis simply makes possible to run programs that could not be executed without it due to memory explosion. This was the case in particular for constraint satisfaction problems. In other examples, this analysis significantly decreased the number of set choice points and improved the performance. The ELAN compiler can handle large specifications (thousands of rules and strategies), long computations (more than 20.10^9 applied rules), and can apply on some examples up to 17.10^6 rewrite steps per second.
The simple rewriting paradigm that is implemented in ELAN as the evaluation mechanism of the language actually provides a logical framework in which deduction systems can be expressed and combined. Rewriting logic is a natural semantic framework for concurrency and parallel programming, and for the specification of systems and languages. It has also good properties as a logical framework for representing logics. A growing number of research efforts exploring the application of rewriting logic in all these directions are being carried out worldwide, and several languages based on rewriting logic are being designed and implemented. ELAN is one of them and can be compared to other systems such as ASF+SDF (CWI, The Netherlands), Maude (SRI, California) or Cafe-OBJ (JAIST, Japan). The originality of ELAN with respect to these other languages is to provide non-deterministic computations and to have initiated the implementation of strategies.
Perspectives for the ELAN project include improvement of the overall design of the system, the study of reflection properties of the framework, and the design of proof editing and debugging tools.
For more information on the ELAN system, see http://www.loria.fr/ELAN/Please Contact:
Hélène Kirchner - LORIA
Tel: +33 3 83 59 30 12
E-mail: Helene.Kirchner@loria.fr