TeReSe

5th Informal Workshop on Term Rewriting


November 18, 2005          Aachen, Germany



Important Dates - Practical Information - Preliminary Schedule - Abstracts


The TeReSe meetings started with a festive meeting in Amsterdam celebrating the publication of the TeReSe book. Traditionally, the format of this meeting is an afternoon of presentations with room for discussions over dinner. Subsequent workshops took place in Eindhoven, in Utrecht and again in Eindhoven. We hope to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research.

IMPORTANT DATES

Registration of TalksSunday, October 30
Participant registrationSunday, November 6

Please contact Peter Schneider-Kamp for registering talks and participants.

PRACTICAL INFORMATION

The TeReSe will take place in the computer science complex located at Ahornstr. 55. The presentations will be held in the media room 5052 which is located on the ground floor of the building E2. For information on how to get there, please look at the arrival information.

If you are interested in giving a talk or if you have any other questions regarding the organization of the meeting, please contact:

Peter Schneider-Kamp
psk@informatik.rwth-aachen.de
PRELIMINARY SCHEDULE  (Ahornstr. 55, Building E2, Media Room 5052)

Friday, November 18

13:00 - 13:45   Application of a Prefix Property of Higher-Order Rewriting Systems to Finite Family Developments




Sander Bruggink, Universiteit Utrecht
13:45 - 14:30   Match-Bounded String Rewriting




Jörg Endrullis, Vrije Universiteit Amsterdam
 
14:30 - 15:00   Coffee Break
 
15:00 - 15:45   Proving termination of string rewriting by matrix interpretations




Hans Zantema, TU Eindhoven
15:45 - 16:30   Disproving Termination of Term Rewriting




Jürgen Giesl, RWTH Aachen
16:30 - 17:00   TeReSe business meeting




17:00 - ??:??   Dinner and Christmas Market




ABSTRACTS

Sander Bruggink: Application of a Prefix Property of Higher-Order Rewriting Systems to Finite Family Developments

A rewriting system has the prefix property, in its most general form, if it is the case that, given some rewrite step from s to t, the ancestor of a prefix of t is a prefix of s. In this talk I prove a prefix property for higher-order rewriting systems, by reducing the property to a prefix property for a lambda calculus with explicit substitutions, and use this result to prove finiteness of family developments.

Jörg Endrullis: Match-Bounded String Rewriting
  1. Proving termination with match-bounded string rewriting
  2. Finite automata that certify the termination of string rewriting
  3. A efficient decomposition algorithm
  4. Jambox
Hans Zantema: Proving termination of string rewriting by matrix interpretations

Termination of 
aa -> bc
bb -> ac
cc -> ab
was an open problem until a few months ago when it was solved by Hofbauer and Waldmann by very elementary matrix interpretations found as a result of extensive computer search. In this talk we present
  • the approach for arbitrary string rewriting,
  • a termination proof for this system,
  • indications of how to find such a proof, and
  • a simplification of the approach as it has been implemented in the most recent version of TORPA.
Jürgen Giesl: Disproving Termination of Term Rewriting

Most existing techniques for automated termination analysis try to prove termination and there are hardly any methods to prove non-termination. In this work, we introduce techniques to disprove termination of term rewrite systems (TRSs) within the so-called dependency pair framework. Apart from disproving full termination, we also present new methods which can disprove termination under the innermost evaluation strategy (i.e., they can disprove innermost termination). Innermost termination is particularly important in practice, since it corresponds to termination under the eager call-by-value evaluation strategy used in many programming languages.

We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving (innermost) termination of term rewriting.

The talk is based on joint work with Rene Thiemann and Peter Schneider-Kamp.