Frequently Asked Questions
- Can ELAN run under LINUX?
ELAN runs under Linux on PC machines. Look at
How to get ELAN
- Can ELAN run on Windows9* or NT?
Not yet fully. We have already a first port of the interpreter to NT,
but we do not distribute it currently. If you are interested in getting a
preliminary NT version or in contributing to porting it, do not hesitate to
contact us (email@example.com).
- Is ELAN devoted to prototyping constraint solvers?
We made many implementations of constraint solvers using ELAN, and the
use of the strategy languages is extremely useful to describe the behavior
of the solvers. But ELAN is by no mean devoted to this specific objects, and
many other applications have been programmed in the language, see .
- What is the relationship with CHR?
Constraint Handling Rules introduced by Thom Fruewirth is a language
devoted to the description of constraint manipulation rules, initialy designed
as an extention of the constraint logic programming system Eclipse. ELAN has
also been used to program constraint manipulations. Interests of ELAN over
CHR are the semantics of ELAN (either rewriting calculus or logic), the possibility
to use strategies (either deterministic or not), the possibility to use associative-commutative
operators, and that rewrite rules and strategies are compiled very efficiently.
One nice feature of CHR is to have constraints as a first class concept, which
is not currently the case in ELAN.
- Does ELAN need the term rewrite systems it implements
to be confluent and terminating?
In an ELAN program, the set of rules is splitted in two main parts: labelled
and unlabelled rules. The set of unlabelled rules is assumed to be confluent.
On the set of labelled rules no hypothesis is made and it is perfectly OK
to have for example the rule
In order to use labelled rules, ELAN require the user
to specify a strategy describing how they should be applied. The strategy
language is described in Strategies Specification.
- Is ELAN using backtracking?
Yes this is the fundamental mechanism used for implementing dk (don't
know) first and dc (don't care) strategies. It is implemented particularly
efficiently and documented in CPL
a Choice Point Library
- What is the relationship between ELAN and LCF,
specificaly, the way rewriting is defined and used in LCF?
A first important difference is that the underlying calculus of ELAN is
the rewriting calculus: i.e. rewriting plus strategies. In LCF, the primarily
calculus is the lambda calculus. The following excerpt from A Higher-Order
Implementation of Rewriting enlight the relationship between LCF and ELAN.
It situates also the general research direction on the rewriting calculus.
``LCF is used not only for performing particular
proofs, but also for research into proof techniques. The programming language
ML provides the flexibility needed for this research. The discovery of the
operators THEN, ORELSE, and REPEAT, for combining tactics, was a breakthrough
in the development of Edinburgh LCF. So it is exciting to find similar operators
for combining conversions, especially since tactics and conversions have
little else in common. This calls for an inquiry into instances of this
- What is the relationship between ELAN and MAUDE,
developped at SRI?
ELAN and MAUDE are both rule based languages that inherit in particular of
the OBJ language and experience. From the language point of view, the main
difference between the two languages is that ELAN as two first class concepts:
Rules and Strategies. In Maude the first class concept are Rules and strategies
are reached via the reflective capability of rewriting logic. From the system
point of view, the main difference is that MAUDE has a very efficient interpreter
as ELAN has an interpreter as well as a very efficient compiler. See this
page on related systems for more details.