Abstract

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).