University of Birmingham > Talks@bham > Theoretical computer science seminar > Solving corecursive equations

Solving corecursive equations

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

  • UserVenanzio Capretta, University of Nottingham
  • ClockFriday 19 November 2010, 16:00-17:00
  • HouseUG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

Given some equations on a type of infinite objects, we want to determine whether there is a unique solution. The most common version of this problem is the definition of functions on streams, infinite sequences on a given type. If the equations have form that satisfies a condition called ``guardedness’’, they are guaranteed to be productive and have a unique solutions. However, there are simple equations that have unique solutions but are not guarded. Are there more general criteria to solve them? Under what conditions is the problem decidable?

I will give some examples of such equations on streams. Using standard topological methods we can determine that they have unique solutions. The challenge is to do it automatically. A powerful, although partial, technique to determine just unicity consists in computing a ``bisimulation’’. This is an equivalence relation consistent with the data structure. On coinductive types it implies extensional equality. We can use it to show that any two solutions of the equations are equal.

The general problem of determining solvability is undecidable. But it may be decided for particular classes of equations. In particular, the problem for ``pure’’ stream equations, those that don’t use the specific data element, is still open.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.