17th Informal Workshop on Term Rewriting

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


Participant registrationSunday, March 25

Please contact Thomas Ströder for registering participants.


The TeReSe will take place in the computer science complex located at Ahornstr. 55. The presentations will be held in the lecture hall AH II which is located on the first floor of the main building. 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:

Thomas Ströder

PRELIMINARY SCHEDULE  (Ahornstr. 55, Main Building, Lecture Hall AH II)

Wednesday, March 28

13:30 - 14:00   Soundness and Completeness of Infinitary Term Graph Rewriting

Patrick Bahr, Københavns Universitet
14:00 - 14:30   CRSX: a polymorphic specification language (Or: what I did last summer)

Cynthia Kop, Vrije Universiteit Amsterdam
14:30 - 15:00   Polynomial Interpretations for Higher-Order Rewriting

Carsten Fuhs, University College London
15:00 - 15:30   Coffee Break
15:30 - 16:00   Expressibility in the Lambda Calculus with Letrec

Jan Rochel, Universiteit Utrecht
16:00 - 16:30   CARPA: Counter examples in Abstract Rewriting Produced Automatically

Hans Zantema, TU Eindhoven / RU Nijmegen
16:30 - 17:00   Detecting Non-Looping Non-Termination

Jürgen Giesl, RWTH Aachen

17:00 - 17:30   TeReSe business meeting

18:00 - ??:??   Dinner at Waldschenke (Lütticher Str. 340) - location info


Patrick Bahr: Soundness and Completeness of Infinitary Term Graph Rewriting

Infinitary term rewriting provides a tool for reasoning about infinite computations and infinite data as we conceptually find them in lazy functional programs. Term graph rewriting, on the other hand, captures the other defining aspect of lazy functional programming: sharing. With the goal of unifying both paradigms, we generalise the infinitary term rewriting theory to term graphs. We follow two approaches known from infinitary term rewriting: one based on a metric and another based on a partial order on term graphs.

In the literature, infinitary term graph rewriting has been dismissed as not being complete w.r.t. infinitary term rewriting. Our results show, however, that partial order infinitary term graph rewriting is sound and complete w.r.t. infinitary term rewriting. Moreover, we show that the partial order-based calculus forms a conservative extension of the metric-based one similarly to the setting of infinitary term rewriting. Using this correspondence between the partial order-based calculus and the metric-based calculus, we are able to derive soundness and a weakened form of completeness for metric infinitary term graph rewriting.

Cynthia Kop: CRSX: a polymorphic specification language (Or: what I did last summer)

The CRSX system, a functional programming language particularly designed to specify compilers, can be seen as a formalism of higher-order term rewriting. I will discuss this formalism, its peculiarities, and its relation to other higher-order term rewriting formalisms.

Carsten Fuhs: Polynomial Interpretations for Higher-Order Rewriting

The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed λ-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA.

This talk is based on joint work with Cynthia Kop.

Jan Rochel: Expressibility in the Lambda Calculus with Letrec

We investigate the relationship between finite terms in lambda-letrec, the lambda calculus with `letrec', and the infinite lambda terms they express. As there are easy examples of infinite lambda terms that, intuitively, are not unfoldings of terms in lambda-letrec, we consider the question: How can those infinite lambda terms be characterised that are lambda-letrec-expressible in the sense that they can be obtained as infinite unfoldings of terms in lambda-letrec?

For `observing' infinite lambda terms through repeated `experiments' carried out at the head of the term we introduce two rewrite systems (with rewrite relations) -reg-> and -reg+-> that decompose the term structure, and produce `generated subterms' in two notions. Thereby the sort of the step can be observed as well as its target, a generated subterm. In both systems there are four sorts of decompo- sition steps: -lambda-> steps (decomposing a lambda-abstraction), -@_0-> and -@_1-> steps (decomposing an application into its function and argument), and respectively, -del-> steps (delimiting the scope of an abstraction, for -reg->), and -S-> (delimiting of scopes, for -reg+->). These steps take place on infinite lambda-terms furnished with a leading prefix of abstractions for gathering previously encountered lambda-abstractions and keeping the generated subterms closed. We call an infinite lambda term `regular'/ `strongly regular' if its set of -reg-> -reachable/-reg+-> -reachable generated subterms is finite. Furthermore, we analyze the binding structure of infinite lambda terms with the concept of `binding-capturing chain'.

Utilizing these concepts, we answer the question above by providing two characterizations of lambda-letrec-expressibility. For all infinite lambda terms M, the following statements are equivalent:
(i): M is lambda-letrec expressible;
(ii): M is strongly regular;
(iii): M only has finite binding-capturing chains.

Hans Zantema: CARPA: Counter examples in Abstract Rewriting Produced Automatically

Rewriting notions like termination, normal forms, and confluence can be described in an abstract way referring to rewriting only by a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counter examples showing that particular generalizations do not hold. In this talk a technique is presented to find such counter examples fully automatically by the tool CARPA.

The basic idea is to fix the number of objects of the abstract rewrite system, and to express required conditions in a satisfiability (SAT) formula, and then call a current SAT solver. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

Jürgen Giesl: Detecting Non-Looping Non-Termination

We introduce a technique to prove non-termination of term rewrite systems automatically. In contrast to most previous approaches, our technique is also able to detect non-looping non-termination.

This is joint work with Fabian Emmes and Tim Enger.