CiME : Completion Modulo E
Introduction
Completion algorithms are used for computing canonical rewrite systems
for equational specifications. Completion modulo a theory E
allows to build-in some theories E, but until now the only
case seeming useful is when E is the associativity and
commutativity of some operators. One problem arising when using such a
technique with other E such ACU (AC+unit), ACI
(AC+idempotency), groups theory, etc.; is that rewriting on
E-congruence classes does not terminate in general. Another
problem is the unification process, which has to be done modulo
E. These difficulties have been solved by the use of a new
rewrite relation: E-normalised rewriting, and a corresponding
completion algorithm has been designed.
The background theory is explained in the LICS'94 article (extended
abstract) Normalised rewriting
and normalised completion and in the JSC article (full paper) Normalized
Rewriting: an alternative to Rewriting modulo a Set of
Equations.
CiME is developed in our research team DÉMONS, the main
author is Claude Marché,
with contributions of Evelyne
Contejean , Ralf
Treinen, Emmanuel Engel,
Florent Jacquemard, Hubert Comon.
The development of CiME is supported in part by
the EU project CCL, the HCM Network SOL, the HCM
Network CONSOLE, the « GDR de
programmation du CNRS », and a cooperation between the CNRS and the JNICT (project 4312).
Current state of development
The last release is CiME 1.15 alpha, dated September 30,
1997. It is an alpha version that have several known bugs, see
below. Several new things have been added since this version, and
there will be no CiME 1.15 version.
The next release will be numbered 2.0 and will include several
improvements including :
- Automatic generation of termination orderings, including weak
orderings for dependency pairs criteria.
- Fast reduction by compiling rewrite rules via discrimination nets.
- Check for completeness of definitions via automata techniques.
- An extended syntax, including an interactive top level.
Acknowledgments
CiME is written in Objective CAML, a functional
language of the ML family developed in the CRISTAL project at INRIA Rocquencourt.
CiME also uses the very fast AC-matching algorithm written by
Steven Eker from the PROTHEO project at
INRIA-Lorraine.
Last modification of this page: may 19, 1999
To DÉMONS home page