J.W. Klop,
see also
J.W.K.'s
personal page)
with a
thesis on *proof theoretic connections between proof systems for
recursive type equivalence*. Subsequently for two-and-a-half years I was
postdoc in the same group, employed for the NWO-project "GeoProc", which
was concerned with investigating geometrical, as well as topological,
proofs in process theory. Also, I worked on
Robin Milner's process
interpretation of regular expressions.
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".

#### Productiviteit van Streamspecificaties

The text in Dutch called *Productiviteit van Streamspecificaties*,
which gives an overview about our research concerning productivity of stream definitions,
and which has been written for the periodical ``De Filosoof'' of the
association of philosophy students of Utrecht University is available as a
(doc)[MS-Word]-file.

(*My thanks* for helping with corrections of my Dutch sentences in this text go
to Dimitri Hendriks and
Vincent van Oostrom.)

[Back
to my homepage]

Clemens Grabmayer / Universiteit Utrecht /
clemens one at
phil one dot
uu one dot
nl
/
Last modified: Thu Sep 27 12:07:25 MET DST 2007