TE(rm) RE(writing) SE(minar)

Nijmegen, November 28, 2008

This meeting on term rewriting will be held at the Radboud Universiteit Nijmegen on November 28, 2008, in
Gymnasion
Heyendaalseweg 141
room 4
How to get there?
Gymnasion is located at D5/6 on the campus map. Once you have arrived at Nijmegen Central Station, the easiest way to get to the university is by bus 10.

Schedule:

time	speaker	title
13.30 - 14.15	Vincent van Oostrom (UU)	Preservation of strong normalisation
14.15 - 15.00	Fabian Emmes (RWTH Aachen)	Improving Context-Sensitive Dependency Pairs
15.00 - 15.30	break
15.30 - 16.15	Herman Geuvers (RU / TUe)	Degrees of undecidability of TRS properties
16.15 - 17.00	Jan Willem Klop (VU / RU)	A Gallery of Streams
17.00 - 17.30	TERESE business meeting
18.00 - ???	dinner in city of Nijmegen	Restaurant Ankara, B. vd Berghstraat 144, 6512DR Nijmegen

Abstracts:

Vincent van Oostrom: Preservation of strong normalisation
We present several implementations of the lambda-calculus proposed in the literature (e.g. due to Revesz, Bloo, Rose, Sinot, O'Conchuir, Kesner, Lengrand,...), relate them via our notion of implementation, and classify them according to whether or not they preserve termination. Although most, but not all, of the latter results are known, we will put emphasis on our proof method which works rather uniformly over all these implementations.

Fabian Emmes: Improving Context-Sensitive Dependency Pairs
Context-sensitive rewrite systems (a generalized form of term rewrite systems) are used to model the evaluation of lazy programming languages. We present a contemporary approach to prove termination of such rewrite systems. For analysis of full termination, dependency pairs are among the most popular techniques, and a whole framework has been developed for the resulting termination problems. In recent work, the notion of dependency Pairs has been adapted to the context-sensitive setting. However, these context-sensitive dependency pairs include collapsing dependency pairs where the right-hand side is just a variable. This makes adapting the dependency pair framework to context-sensitive dependency pairs hard. We show how to avoid these collapsing dependency pairs and how to adapt the dependency pair framework to context-sensitive rewriting. In particular, techniques from the dependency pair framework that transform dependency pairs become extremely powerful when using them for context-sensitive rewriting. Empirical results show that our approach improves the power of termination analysis for context-sensitive rewriting considerably.

Herman Geuvers: Degrees of undecidability of TRS properties
This is joint work with Joerg Endrullis and Hans Zantema.
Many (most?) interesting problems in term rewriting are undecidable, but there are different levels of undecidability. The most well-known is the class of recursive enumerable (r.e.) problems. P(x) is r.e. if one can write a semi-decision algorithm f such that f(x) = 1 iff P(x) holds (but f(x) may not terminate if P(x) is false). There is a hierarchy of undecidable problems, called the arithmetic hierarchy. The position in the arithmetic hierarchy of a problem is determined by the number of quantifier alterations that is required to describe it, where the quantifiers range over the natural numbers.
In term rewriting, interesting undecidable results are WN and SN, either for a rewrite system or for a term in a fixed rewrite system. We will review the place of these problems in the arithmetic hierarchy, which is well-known.
For infinitary rewriting, the property SN^infty is relevant, stating that every infinite reduction -- roughly speaking -- produces a larger and larger "fixed" part of an infinite term. Similarly one can define WN^infty. These properties are also undecidable, but they are more complex than any problem in the arithmetic hierarchy: they require a quantification over infinite sequences of natural numbers. Thus SN^infty and WN^infty are placed in the analytic hierarchy, as well as DP problems. In the talk we will discuss and prove their exact place.

Jan Willem Klop: A Gallery of Streams
We present work (in cooperation with Joerg Endrullis, Clemens Grabmayer, Roel de Vrijer, Dimitri Hendriks) on some graphical renderings of various interesting streams such as Thue-Morse, Toeplitz, Sierpinski, Fibonacci, Mephisto Walz, Baum-Sweet, Kolakoski, Rudin-Shapiro. Next we propose an equivalence on streams via finite state transducers and discuss some of the ensuing questions such as: what is the structure of the hierarchy of degrees induced by this equivalence? Do some well-known streams such as Thue-Morse, and Sierpinsky, have the same degree? Finally, we are interested in prime degrees. A degree is prime if it only reduces to itself or to the bottom degree 0 of the eventually periodic streams. We investigate the primality of the Thue-Morse stream, and others.