Term Rewriting Seminar (TeReSe)
14th Informal Workshop on Term Rewriting, November 18th 2010
The Term Rewrite Seminar is a biannual 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 email: 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:4514:00
 Arrival
 14:0014:45

Jeroen Ketema (University of Twente)
Computing with Infinite Terms and Reductions
 14:4515:30

Thomas Ströder (RWTH Aachen University)
Termination Analysis of Real Programming Languages with
Termination Graphs and Dependency Triples
 15:3016:00
 Break
 16:0016:45
 Joerg Endrullis, Clemens Grabmayer, JanWillem Klop, Vincent van Oostrom (University of Utrecht, VU University Amsterdam)
On Equal μterms
 16:4517:30
 Hans Zantema (TU Eindhoven, RU Nijmegen)
Proving equality of streams automatically
 17:3018: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 noncollapsing systems where rules have finite righthand
sides, i.e. we show that if the peak of a ChurchRosser 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 nonlogical 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 higherorder 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 firstorder 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 αconversionfree way, essentially
treating μterms as firstorder terms. The second proof uses
techniques from higherorder 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 αconversionavoiding μ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:
 it restricts to ways of specifying streams that are terminating;
 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 THueMorse stream. This is joined work with
Joerg Endrullis.