Term Rewriting Seminar (TeReSe)

14th Informal Workshop on Term Rewriting, November 18th 2010

The Term Rewrite Seminar is a bi-annual event by the Dutch (and nearby) term rewriting community. It typically takes the form of an afternoon with presentations from each of the represented universities, with room for discussions during a joined dinner. Previous meetings were in Amsterdam, Eindhoven, Utrecht, Eindhoven, Aachen, Amsterdam, Utrecht, Eindhoven, Aachen, Amsterdam, Nijmegen, Utrecht, and in Aachen.

For information and registration, please contact Cynthia Kop by e-mail: kop at few.vu.nl

Coordinates

Thursday November 18, 2010
13:45 - 17:45
Faculty of Sciences, Vrije Universiteit
De Boelelaan 1081, 1081 HV Amsterdam
Room F647 (6th floor, F wing)

How to get there
VU campus map (pdf) -- building (4)

Program

13:45-14:00
Arrival
14:00-14:45
Jeroen Ketema (University of Twente)
Computing with Infinite Terms and Reductions
14:45-15:30
Thomas Ströder (RWTH Aachen University)
Termination Analysis of Real Programming Languages with Termination Graphs and Dependency Triples
15:30-16:00
Break
16:00-16:45
Joerg Endrullis, Clemens Grabmayer, Jan-Willem Klop, Vincent van Oostrom (University of Utrecht, VU University Amsterdam)
On Equal μ-terms
16:45-17:30
Hans Zantema (TU Eindhoven, RU Nijmegen)
Proving equality of streams automatically
17:30-18:00
TeReSe Business Meeting

Afterwards there will be a joined TeReSe dinner for those willing to come. The dinner will take place in Restaurant Mika, a Korean restaurant approximately 15 minutes by foot from the university (or two stops in the metro).

Abstracts of the talks

Computing with Infinite Terms and Reductions (by Jeroen Ketema from the University of Twente).
We define computable infinitary term rewriting, thus introducing computable infinite terms and computable infinite reductions to the study of convergent, potentially infinite reductions over potentially infinite terms. Furthermore, we give a constructive proof of confluence for orthogonal non-collapsing systems where rules have finite right-hand sides, i.e. we show that if the peak of a Church-Rosser diagram consists of computable terms and reductions, then so does the valley, and there is a program computing the valley when given the peak as input.
Termination Analysis of Real Programming Languages with Termination Graphs and Dependency Triples (by Thomas Ströder from RWTH Aachen University)
Termination analysis of term rewrite systems is widely studied. In this talk we investigate techniques and methods how to make this work applicable for termination analysis of programming languages used in real world applications. We use the concept of termination graphs to model the complex aspects of such programming languages. For a given program in a complex language we construct a termination graph and generate a program in a simpler programming language from this graph whose termination implies termination of the original program. The simple programming languages we use in this methodology are term rewrite systems and various extensions of them. We will have a closer look at one such extension, namely dependency triples. These are used to analyse Prolog programs containing non-logical features like, e.g., cuts.
On Equal μ-Terms (by a cooperation of speakers from the University of Utrecht and the VU University Amsterdam)
We consider the higher-order term rewriting system Rμ with its single rule of the form μx.Z(x) → Z(μx.Z(x)), where the signature consists of the variable binding operator μ, a single binary first-order function symbol F, and possibly some constant symbols. We investigate the question whether weak μ-equality , the equivalence relation =μ that is induced by the rewrite relation →μ in R  is decidable.

We establish decidability of =μ by using confluence of →μ to link =μ to joinability of →μ, and by showing decidability of the latter, in three alternative ways. As a preparation we give a characterisation of μ-terms that can be reduced without having to use α-conversion.

The first two proofs build on an idea by Cardone and Coppo to use standardisation of →μ -rewrite sequences. One proof proceeds in an α-conversion-free way, essentially treating μ-terms as first-order terms. The second proof uses techniques from higher-order rewriting, by viewing Rμ as a HRS, and thereby reasoning with α-equivalence classes of μ-terms.

The third proof, which is again organised in an α-conversion free way, uses the fact that the set of →μ-reducts of an α-conversion-avoiding μ-term form a regular tree language. It exploits the fact that recognising emptiness of the intersection of regular tree languages is decidable.

Proving equality of streams automatically (by Hans Zantema from the Technical University Eindhoven and the Radboud University Nijmegen)
We consider the principle of circular coinduction to prove equality of streams. A tool exploiting this principle is CIRC, developed by Rosu and Lucanu, as a layer on the rewriting tool Maude. There the basic approach to check whether two terms are convertible is by computing normal forms and checking whether they are equal. This has two main drawbacks:
  1. it restricts to ways of specifying streams that are terminating;
  2. it is not complete if the TRS is not confluent, which is often the case after adding lemmas and coinduction hypotheses to the TRS.
In our approach we have a general machinery for convertibility, by which the approach can also be used for formats of stream specification that are not terminating, for instance, the pure stream format.
By using several more features like the automatic generation of lemmas, our tool succeeds in proving several equalities fully automatically, for instance, in proving equivalence of several specifications of the THue-Morse stream. This is joined work with Joerg Endrullis.