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
