University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > TALK CANCELLED: An overview of structural corecursion

TALK CANCELLED: An overview of structural corecursion

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

THIS TALK HAS BEEN POSTPONED. We hope to reschedule for later in the term.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2020, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity