Project leader: Dr. Roel de Vrijer (VU) Consortium: CWI, UU, VU Total FTE: 3.0 (heads: 3 faculty: 3, assist. prof.: 2, PD: 1) Key BRICKS publications: • H.H. Hansen, C. Kupke, and E. Pacuit. Bisimulation for Neighbourhood Structures. In: Proceedings of CALCO 2007, number 4624 in LNCS, pages 279-293. Springer, 2007. • J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, and J.W. Klop. Productivity of Stream Definitions. In: Proceedings of FCT~2007, number 4639 in LNCS, pages 274-287. Springer, 2007. • J.C.M. Baeten, F. Corradini, and C.A. Grabmayer. A Characterization of Regular Expressions Under Bisimulation. In: Journal of the ACM (volume 54, number 2), April 2007

We consider three directions of approach. One direction is Proof Theory for recursively defined objects. Another main direction is Term Rewriting, in particular infinitary term rewriting and graph rewriting. The third main direction, which has seen a vigorous development in the last decade, is that of coalgebraic techniques. We tackle the field of infinite objects with the combined force of these three methods. Our project aims to unify the three approaches, and to contribute to development of methods for guaranteeing correctness.

Coalgebra and infinite objects
Our main goal is to develop a general theory of representing "infinite objects" by finitary, coalgebraic means. A starting point is the observation that infinite objects can be described using different finite sets of operations (e.g. infinite streams can be described using{head,tail} or {head,even,odd}). In hidden algebra the notion of a cobase gives a formal criterion for when such a description is complete. We rephrased the definition of a cobase in coalgebraic terms. Our aim is to devise and study a family of co-inductive stream definition schemes that is parametric in the choice of the cobase. Furthermore our coalgebraic formulation will allow for a straightforward generalization to other infinite objects such as infinite binary trees and bi-infinite streams.

A different line of our research is concerned with investigating the semantics of modal logic using coalgebraic techniques. We studied bisimulations between neighbourhood frames and proved a Van Benthem characterization theorem for classical modal logic.

Proof theory and infinite objects
We investigate regular languages, as axiomatised by Salomaa, in a process theoretic interpretation based on bisimilarity, and tackle a famous open problem in this context posed by Milner. We also explore relations between various proof systems for cyclic objects, the classical fixed point proof systems, but also the recent coinductive proof system of Brandt-Henglein, as well as notions of circular coinductive rewriting (Goguen, Rosu, Moschovakis).

Our work on decision and recognition algorithms for productivity of stream definitions is intended to lead also to proof systems for demonstrating productivity, or non-productivity, of stream specifications by formal derivations.

Term rewriting and infinite objects
We investigate the notion of productivity for (recursive) stream definitions: a stream definition is called productive if it can be evaluated continually to build up a uniquely determined stream of which each element can be computed. While productivity is undecidable with respect to the class of all stream definitions, we show that it is decidable for two practically relevant subclasses.

We also describe a method for obtaining computable criteria for productivity and non-productivity of stream specifications that apply under the assumption that computable bounds are given for the productivion of the stream function specifications occurring.

International cooperation
In March 2006 we have organized a well-attended international symposium, resulting in active contacts with, e.g., University of Illinois, Urbana-Champaign, and the University of Leicester.

Highlights 2005-2006
As this project is part of the second phase of the BRICKS program (financed through the first open round July 2005), the project is only currently in full swing. Likewise, the number of BRICKS key publications is limited.

Research highlights

• An infinitary term rewriting system able to compute with very large ordinal numbers such as epsilon-zero and gamma-zero, in the
• A new algorithm based on infinitary rewriting to conclude \u2018productivity\u2019 of definitions of
• An in-depth 70 page study of infinitary CRSs, submitted to JACM.
• A van Benthem characterization theorem for classical modal logic.
• A computable, sufficient, and 'data-obliviously' optimal criterion for productivity that applies to a large class of stream specifications. The stream specifications in this class are based on `non-nesting' stream function specifications and employ exhaustive pattern matching on data.

Economic & societal impact
The project pursues basic research in a field that is highly relevant to innovation in information technology. For example, productivity is an important notion of correctness for functional programming; a productive program `works' and is immune to deadlocks. We believe that our decision and recognition results can provide helpful tools for functional programming practice. However, societal relevance is not easy to quantify and at present only indirectly visible in citations or other influences of the output.

Future work 2007-2009
We are currently working on an explicitation of the strong connection between infinitary rewriting with orthogonal rules, guaranteeing unique normal forms, and coalgebraic definitions of infinite objects.

For the study of productivity of stream specifications we used `pebbleflow nets' as a data-oblivious semantics for the evaluation of stream specifications. We are interested in utilizing this idea to clarify the extent to which term graph rewriting systems can be viewed as a semantics for term rewriting systems.

Concerning productivity of stream specifications, we want to explore the possibility to refine the pebbleflow semantics to account for the delay of evaluation of stream elements, in order to obtain a more genuine modelling of lazy evaluation of stream specifications.

Also we want to develop a method that goes beyond a data-oblivious analysis, i.e. one that does take into account the dependence of productivity on concrete data values of stream elements.

AFM5 Researchers funded by BRICKS

• Dr. Dimitri Hendriks (VU)
• Dr. Clemens Grabmayer (UU)
• Dr. Clemens Kupke (CWI)

For more information, please refer to the publications and posters of this project.