Towards Parametric Direcursion

Johan Glimming

(University of Cambridge)

Often, denotational semantics is based on solving recursive domain
equations of mixed-variant type, such as untyped lambda calculus,
object calculi, or, languages with higher-order store. Denotational
semantics in these cases involve recursive function spaces in the
domain, and for such domains Freyd proposed a recursion scheme, called
direcursion, which allows definition and proofs for semantic elements,
as studied also in the work of Pitts. We will in this paper generalise
this mixed-variant recursion scheme and show that it can be
parameterised by an adjunction equipped with two natural
transformations that distribute the functors of the adjunction in a
certain sense over the domain constructors, generalising strength for
endofunctors to the mixed-variant situation. The new recursion scheme,
called parametric direcursion, solves the problem of maintaining
additional arguments while computing with recursive types. In addition
to constant parameterisations (c.f. Cockett et al's strong
initiality), we also deal with parameterisations where, at each
recursive step, the parameters may be modified both covariantly and
contravariantly. This amounts to what functional programmers have
termed ``accumulating parameters'' (c.f. Pardo), but here in the
context of recursive domain equations. We illustrate the applicability
of the result with some examples of parameterisations in denotational
Tuesday 17th February 2009, 14:00
Robert Recorde Room
Department of Computer Science