ISR 2010

5th International School on Rewriting

3 – 8 July 2010, Drift 21, Utrecht, Netherlands



Jörg Endrullis (VU Amsterdam, The Netherlands), Dimitri Hendriks (VU Amsterdam, The Netherlands), Clemens Grabmayer (Universiteit Utrecht, The Netherlands)


(advanced track, 2 lecture sessions)

For programming with infinite structures, productivity is what termination is for programming with finite structures. Productivity captures the intuitive notion of unlimited progress, of `working' programs producing defined values indefinitely. In functional languages, lambda-calculus, coalgebra, and in logic, use of infinite structures is common practice. For the correctness of programs dealing with such structures one must guarantee that every finite part of the infinite structure can be evaluated, that is, the specification of the infinite structure must be productive. While termination has been and still is a widely studied research subject, productivity has gained limited attention, but has been a recurrent theme in functional and dataflow programming, and in theoretical computer science.

In our course, we root the analysis of productivity firmly in the framework of term rewriting. Starting with the history of productivity, we explain its mathematical theory, sketch proofs for its undecidability and Pi-0-2-completeness, and discuss several methods for proving productivity, methods employing dataflow analysis, typing systems, etc.

We focus on productivity of programs that produce or operate on infinite streams. Streams are one of the most widely studied infinite datastructures. We describe a decision algorithm for productivity of stream specifications from a rich, syntactically defined class. The production of a specification can be calculated by translation into a dataflow net, and by simplification of the net. Apart from explaining extensions of this algorithm, and giving an overview of other, currently used methods, we also want to demonstrate to students how they can use the productivity prover ProPro to check their intuitions about productivity by experimenting with stream specifications.