|Registration of Talks||Wednesday, May 12|
|Participant registration||Sunday, May 16|
If you are interested in giving a talk or if you have any other questions regarding the organization of the meeting, please contact:
| Friday, May 28
|13:30||-||14:15||Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting|
|Clemens Grabmayer, Universiteit Utrecht|
|Johannes Waldmann, HTWK Leipzig|
|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|
|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:
This talk is based on joint work with Lars Noschinski and Jürgen Giesl.