--------------------------------------------------------------------------------
Minutes of the Third Workshop of the
IFIP WG-1.6 on Term Rewriting
University of Utrecht, Utrecht, The Netherlands
May 25, 2001
--------------------------------------------------------------------------------
Agenda
1. Progress reports.
1.1. Deciding the confluence of GTRS in PTIME,
Robert Nieuwenhuis.
1.2. Computing BDDs by rewriting,
Hans Zantema.
1.3. Rewriting activities in Valencia,
Salvador Lucas.
1.4. Progress report on rewriting activities in Japan,
Yoshihito Toyama.
1.5. Progress report on rewriting activities in Austria,
Bernhard Gramlich.
1.6. About 2 applications of rewriting: multiplying by 11 and Origami,
Corrado Boehm.
1.7. On applying dependency pairs to process verification,
Juergen Giesl.
2. Business session.
3. How to promote rewriting in the large?
4. Panel: On applications of rewriting.
Chaired by Claude Kirchner.
Participants: Franz Baader, Corrado Böhm, Nachum Dershowitz, Jürgen Giesl
(invited), Bernhard Gramlich (invited), Thomas Hillenbrand (representing
Harald Ganzinger), Tetsuo Ida, Claude Kirchner (Vice-Chairman), Jan Willem
Klop, Sébastien Limet (representing Siva Anantharaman), Salvador Lucas
(invited), Aart Middeldorp, Robert Nieuwenhuis, Vincent van Oostrom, David
Plaisted, Yoshihito Toyama, Laurent Vigneron (Secretary), Hans Zantema.
Meeting opened at 9:00
Meeting closed at 17:10.
--------------------------------------------------------------------------------
1. Progress reports.
1.1. Deciding the confluence of GTRS in PTIME,
Robert Nieuwenhuis (Barcelona).
(joint work with H. Comon and G. Godoy)
Termination and confluence are undecidable in general.
In the ground case, termination is PTIME [Plaisted 93], and confluence is
decidable [Dauchet et al. 87, Oyamaguchi 87] in exponential time.
The question is: what is the exact complexity of deciding confluence of
ground term rewriting systems (GTRS)?
Many attempts have been done, based on rewriting suffixes and considering
stable prefixes (for strings).
The first presented result is an algorithm in PTIME for strings rewriting
systems. It is based on the following ideas:
- to transform a rewrite system R into a system where the left-hand sides
are subterms of R (Plaisted's idea),
- to apply reductions in order to always increase the length of the stable
prefix.
A PTIME algorithm has been designed for full GTRS:
- to apply three PTIME transformations: Curry form (one binary operator +
constants), shallow rules, Plaisted's transformation,
- to decide in PTIME if the binary operator becomes stable only by
rewriting in its arguments,
- to check the necessary conditions for confluence,
- to test in PTIME if the sides of the rewrite system are deeply joinable.
The exact complexity obtained is PTIME-hardness for strings, and
PTIME-completeness for strings and terms.
1.2. Computing BDDs by rewriting,
Hans Zantema (Eindoven).
Decision trees can be written as terms, since a decision tree can be seen
as a Boolean function. Sharing subtrees consists in building a directed
acyclic gragh, and to solve a binary decision diagram (BDD).
The main problem is to get a unique representation.
By ordering atoms, we get ordered BDD (OBDD). But we need maximally shared
OBDD, and without simplifiable subtrees. This corresponds to reduced OBDD
(ROBDD).
Each Boolean function has a unique representation by a ROBDD.
This result follows from the termination and confluence of a TRS
transforming a BDD into an OBDD.
Note that standard ROBDD computation has polynomial complexity.
However, the satisfiability of BDDs is NP-hard, and BDDs can be of
exponential size.
1.3. Rewriting activities in Valencia,
Salvador Lucas (Valencia).
The rewriting activities in Valencia have started in the 70s with the
collaboration of Isidro Ramos with Claude Pair (Nancy). They worked on
algebraic methodologies, types and logics. This collaboration between
Valencia and Nancy has continued in the 80s with Miguel Muñoz and
Jean-Pierre Jouannaud.
María Alpuente is now at the head of the ELP group. The main topics of
this group concern programming languages:
- semantics of the integration: formalization, optimization strategies
based on incremental narrowing, semantics of narrowing computations,
- program analysis: abstract narrowing for testing equational
satisfiability,
- program transformation: partial evaluation of functional logic programs,
- inductive programming in functional logic programs, and applications in
software engineering,
- rewriting techniques in programming: context sensitive rewriting (CSR),
termination, semantics of rewriting computations, rewriting strategies.
The ELP group has many collaborations in Europe, plus some in the USA and
in Japan. It is involved in several national and international projects.
The ongoing work concerning rewriting includes:
- innermost termination of CSR,
- comparison of models for rewriting with syntactic replacement
restrictions,
- termination of OBJ programs,
- decidability issues in transfinite rewriting,
- analysis of program properties using rewriting semantics.
1.4. Progress report on rewriting activities in Japan,
Yoshihito Toyama (Sendai).
A lot of groups, all over Japan, work on rewriting. Twice a year, there is
a common meeting (plus some invited foreigners), where each participant
gives a talk. The scope of this meeting concerns: TRS, lambda-calculus,
type theory, proof theory, functional programming, logic programming,
automated deduction, ...
The main topics developed in Japan are:
- reduction strategies for TRS (most use tree automatas),
- termination,
- narrowing (conditional TRS, lazy conditional narrowing),
- higher-order: simply typed TRS, HRPO, theory of typed HRS,
- infinite lambda-calculus, transfinite reduction,
- Church-Rosser property,
- modular: top-down labelling, disjoint GRS,
and many other topic related to concurrence,...
The most well-known systems developed in Japan are CafeOBJ (JAIST) and CFLP
(Tsukuba).
Note that the international workshop on Rewriting in Proof and Computation
(RPC) will take place in Sendai, Oct. 25-27, 2001.
1.5. Progress report on rewriting activities in Austria,
Bernhard Gramlich (Vienna).
The number of universities with research in computer science,
rewriting/equational theory, or theory is very low in Austria. There are
mainly three: TU Wien, U. Wien, U. Linz/RISC. Another university is getting
concerned: U. Innsbruck.
Main researchers in Linz: Buchberger, Winkler.
Topics: symbolic computation, Groebner bases,...
Main researcher in U. Wien: Friedman.
Topic: set theory.
The main center of research is the TU Wien, where people work on:
- equational reasoning: meta terms, unification theory, equational problems
(algorithms and complexity), rewriting, deduction, strategies (Salzer,
Pichler, Gramlich),
- proof theory: model construction and representation for clause sets,
semantics trees, induction (Fermüller, Leitsch,...),
- automata, formal languages (Kuide),
- functional logic programming (Krall,...),
- logic, databases, AI, knowledge representation (Gottlob,...).
So the main domains are: proof theory, mathematical logic, non-classical
logic(s), databases and complexity.
But rewriting and equational reasoning are underrepresented.
1.6. About 2 applications of rewriting: multiplying by 11 and Origami,
Corrado Boehm (Roma).
The first presentation is a functional description of number stacks:
rewrite rules describing addition of numbers represented by stacks of
digits.
Question: is multiplication by 11 simpler tan addition?
Answer: yes, with one more memory.
The second presentation concerns geometrical origami.
Functions are described like agents. For example, the intersection of two
lines, the line passing through two points, the perpendicular of a line
passing through a point wrt. another point,...
This permits to represent second and third degree problems.
Therefore, constructing 3D origami solved third degree problems.
This is exemplified with the construction of a paper glass.
1.7. On applying dependency pairs to process verification,
Juergen Giesl (Aachen).
(joint work with Thomas Arts)
Process verification consists in testing the termination of a conditional
TRS.
Messages are sent to the process, it computes something, then sends
the results. The problem is that the size of the messages sent is
limited. What cannot be sent is stored in the process.
Because of those stores, one needs to send empty messages to the processes
for emptying their memory.
The verification of a process is coded as a conditional TRS left-right
decreasing, but proving its termination is difficult.
The CTRS is transformed into a TRS, and its innermost termination is proved
using dependency pairs: there should be no innermost infinite chain of
dependency pairs.
Narrowing is used for breaking cycles (some pairs are deleted, other are
added).
But this is valid only for non-overlapping systems.
For overlapping systems, innermost termination does not imply termination.
So a solution is to use narrowing, rewriting, and instantiation of
dependency pairs.
The application of this technique concerns properties that are not set,
ie. to verify that something will happen.
2. Business session.
* Election: Jieh Hsiang has decided to leave the chair of the group. There
was one candidate, Claude Kirchner.
Nachum Dershowitz has organised the elections by e-mail. From 43 members,
there has been 37 votes: 34 in favor; 1 abstention; 2 additional votes are
questionable.
So Claude Kirchner has been proposed as new chairman of the group to the
TC1 chair, Giorgio Ausiello.
* Evolution of the working group members:
- Some members are not active. People missing three consecutive
meetings can loose their membership. This will be decided at
each meeting. A possibility is to have honorary members.
- Some people are interested to join the working group. The main problem is to
know the rules to follow. Do we have to set criteria? (number of
invitations to the group meetings, number of publications in the field,
recommandation of current members,...)
* Next meeting: it will take place the day after the next RTA (July 25,
2002), in Copenhagen (Denmark); but we have to ask it to the FLoC
organizers.
In this meeting, the talks should be about collaborations, and research in
some countries.
3. How to promote rewriting in the large?
There are two levels of promotion:
- internal: to put together examples, counter-examples, systems, so that it
can be easily found and completed,
- external: to promote rewriting in other research domains; to attract
students; to show to the general public that rewriting is used everywhere.
For this, several propositions are done:
- to create a database of examples and counter-examples, starting with very
simple examples taken in recent books; other examples may be added by
students. The best medium for this would be a web page. Some of us have
already some examples, but they need to be maintained.
- to create a rewrite laboratory, essentially for teaching. Its minimal
requirements are: Knuth-Bendix procedure, computation of canonical
forms,... The main problems for creating this tool is to decide what to
put inside, who is going to implement it, and who is going to maintain it.
Some systems like this have already been designed (eg. RRL), but they are
no more maintained.
- to compete with other scientific domains.
- to promote books/surveys for undergraduate, but to impose a course at this
level is difficult.
One of the best way to promote rewriting is to create an e-book: it is
incremental, easy to consult. Some people are interested to contribute.
But for realizing it, we need a steering committee, able to find specialists
for writing chapters.
The organization of the e-book itself is to be discussed: shall we follow the
historical development?
And it has not to be in competition with existing books.
The last point that is mentioned is to use more often the rewriting list,
maintained by Pierre Lescanne (rewriting@ens-lyon.fr).
4. Panel: On applications of rewriting.
The main remarks are that the 'A' of RTA is not considered enough: we have to
present papers about applications, to involve industrials (in the program
committee, for instance), and to invite industrials.
A challenge would be that all of us write an application paper within two
years.
--------------------------------------------------------------------------------