University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Towards parametric direcursion: structured mixed-variant recursion with parameters

Towards parametric direcursion: structured mixed-variant recursion with parameters

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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