In February I joined the Department of Philosophy in the framework of the NWO-BRICKS Project Infinity, which links our department (Albert Visser and Vincent van Oostrom are part of the research team) with two research groups in Amsterdam (Theor. Computer Science, VU, SEN-3, CWI) and which brings together three different fields: term rewriting, coalgebra, and proof theory. In this project we are interested in the precise formal treatment of infinite mathematical objects such as streams (infinite sequences) and infinite trees. Starting already last year, I have collaborated with four colleagues from the VU in work concerning the question of `productivity': How can it be recognised whether a given (finitary) stream definition does indeed evaluate to an infinite stream? This is an undecidable problem. But for a rich subclass we have found and also implemented a substantially new decision algorithm that we expect to be a useful tool for functional programming practice. Currently we work on a number of extensions of this result. As another goal I want to investigate, together with Vincent van Oostrom, ideas used for the result on productivity with the aim of developing statements clarifying the precise extent to which term graph rewriting systems can be viewed as a semantics for (finitary or infinitary) term rewriting systems.
Clemens Grabmayer for project `Infinity': We are interested in infinite mathematical objects such as infinite sequences and infinite trees. An example you can see right on top: the famous Thue Morse sequence, a stream of zeros and ones that is aperiodic, full of symmetries, and can be visualised as a beautiful mosaic.
The project links together three research groups in Amsterdam and Utrecht as well as three different fields: term rewriting, coalgebra, and proof theory.
To mention only one result: we just submitted a paper concerning the question of `productivity': How can it be recognised whether a given stream definition evaluates to a unique infinite stream? This is an undecidable problem. But for a rich subclass we have found and implemented a substantially new decision algorithm that can be useful for functional programming practice.
For more information, search "BRICKS Infinity Project".
[Back to my homepage]