Software developped in the PROTHEO group

Tom

Since 2002, we have developed a new system called Tom. This system consists in a pattern matching compiler which is particularly well-suited for programming various transformations on trees/terms and XML documents. Its design follows our experiences on the efficient compilation of rule-based systems. The main originality of this system is to be language and data-structure independent. This means that the Tom technology can be used in a C, C++ or Java environment. The tool can be seen as a Yacc-like compiler translating patterns into executable pattern matching automata. Similarly to Yacc, when a match is found, the corresponding semantic action (a sequence of instructions written in the choosen underlying language) is triggered and executed.

Tom supports sophisticated matching theories such as associative matching modulo neutral element (also known as list-matching). This kind of matching theory is particularly well suited to perform list or XML based transformations for example. The main idea consists in encoding a DOM object into a term-based representation (a DOM NodeList becomes an associative list-operator), and then perform matching and subterm retrieving using the Tom pattern matching facilities. On one side, this approach is not comparable to XSLT. But, on the other side, the expressivity is very high since it is possible to combine powerful pattern matching constructs with the expressive power of Java.

Tom is documented, maintained and available on the Web. More resources can be found on the Tom Gforge project page and the Tom bug tracker.

ATerm-java and SharedObjects

ATerm-java and SharedObjects are two libraries written in Java. They offer a very efficient implementation for terms, both in time and space. Based on a maximal-sharing approach, terms can be compared in constant time. The libraries also provide several input-output facilities.

These two libraries are included in the Tom release.

Gom

Gom is a generator of typed data-structures. Based on the ATerm-java and the SharedObjects libraries, the generated code offers maximal-sharing and is efficient. Gom makes possible the definition of normalization functions. This is very useful to maintain terms in canonical forms. Predefined functions exist for computing normal forms of terms modulo associative, commutative theories, with neutral element.

Gom can be easily interfaced with Tom, and is available in the release of Tom.

CoLoR

CoLor is a Coq library whose aim is to provide the necessary formal basis for certifying the termination proof candidates searched and built by tools like CiME, AProVE, TTT, CARIBOO, etc. Among other things, it includes a library on vectors, a library on integer polynomials with multiple variables, a library on algebraic terms with symbols of fixed arity, a proof of the termination criterion based on polynomial interpretations, and a proof of the dependancy pairs theorem. The library is likely to evolve and include more developments quickly. For more recent informations, see the CoLoR web page.

Rainbow

Rainbow provides a grammar for termination proofs and a tool for automatically certifying the proofs expressed in this grammar by using the CoLoR library.

ELAN

The ELAN system provides an environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. It offers a natural and simple logical framework for the combination of the computation and deduction paradigms as it is backed up by the concepts of rewriting calculus and rewriting logic. It permits to support the design of theorem provers, logic programming languages, constraint solvers and decision procedures and to offer a modular framework for studying their combination.

ELAN takes from functional programming the concept of abstract data types and the function evaluation principle based on rewriting. But rewriting is inherently non-deterministic since several rules can be applied at different positions in a same term, and in ELAN, a computation may have several results. This aspect is taken into account through choice operations and a backtracking capability. One of the main originality of the language is to provide strategy constructors to specify whether a function call returns several, at-least one or only one result. This declarative handling of non-determinism is part of a strategy language allowing the programmer to specify the control on rules application. This is in contrast to many existing rewriting-based languages where the term reduction strategy is hard-wired and not accessible to the designer of an application.

The strategy language offers primitives for sequential composition, iteration, deterministic and non-deterministic choices of elementary strategies that are labelled rules. From these primitives, more complex strategies can be expressed. In addition the user can introduce new strategy operators and define them by rewrite rules. Evaluation of strategy application is itself based on rewriting. So the simple and well-known paradigm of rewriting provides both the logical framework in which deduction systems can be expressed and combined, and the evaluation mechanism of the language.

ELAN is documented, maintained and available on the Web.

Other software