u.nl Term Rewriting Seminar

Term Rewriting Seminar (TeReSe)

The coordinates of the next TeReSe, an afternoon with presentations on rewriting, are as follows:

Tuesday June 24, 2008
13.15 - 17.30
Faculty of Sciences, Vrije Universiteit
De Boelelaan 1081, 1081 HV Amsterdam
room S205

how to get there
VU campus map (pdf)


13.15 Raúl Gutiérrez (UP de Valencia, RWTH Aachen):

Usable Rules for Context-Sensitive Rewrite Systems

13.45 Joerg Endrullis (VU):
Data-oblivious stream productivity

14.30 Matthias Raffelsieper (TU/e):
A transformational approach to prove outermost termination automatically

15.15 break

15.45 Carsten Fuhs (RWTH Aachen):
Beyond Integer Polynomial Interpretations

16.30 Vincent van Oostrom (UU):
Confluence by decreasing diagrams, converted

17.15 business meeting

17.30 end

Afterwards there will be the opportunity to eat out together.
We intend to have pancakes in the "Amsterdamse Bos".

Abstracts of the talks

Usable Rules for Context-Sensitive Rewrite Systems by Raúl Gutiérrez (UP de Valencia, RWTH Aachen)

Recently, the dependency pairs (DP) approach has been generalized to context-sensitive rewriting (CSR). Although the context-sensitive dependency pairs (CS-DP) approach provides a very good basis for proving termination of CSR, the current developments basically correspond to a ten-years-old DP approach. Thus, the task of adapting all recently introduced dependency pairs techniques to get a more powerful approach becomes an important issue. In this direction, usable rules are one of the most interesting and powerful notions. Actually usable rule have been investigated in connection with proofs of innermost termination of CSR. However, the existing results apply to a quite restricted class of systems. In this paper, we introduce a notion of usable rules that can be used in proofs of termination of CSR with arbitrary systems. Our benchmarks show that the performance of the CS-DP approach is much better when such usable rules are considered in proofs of termination of CSR.

Data-oblivious stream productivity by Joerg Endrullis (VU)

We are interested in finite specifications of infinite streams of data that are based on orthogonal rewrite rules. A stream specification is called `productive' if it can be evaluated continually with a unique data stream being obtained as the limit. Whereas productivity is undecidable in general, for restricted formats computable sufficient conditions can be formulated, and for some formats even decidability of productivity can be established. The usual analysis of the productivity problem, which we also adopt, disregards the identity of data, thus leading to approaches that we call "data-oblivious". We found a method that is provably optimal among all such data-oblivious approaches. This means that in order to improve on our algorithm one has to proceed in a data-aware fashion. For more information about our work on productivity of stream definitions, please visit the productivity page of the infinity project.

A transformational approach to prove outermost termination automatically by Matthias Raffelsieper (TU/e)

We present a transformation from left-linear TRSs to TRSs such that outermost termination of the original TRS can be concluded from termination of the transformed TRS. In this way we can apply state-of-the-art termination tools for automatically proving outermost termination of any given left-linear TRS. Experiments show that this works well for non-trivial examples. This is joint work with Hans Zantema.

Beyond Integer Polynomial Interpretations by Carsten Fuhs (RWTH Aachen)

We present a new approach for termination proofs that uses polynomial interpretations (with possibly negative coefficients) together with the "maximum" function. To obtain a powerful automatic method, we solve two main challenges:

Furthermore, not only can the power of polynomial interpretations be increased by changing the shape of the interpretation (e.g., by using the "maximum" function), but also by using interpretations into a different domain, such as the rationals. However, searching for such interpretations is considerably more difficult than for integer polynomials. Hence, we develop new criteria to decide when to use rational instead of integer polynomial interpretations. Moreover, we present SAT-based methods for finding rational polynomial interpretations efficiently. We implemented our contributions in the termination prover AProVE, and experimental results show that both approaches lead to further increases in termination proving power.

Confluence by decreasing diagrams, converted by Vincent van Oostrom (UU)

The decreasing diagrams technique is a complete method to reduce confluence of a rewrite relation to local confluence. Whereas previous presentations have focussed on the proof the technique is correct, here we focus on applicability. We present a simple but powerful generalisation of the technique, requiring peaks to be closed only by conversions instead of valleys, which is demonstrated to further ease applicability.

slides of the talk `Confluence by decreasing diagrams, converted'