--------------------------------------------------------------------------------
Minutes of the Fourth Workshop of the
IFIP WG-1.6 on Term Rewriting
Copenhagen, Denmark
July 25, 2002
--------------------------------------------------------------------------------
Agenda
1. Progress reports.
1.1. Modular Termination Proofs Using Dependency Pairs,
Jürgen Giesl.
1.2. On Modularity in Context-sensitive Rewriting,
Bernhard Gramlich.
1.3. Deciding satisfiability problems by rewrite-based deduction: experiments
in the theory of arrays,
Maria Paola Bonacina.
1.4. Progress report,
Nachum Dershowitz.
1.5. Lambda-calculus with end-of-scope,
Vincent van Oostrom.
1.6. Computational restrictions of rewriting in functional programming,
Salvador Lucas.
2. Business session.
Chaired by Claude Kirchner.
Participants: Franz Baader, Maria Paola Bonacina, Nachum Dershowitz, Jürgen
Giesl (invited), Bernhard Gramlich (invited), Jean-Pierre Jouannaud, Claude
Kirchner (Chairman), Hélène Kirchner, Salvador Lucas (invited), Aart
Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Yoshihito Toyama,
Laurent Vigneron (Secretary).
Meeting opened at 9:00
Meeting closed at 17:00
--------------------------------------------------------------------------------
1. Progress reports.
1.1. Modular Termination Proofs Using Dependency Pairs,
Jürgen Giesl (Aachen).
The dependency pair approach allows automated termination and innermost
termination proofs for many term rewriting systems for which such proofs
were not possible before. The motivation for this approach is that
virtually all previous techniques for automated termination proofs of term
rewriting systems were based on simplification orderings. In practice,
however, many rewrite systems are not simply terminating, i.e., their
termination cannot be verified by any simplification ordering.
The dependency pair approach has been refined in order to prove termination
in a modular way. This refinement, permitting the use of several different
orderings in one termination proof, is inevitable in order to verify the
termination of large rewrite systems occurring in practice.
New modularity results based on dependency pairs are presented. First, the
well-known modularity of simple termination for disjoint unions can be
extended to DP quasi-simple termination, i.e., to the class of rewrite
systems where termination can be shown automatically by the dependency pair
technique in combination with quasi-simplification orderings. Second, the
refinement of the dependency pair approach yields new modularity criteria
for innermost termination, extending previous results in this area. In
particular, existing results for modularity of innermost termination can
easily be shown to be direct consequence of these new criteria.
1.2. On Modularity in Context-sensitive Rewriting,
Bernhard Gramlich (Vienna).
Context-sensitive rewriting (CSR) has recently emerged as an interesting
and flexible paradigm that provides a bridge between the abstract world of
general rewriting and the (more) applied setting of declarative
specification and programming languages such as OBJ*, CafeOBJ, ELAN, and
Maude. A natural approach to study properties of programs written in these
languages is to model them as context-sensitive rewriting systems. Here we
are especially interested in proving termination of such systems, and
thereby providing methods to establish termination of e.g. OBJ* programs.
For proving termination of context-sensitive rewriting, there exist a few
transformation methods, that reduce the problem to termination of a
transformed ordinary term rewriting system (TRS). These transformations,
however, have some serious drawbacks. In particular, most of them do not
seem to support a modular analysis of the termination problem. We show
that a substantial part of the well-known theory of modular term rewriting
can be extended to CSR, via a thorough analysis of the additional
complications arising from context-sensitivity. More precisely, we mainly
concentrate on termination (properties). The obtained modularity results
correspond nicely to the fact that in the above languages the modular
design of programs and specifications is explicitly promoted, since it can
now also be complemented by modular analysis techniques
1.3. Deciding satisfiability problems by rewrite-based deduction: experiments in
the theory of arrays,
Maria Paola Bonacina (The University of Iowa).
Joint work with Alessandro Armando, Silvio Ranise, Michael Rusinowitch,
Aditya Sehgal.
Satisfiability procedures are a key component of verification tools. The
endeavour of designing, proving correct, and implementing a satisfiability
procedure for each decidable theory of interest is far from simple. Most
problems involve more than one theory, needing to combine satisfiability
procedures.
Using a theorem prover, with the union of the theories in input, is
simpler, and does not require theory-specific completeness proofs, assuming
the theorem proving strategy is sound and complete. If the theorem-proving
strategy is guaranteed to terminate on the theories of interest, it is in
itself a decision procedure. Such termination results were recently
obtained for ordering-based strategies, with a paramodulation-based
inference system, on the theories of lists, arrays with extensionality and
their combination, among others. Termination achieved, the issue of
efficiency remains.
We propose two sets of synthetic benchmarks in the theory of arrays with
extensionality, and we report on experiments showing that a theorem prover
- the E system - compares successfully with the state-of-the-art validity
checker CVC. This offers evidence that an approach based on
general-purpose deduction may be both practical and theoretically elegant.
1.4. Progress report,
Nachum Dershowitz (Tel Aviv).
Presentation of the last books published concerning calendar calculations,
based on constraints solving. Presentation of the ongoing works and
cooperations.
1.5. Lambda-calculus with end-of-scope,
Vincent van Oostrom (Utrecht).
Presentation of an extension of the lambda-calculus with an end-of-scope
operator, which came up naturally, while extending the optimal first-order
setting to higher-order. The rough idea is that a role of the lambda is to
open a scope and it is only natural to introduce an explicit operator to
end a scope. The nice thing is that (an extension of) beta-reduction can
be defined which is confluent without alpha-reduction. Alpha reduction is
only needed when removing end-of-scopes. This calculus is halfway toward
an optimal implementation of the lambda calculus: for that also the
explicit operators for (un)sharing, the so-called fan-in and fan-out, need
to be introduced.
The proofs have been realized in Coq.
1.6. Computational restrictions of rewriting in functional programming,
Salvador Lucas (Valencia).
Given a term rewriting system, the definition of a strategy over this
system should always preserve normal forms. When this is not the case, one
should talk about computational restrictions, for which one can define
strategies.
Using computational restrictions, the termination of (functional) programs
corresponds to termination of strategic rewriting, and the semantics of
(functional) programs corresponds to infinitary normalizing strategies.
Computational restrictions on rewriting are a trade off between termination
and correctness/completeness. Some examples of computational restrictions
are strategy annotations, just-in-time annotations, on-demand strategy
annotations, and context-sensitive rewriting.
2. Business meeting.
** Rewriting events:
In the past year, with the following abbreviations,
S: submissions
IP: invited presentations
T: tutorials
PL: panel list
SP: system presentations
RP: regular presentations
we had:
- Conference on Rewriting Techniques and Applications
(RTA'02, Copenhagen, Jul. 21-24, 2002):
49 S, 3 IP, 4 SP, 22 RP
Proceedings: LNCS 2378
- Workshop on Rule-Based Programming
(Rule'01, Firenze, Sept. 4, 2001):
14 S, 11 RP
Proceedings: ENTCS volume 59-4 (all presented papers)
- Workshop on Reduction Strategies in Rewriting and Programming
(WRS'01, Utrecht, May 26, 2001):
6 S, 2 IP, 3 PL, 6 RP
Proceedings: ENTCS volume 57 (all presented papers)
- Workshop on Reduction Strategies in Rewriting and Programming
(WRS'02, Copenhagen, Jul. 21, 2002):
10 S, 2 IP, 8 RP
Proceedings: ENTCS volume 70-6
- Workshop on Termination
(WST'01, Utrecht, May 20-21, 2001):
21 RP
- Workshop on Rewriting in Proof and Computation
(RCP'01, Sendai, Oct. 25-27, 2001):
9 IP, 12 RP
- Workshop on rewriting logic and applications
(WRLA'02, Pisa, Sept. 19-21, 2002):
17 S, 3 IP, 4 T, 4 SP, 12 RP
For a total of 129 submissions (of course there may be redondancies)
104 regular presentations
23 invited presentations
Some workshops do even publish their proceedings. This confirms
the good health of rewriting activities. The multiplicity of
rewrite events allows to spread the rewriting publications is
related areas. We should consequently take care to maintain the
main conference RTA with a good level of submissions and of
participants. Group members are invited to stimulate their
collegues to submit their best paper to RTA!
In 2003, RTA will be part of RDP (Federated Conference on Rewriting,
Deduction and Programming) in Valencia, Spain, together with TLCA, FTP and
some other workshops (including the next meeting of this IFIP working
group).
In 2004, RTA will be in Aachen, Germany.
** E-book on Rewriting:
To initiate the work on the e-book, the idea to set up a database
of examples with references and keywords raises. Femke van
Raamsdonk will collect these examples and the access to the
database will be done in XML. Members of the group who are
interested have to contact Femke.
From the general discussion on the e-book, several ideas emerge:
- An editorial board should certainly be set up,
- The contents of the book will have to be different from the
published paper books.
** A new book is going to be published soon and is presented by Vincent:
"Term Rewriting Systems", Cambridge University Press, by Terese
(editors M. Bezem, J.W. Klop and R.C. de Vrijer, Amsterdam).
** Renewal of group membership:
Some members of this IFIP working group being non-active (wrt. the group),
we have defined the following policy:
" After 3 years of not participating to a group meeting, a member
is asked to confirm his involvement in the working group or to
leave his place to allow for the admission of new members."
The list of members concerned will be set annually and the chair
of the working group will be in charge to ask them for their further
involvement. Honorary Members will also be proposed and ratified
by the active members.
The integration of new researchers will be done after two invitations in a
meeting, after approval by the group members.
This year, four researchers are added:
- Femke van Raamsdonk (http://www.cs.vu.nl/~femke/),
- Jürgen Giesl (http://www-i2.informatik.rwth-aachen.de/giesl/),
- Bernhard Gramlich (http://www.logic.at/staff/gramlich/),
- Salvador Lucas (http://www.dsic.upv.es/users/elp/slucas.html).
========================================================================
The next WG1.6 meeting will be held during the RDP joint conference in
Valencia, Spain, Thursday 12, June 2003. Even if there are several
other quite interesting meetings in parallel, please make a priority to
attend the workshop.
========================================================================
---------------------------- Calendar of RDP'03 ------------------------------
June 2003 sun mon tue wed thu fri sat m=morning
8 9 10 11 12 13 14 a=afternoon
e=evening
RTA ma ma m
TLCA ma m ma
FTP ma ma ma
WG 1.6 ma
RULE ma
UNIF ma ma
WFLP ma ma
WRS ma
WST ma ma
Excursion a
Joint inv. speaker m
Dinner e
TLCA bussiness m. e
RTA bussiness m. e
FTP bussiness m. e
------------------------------------------------------------------------------