Infinite Objects: computation, modeling and reasoning

Project code: INFINITY
Research group: Coalgebraic models of computation (SEN3.3)

Start: 2006-02-01
End: 2009-02-01

Project coordinator: Jan Rutten

We consider infinite objects, such as streams, infinite trees and terms, infinite term graphs or infinite processes. Often these exhibit a regular or cyclic nature, but we are also interested in general infinite objects. A paradigm example is the coalgebra of infinite bitstreams. Several operators can be defined on these objects, such as the operator zip that zips two streams alternatingly into one. Defining ones = 1 : one, zeros = 0 : zeros, and alt = 0 : 1 : alt, we have equations such as zip(zeros, ones) = alt. The equations holding in this coalgebra between these objects and their operators can be proved in three different ways: by coalgebraic techniques, by proof theory, and by infinitary term rewriting. These three methods have been developed up to now in isolation. This project investigates the relations between these approaches, and aims to design methods such as new proof systems to deal with the infinite objects and their equations. Issues are well-definedness criteria, completeness of the methods, decidability and implementation. Thus our project combines for infinite objects the activities of computing, modeling, and reasoning. 

Members
Frank de Boer, Clemens Kupke, Jan Rutten

Cooperation