Solving corecursive equations

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

• Venanzio Capretta, University of Nottingham
• Friday 19 November 2010, 16:00-17:00
• UG40 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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.