# 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

semantics.

**Tuesday 17th February 2009, 14:00**

Robert Recorde Room

Department of Computer Science