AirCube: Rewrite Rule Research
Motivation and history of the cooperation
The Generic Language
Technology group at CWI in
Amsterdam and the
Protheo team at
LORIA and
INRIA Lorraine in Nancy have an
active cooperation since several years. It is based on a close
relationship of the scientific interests of both groups and on
the common goal to make rewriting concepts and tools widely
available for program logic, semantics, and (program) transformation.
ASF+SDF formalism and the
ASF+SDF
Meta-Environment are projects of the
GLT group, these
projects started in 1985 and they have two complementary
goals.
The first one was the development of a formalism to describe
the syntax and semantics of a (programming) language. This has
resulted in the ASF+SDF formalism. SDF (Syntax Definition
Formalism) allows the definition of the syntactical aspects of
a language. It uses the latest parsing technologies in order
to write down syntax definitions and it provides a parser
generator and a scannerless generalized LR parser. ASF
(Algebraic Specification Formalism), allows the equational
definition of semantics in user-defined syntax. An efficient
compiler has been developed to execute ASF specifications. The
application area of ASF+SDF is targeted to language
prototyping, domain specific languages, and software
renovation. The second goal was the development of an
integrated interactive environment to develop and test
ASF+SDF specifications, this environment offers
syntax-directed editing facilities, an interpreter, compiler,
parser generator, parser, pretty printer, and debugger.
The Protheo project
in Nancy develops concepts, methods, and tools using rewriting
as the main computation and deduction paradigms. In this context,
we developed ELAN as a
language and environment allowing to express and execute
strategy guided rewrite systems. The semantical foundation of
the systems rely on the rewriting calculus
and the compilation
techniques developed for the language allows us to deal
efficiently with associative-commutative symbols as well as with
non-determinism. The application area of ELAN concerns more
specifically safe program development and encompass constraint
solving, theorem proving, and model checking.
The two teams share a strong core of common knowledge
and knowhow in the field of rewriting and their collaboration
benefits from complementary point of views on concepts,
implementation, applications, and potential transfers.
This common culture and common view on the general goals, together
with the opportunity to share knowledge and developments lead us to
initiate a collaboration starting with the organization of two
workshops followed by several visits.
The ideas were ripping the last two years and the last workshop in Volkrange
enlightens the strong common interest of the two groups to collaborate
on the design and implementation of reusable modules for rewriting,
controlling and analyzing. Since such development is quite involving
both at the conceptual level and technical development level, there is
a strong common commitment in pursuing and further developing the
current cooperation. To this end we decided to increase our
partnership in at least two ways:
- by answering to the INRIA call for associated teams abroad,
- by a one year stay of Mark
van den Brand in Nancy starting in November 2001 as
"Spécialiste Adadémique Etranger" .
Work program
The main idea of the future developments of the ASF+SDF and ELAN
systems is quite simple: make these systems the result of the assembly
(a kind of "Lego") of basic independent and re-usable software
components. From work performed both at the conceptual level and the
implementation level over the last ten years, it appears that this is
now needed and indeed feasible.
It is needed because the rewriting concept and technology is used
implicitly or explicitly in many domains from theory to
applications. To provide re-usable tools is a real scientific and
technological challenge.
It is possible since the scientific knowledge and knowhow are now
available to reach the goal: let us mention in particular the
discovery and study of the rewriting logic (at SRI International),
rewriting calculus (at LORIA), and the design of really efficient
compilers for rewriting (both at CWI and LORIA).
Visits
- Mark van den Brand long term visit (1 year)
- Hubert Dubois visited the CWI for 3 days (june, 12-14)
- Paul Klint will visit the LORIA for a week (September)
- Jurgen Vinju will visit the LORIA for 3 months (September to
November 2002)
- Pieter Olivier will visit the LORIA for 1 week in Septembre 2002
Activities
From 2nd to 6th of February 2004, the third AirCube workshop will be
held in Val d'Ajol (Vosges, France).
The idea is to have a one-day workshop for the 2 teams to meet and the
other days will be used to work together in smaller groups on specific
topics.
A preliminary program is under construction.
From 30th of January until the 1st of February the first AirCube workshop
was held in Hotel De Oude Geul te Gulpen (The Netherlands). There were 10 presentations on
ongoing developments in both teams. The full program
is available together with the slides of each presentations.
The following topics were discussed in more detail:
- Architecture of the ...+SDF Meta-Environment.
- Common back-end for ASF compiler and ELAN compiler.
- Organization of future cooperation.
Discussion
Since January, an AirCube mailing list has been created in order to
make the discussions easier (aircube@loria.fr).
One of the most active topic is related to the design and the
implementation of the new ...+SDF Meta-Environment.
The main goal of this project is to make the ASF+SDF Meta-Environment
sufficiently generic to be able to parameterize it by the Specification
Formalism.
The Meta-Environmentat would become ...+SDF, where the
... could be instantiated by at least ASF and ELAN for example.
Implementation
In parallel to this project, a new ELAN+SDF environment is built. This
project has two main impacts:
- it helps the Generic Language Technology group, by replacing ASF
by ELAN, to understand what could be made more generic in the
ASF+SDF Meta-Environment.
- it helps the Protheo group, by using a new parsing technology,
to make the notion of rules and strategies more uniform in the ELAN
language.
Application
Transforming DLMF LaTeX to OMDoc
In the context of the Digital Library of Mathematical Functions (DLMF)
we are working on a project to transform LaTeX to OMDoc.
The DLMF is a project of the
National Institute of Standards and Technology of the USA
that aims to create a standard reference for special mathematical functions
both in book form and in various interactive presentations.
OMDoc
is an emerging standard format for mathematical texts based on XML,
in particular on the XML based standards
MathML and
OpenMath.
Among its aims is not only the rendering of the mathematical texts,
but also a representation with well-defined semantics
to facilitate interchange with computer algebra and proof systems.
However, OMDoc is not suitable as an input format for humans.
LaTeX is the format that most mathematicians use for writing
their articles and books, so it is natural to use it as an input format.
However, it is very much oriented towards typesetting and
its semantics is presentation rather than contents oriented.
In the DLMF project this is mitigated by a standard set of macros,
and it is conceivable to add semantical markup where needed,
for example to specify types.
The powerful parsing technology of SDF combined with rewriting in ELAN
promises to be suitable platform for this project.
In particular we plan to use island grammars to isolate
the mathematical content,
to investigate how to best divide the work between parsing and rewriting,
and to compare the expressiveness of ELAN with XSLT.
Results
A consequence of this cooperation is a strong synergy between the two
groups.
The Protheo group, for example, is now more familiar with the notion
of ATerms
(developped at CWI) and has begun to
develop several tools based on this formalisms.
An interesting point is that the Protheo group has improved the
implementation of the ATerm library and has implemented an extension
of the Java version of the ATerm library. This new extension is based
on the Rho-calculus and is now used in the group to support the
theoretical research.
Similarly, the Generic Language Technology group has adopted several
tools and ideas developped at Loria to support their research.
For example, the TOM
compiler has been used as a back-end for JJForester.
Another interesting point is the influence of the Protheo group on the
ASF+SDF developpment. Since January, the notion of builtins and
libraries have been introduced in the ASF+SDF Meta-Environment.
The different signs clearly show the beginning of a true deep
cooperation and the unification of different concepts.
Furthermore, the first academic results are promising:
- a completely new ELAN system has been built and will be released
soon (by the end of July).
- the ELAN+SDF system has been presented at LDTA'2002.
- a new implementation of the garbage collector of the ATerm
library has been integrated in the CWI CVS repository
- the Java implementation of the ATerm library and its extension
to RTerm are available
Members
Pierre-Etienne Moreau
Last modified: Thu Dec 6 10:43:20 CET 2001