--------------------------------------------------------------------------------
Minutes of the Second Workshop of the
IFIP WG-1.6 on Term Rewriting
University of East Anglia, Norwich, U.K.
July 9, 2000
--------------------------------------------------------------------------------
Agenda
1. Progress reports.
1.1. Declarative Debugging of Lazy Narrowing Computations,
Mario Rodríguez-Artalejo.
1.2. On Ordering Constraints,
Michaël Rusinowitch.
1.3. Progress reports on Maude and ELAN,
Maude: José Meseguer,
ELAN: Hélène Kirchner.
1.4. Efficient Implementation, Applications and Complexity of Rewriting,
Rakesh Verma.
2. Business session.
3. General discussion.
4. Rewriting and higher-order features.
4.1. The Rewrite Calculus as a Uniform View of Rewriting and Lambda-Calculus,
Claude Kirchner.
4.2. General discussion on that topic.
Chaired by Claude Kirchner.
Participants: Leo Bachmair, Corrado Böhm, Nachum Dershowitz, Richard Kennaway,
Claude Kirchner (WG Vice-Chair), Hélène Kirchner, José Meseguer, Aart
Middeldorp, Mario Rodríguez Artalejo, Michaël Rusinowitch, Yoshihito Toyama,
Femke van Raamsdonk (representing Jan Wilhem Klop) , Rakesh Verma (Invited),
Laurent Vigneron (WG Secretary), Uwe Waldmann (representing Harald Ganzinger).
Meeting opened at 9:00
Meeting closed at 18:00.
--------------------------------------------------------------------------------
1. Progress reports.
1.1. Declarative Debugging of Lazy Narrowing Computations,
Mario Rodríguez-Artalejo (Madrid).
Declarative debugging is used in logic programming and can be applied to
lazy functional (logic) programs.
Lazy narrowing calculus is used to formalize computations; a proof tree is
extracted (using formal methods) from the narrowing computations, and
simplified to get a computation tree.
This technique is used for detecting wrong answers in a set of declarative
conditional rewrite rules. This consists in checking the correctness of
the nodes of the tree w.r.t the intended model. A buggy node is a wrong
node with correct sons.
1.2. On Ordering Constraints,
Michaël Rusinowitch (Nancy).
The Recursive Path Ordering (RPO) is one of the most used ordering since it
gives simple syntactic conditions for orienting equations as rules. An
optimal way to apply RPO is to orient an equation u=v as u->v if for all
ground substitutions \theta, u\theta >{rpo} v\theta. When the precedence
is total this amounts to checking the unsatisfiability of the ordering
constraint v >{rpo} u or u ={rpo} v. Ordering constraints based on RPO
and its variants also allow us to express theorem-proving strategies such
as ordered resolution, ordered paramodulation and unfailing completion.
RPO constraint solving has been shown NP-complete for a total precedence
(joint work with P. Narendran and R. Verma). In the unary (and total) case
the whole first-order theory is decidable using tree automata techniques
(joint work with P. Narendran).
1.3. Progress reports on Maude and ELAN,
Maude: José Meseguer (Menlo Park),
ELAN: Hélène Kirchner (Nancy).
Maude (maude.csl.sri.com) is a system and language implementing rewriting
logic. This interpreter can be used as an execution specification
language, and a programming language. It is reflexive, and includes many
tools: an inductive theorem prover, a Church-Rosser checker, many
translators,...
It permits to associate an executable formal semantics in rewriting logic
to software architecture, object-oriented designs and distributed
components. It is used for giving a formal analysis of communication
systems.
Some extensions are considered: an extension supporting mobile
computations, a compiler, a theorem-proving environment.
ELAN (www.loria.fr/ELAN) is an environment for specifying and prototyping
deduction systems. The interpreter and the compiler permit to consider
non-deterministic calculi.
It uses ASF+SDF parsing tools for EFIX, an intermediate format for ELAN
based on A-terms, and a new parser generating EFIX.
ELAN is used for equational reasoning with CoQ: ELAN finds a computation,
and CoQ checks it. ELAN is also used in the CoFI working group for
executing CASL specifications.
Many tools have been realised in ELAN: a library for automata construction
and manipulation; a general framework of Constraint Logic Programming; a
predicate prover; a propositional sequent calculus; completion procedures
for rewrite systems; several examples of constraint solvers; a calculus of
explicit substitutions (the first-order rewrite system lambda-sigma that
mimics lambda-calculus), opening the way of implementing higher-order
logic programming languages via a first-order setting.
Current investigations are done on various enrichments of languages:
objects and constraints are added in objects and rules for the study of
production rules systems. The rewriting calculus rho-calculus provides a
promising framework for integrating lambda-calculus rewriting,
non-determinism and objects.
1.4. Efficient Implementation, Applications and Complexity of Rewriting,
Rakesh Verma (Houston).
LRR is a laboratory for rapid term rewriting. It is based on a term graph
interpreter and Smaran, a congruence-closure based system for equational
computations. It contains many optimisations: encoding of strings,
recursion, built-in data types, discrimination trees for matching,
congruence closure, dependency lists,...
About complexity, there are still many unknown results, even for ground
rewriting (e.g. confluence).
2. Business session.
* Shall we join the IFCoLog initiative?
The rewriting community has been contacted by the IFCoLog representatives,
in order to know if it will be willing to join the initiative. The question
has been redirected to the two current representative organisations of the
rewriting community: the RTA organizing committee that will rise the point
at the RTA2000 general assembly and to our IFIP working group.
The International Federation for Computational Logic (www.ifcolog.org),
whose President is Dana Scott, is an association that has the object to
advance and promote world-wide research and education in all areas of
computational logic.
The discussion about this association raises various points:
- it has to be a light structure for a better representation of the
community in the large.
- IFCoLog may not bring financial facilities, but this could be an
important "label" to add when asking subsidies.
- it will allow to bridge together the various aspects of computational
logic and to promote the ideas at the educational level as well as at the
political level.
The question about the existence of FLoC is raised. Is this conference
going to disappear in favor of a federated computational logic conference
that would hold every 4 or 5 years?
After discussions, all the present members of the WG are in favor to have
term rewriting represented in the IFCoLog initiative.
The question is raised of the best way to reflect this engagement from the
IFIP point of view. The question will be asked to the TC1 chairman, Giorgio
Ausiello.
* The point on many workshops concerned with rewriting.
This year, there are several workshops concerned with rewriting: 1st
Workshop on Rule-Based Constraint Reasoning and Programming (CL'2000), 2nd
Workshop on Rule-Based Constraint Reasoning and Programming (CP'2000),
Workshop on Rule-Based Programming (PLI'2000), Workshop on Rewriting Logic
and its Applications (WRLA'2000).
These 4 workshops are grouped in 6 months!
Do we need to have a coordination between these workshops?
The general opinion is that this rise of direct interest to rewriting is an
healthy indicator of the research activities around rewriting. 3 of these
workshops are organised as conferences adjacent workshops which is a nice
way to promote the ideas in related areas and this should be encouraged.
We have to try to avoid overlaps, and to find joint events (like RTA) where
these workshops can be from time to time (e.g. every 3 or 4 years) in
direct contact with the main core of the rewriting community.
This rises the point of the relationship between RTA and the other rewrite
concern events. The fact that several of these workshops have published
proceedings may explain the small number of submissions to RTA. In
addition, theoretical papers are currently predominant at RTA. The RTA
community should also think on how to attract people who use rewriting for
applications.
* Next meeting.
The next meeting of the WG will hold with RTA in Israel (May 21-24, 2001),
and there is a preference to have it after the conference.
* Actions to promote rewriting in the large.
Several suggestions are done.
- To elaborate material around the complementary needs to have gentle
introductory to the field and some handbook in rewriting. Three
possibilities: a paper book; a dynamic electronic book; tutorials.
- This is also very important to promote the existing tools related to
rewriting, explaining the role of each and the applications they can
handle. This list existing already in the Rewriting Home Page (RHP,
www.rewriting.org), we have to promote this page.
- Rewriting being a natural technique, an experience would be to take as
"clients" kids of 12 years old, and to define tools that would use
mouse oriented rewrite systems. The purpose is to make understand that
the arrow is powerful in many different ways.
- We also need pointers to courses on the RHP.
- If we really want to promote rewriting in the industry, we have to
consider that we need a different approach. This means that we need to
adapt to each kind of public.
This discussion leads to the proposition to have a group of persons
elaborating on the idea of an electronic book. Corrado Böhm, Claude
Kirchner, José Meseguer, Femke van Raamsdonk and Rakesh Verma will discuss
about its contents.
3. General discussion: Where is rewriting going?
Claude and Corrado presented respectively the opinions of David Plaisted and
Marisa Venturini Zilli. Some participants agree that most of the main
questions in the domain have been solved. Some on the contrary believe that
important questions are far to be solved. Points that are mentioned are to
improve the actual standards in complexity; to get new algorithmic results.
There are also many applications of rewriting, but no real breakthrough.
Though rewriting is a notion present in many areas, but it is not always a
research point by itself. Does it have to? Rewriting is a very simple
mechanism that subsumes many techniques. It is not known enough as a
translation tool. For attracting new researchers in our domain, we need to
apply rewriting in other domains, such as biological computing. This may be
achieved by defining a general tool for symbolic computing, hiding the
techniques behind, since term rewriting may be difficult to "sell" as it is.
In addition, rewriting has shown its usefulness as a programming paradigm
(cf. ASF+SDF, ELAN, Maude), but programming with rewrite rules has to be
learned and we need to define a methodology for rule-based specification and
programming.
Also, term rewriting is not taught enough. Why is it not explicitely in each
computer science curricula? There is no undergraduate book on term
rewriting. This would be easy to find mathematical examples illustrating its
main notions.
To sum up: Rewriting is an excellent model of computation as well as
programming paradigm: as stated by Corrado, "rewriting is the best way to
bridge the gap between syntax and semantics".
Important directions are:
- the extreme importance of applications and transfers to industry and other
fields (find killer applications!),
- Application/link with bio-informatics,
- Rewriting with complexity awareness,
- Proof techniques for non necessarily equationally interpreted rewriting,
- Education oriented activities,
- Methodology.
4. Rewriting and higher-order features.
4.1. The Rewriting Calculus as a Uniform View of Rewriting and Lambda-Calculus,
Claude Kirchner (Nancy).
The principle is to use a proof by rewriting as a function. Applying a
rule to a term may give several results, or none. So rules applications
and results have to be explicit objects, rho-terms.
The lambda-calculus, rewriting and conditional rewriting have natural
encoding in the rho-calculus. This gives a functional view of rewriting.
4.2. General discussion on that topic.
The relationships between the rewriting and the higher-order logic
communities are numerous. Concepts that bridge the concepts of rewriting
and higher-order features (CRS, HRS, ERC, rewriting calculus, ...) are
developing and a better understanding of their relationship has to be
developed.
--------------------------------------------------------------------------------