Abstract

The topic of the talk is programming over infinite structures. Non-wellfounded objects can be represented and manipulated by recursive functions whose circularity is restricted in several ways. We do not yet have a satisfactory theory of what recursive definitions should be allowed and how we can reason over them. I will give an overview of the main questions that we are facing and then describe an approach to an abstract characterisation of corecursion that we are developing.

The notion of corecursive algebra characterises structures whose elements contain infinite information. Functions into them can be defined by infinite iteration of productive procedures.

On the other hand, the notion of antifounded algebra characterises structures on which we can reason by using bisimulation. It is not a surprise that this concept is more general than that of corecursive algebra: the principle of bisimulation holds also for wellfounded structures, although it is equivalent with the more manageable structural equality.

The real surprise of our research is that not all corecursive algebras are antifounded. We found a structure that satisfies the principle of corecursion but not that of bisimulation. It is constructed by exploiting a certain colouring of the edges of an infinite tree.

I will introduce and illustrate the notion and then describe our counterexample.

Work in collaboration with Tarmo Uustalu and Varmo Vene.