Towards parametric direcursion: structured mixed-variant recursion with parameters

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

• Johan Glimming (Visiting Research Fellow, University of Cambridge)
• Monday 18 May 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

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

I will speak about Freyd’s universal property generalising that of initial algebras and final coalgebras. This property, termed direcursion, appears to be useful in programming language semantics. For example, typical models of untyped lambda calculus and of object-based programming languages come equipped with this property. Recent work on higher-order store have used recursive domain equations giving rise to the same property. We here begin to develop a new reasoning principle with an aim to allow both constant and modifiable (accumulating) parameters. In the case of initial algebras, it is known (at least) since work by Cockett et al that strong functors, i.e. functors equipped with a natural transformation distributing a product over the endofunctor, give rise to a parametric version of iteration in a cartesian closed category. We therefore ask how the situation generalises to mixed-variant bifunctors and direcursion, and what universal property arises in this more general circumstance. It turns out that we require a generalisation of strength, called distrength, in addition to monoidal closed structure. Existence and uniqueness of solutions are demonstrated for the scheme, under these assumptions, by asymmetrically reducing the scheme back to Freyd’s work using the unit/counit of the assumed adjunction. Current work will be mentioned, including the endeavour to express normalisation-by-evaluation by means of this generalised recursion scheme (parametric direcursion).

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.