Gadgets Manual

This manual presents the version V3.6 of the ELAN language and of its environment. This is mainly an update of version V3.4 with bug corrections with several new features offered by the compiler such that the Input/Output facilities, the new builtins (array, hashing tables) and the possibility to trace the normalisation process in ELAN programs. The ELAN compiler compiles now all possible patterns that contain AC symbols. No program transformation is required for the user. Furthermore, from this version we distribute the sources of the system. The compilation/installation process follows the same procedure as other GNU softwares.

What could you do in ELAN?
Relying on the premiss that inferences rules can be quite conveniently described by rewrite rules, we started in the early nineties to design and implement a language in which inference systems can be represented in a natural way, and executed reasonably efficiently. This leads us quickly to formalise such a language using the rewriting logic introduced by J. Meseguer [Mes92] and to see ELAN as a logical framework where the frame logic is rewriting logic extended with the fundamental notion of strategies [Vit94, KKV95, BKKM02]. A rewrite theory and an associated strategy is called a computational system.
In ELAN, a logic can be expressed by specifying its syntax, its inference rules and a description of how these rules should be applied. The syntax of the logic can be described using mixfix operators as in the OBJ language [GKK+87] or SDF [HHKR89]. The inference rules of the logic are described by conditional rewrite rules with where assignments allowing to introduce variables local to a rule.

From this description of the logic and a theory written in this logic, we infer automatically a computational system consisting of a rewriting theory plus strategies. Since we wanted ELAN to be modular, with a syntactic level well-adapted to the user’s needs, the language is designed in such a way that three programming levels are possible.
• First the design of a logic is done by the so-called super-user, with the help of a powerful preprocessor that expands specific macros into ELAN constructions.
• Such a logic can be used by the (standard) user in order to write a specification.
• Finally, the end-user can evaluate queries in the specification, following the semantics described by the logic.
This corresponds to the general diagram given in Figure 1.1. The query is interactively given by the end-user at the ELAN prompt level

Get pdf Elan v3.6 User Manual