TeReSe

13th Informal Workshop on Term Rewriting


May 28, 2010         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, in Eindhoven, in Aachen, in Amsterdam, in Utrecht, in Eindhoven, in Aachen, in Amsterdam, in Nijmegen, and in Utrecht. We hope to attain the same friendly atmosphere as in past workshops, which enabled fruitful exchanges leading to joint research.

IMPORTANT DATES

Registration of TalksWednesday, May 12
Participant registrationSunday, May 16

Please contact Carsten Fuhs 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:

Carsten Fuhs
fuhs@informatik.rwth-aachen.de
PRELIMINARY SCHEDULE  (Ahornstr. 55, Building E2, Media Room 5052)

Friday, May 28

13:30 - 14:15   Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting




Clemens Grabmayer, Universiteit Utrecht
14:15 - 15:00   Tropical Termination




Johannes Waldmann, HTWK Leipzig
 
15:00 - 15:30   Coffee Break
 
15:30 - 16:15   Complexity of Guided Insertion-Deletion in RNA-editing




Hans Zantema, TU Eindhoven / RU Nijmegen
16:15 - 17:00   Dependency Pairs for Complexity Analysis Revisited




Fabian Emmes, RWTH Aachen
17:00 - 17:30   TeReSe business meeting




18:00 - ??:??   Dinner at Tradition aus Vietnam bei Van (Burtscheider Str. 11-13) - location info




ABSTRACTS

Clemens Grabmayer: Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial.

We show that the infinitary unique normal form property UNinf fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UNinf also fails for the infinitary lambda-beta-eta-calculus.

As positive results we obtain the following: Infinitary confluence, and hence UNinf, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we consider the triangle and diamond properties for infinitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.

This talk is based on joint work with Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom.


Johannes Waldmann: Tropical Termination
The tropical semiring uses the "min" and "plus" operations on the natural numbers, extended with "+infinity".

We use interpretation by tropical vector-valued linear functions to prove termination of string and term rewriting. The development is similar to arctic termination (with "max" and "plus"), and it has been formally verified recently.

The tropical semiring has the distinctive feature that its zero element (+infinity) is maximal in the natural order. It follows that the support of a compatible interpretation is closed w.r.t. rewriting. This allows to apply the tropical semiring in termination proofs that use the RFC method (right hand sides of forward closures).

This talk is based on joint work with Dieter Hofbauer and Adam Koprowski.


Hans Zantema: Complexity of Guided Insertion-Deletion in RNA-editing
Inspired by RNA-editing, we study an elementary formalism of string replacement based on insertion and deletion using a fixed finite set of so-called guides, and in which only occurrences of a single symbol are inserted or deleted.

While in this replacement mechanism computation lengths are at most exponential by construction, we show that this exponential upper bound is tight. Moreover, we show that both the class of regular languages and the class of context-free languages are not closed under this replacement mechanism. The underlying theory is based on string rewriting: it is shown that the replacement mechanism can be mimicked by a particular kind of string rewriting, and results on string rewriting are then transformed to the final results.


Fabian Emmes: Dependency Pairs for Complexity Analysis Revisited
Recent approaches to handle runtime complexity of term rewriting lack full modularity, are only applicable to restricted kinds of TRSs, and impose constraints on the orders which are very hard to fulfil.

In this talk we take a fresh look at the application of dependency pair techniques to analyze innermost runtime complexity. Compared to existing approaches this yields the following advantages:
  • The new design of Complexity Dependency Pair Problems leads to of a framework in which problems can be refined and simplified in the style (and with the ease) of the Dependency Pair Framework.
  • Most techniques from termination analysis can now be directly transferred to the runtime complexity setting.
  • The constraints on the orders used to prove complexity bounds are considerably reduced.
These advantages combined lead to a significant increase in power in relation to the existing methods.

This talk is based on joint work with Lars Noschinski and Jürgen Giesl.