Direct models for the computational lambda-calculus

Carsten Führmann


We give direct categorical models for the computational lambda-calculus. By `direct' I mean that the model consists of one category together with operators on objects and morphisms for modelling type and program constructors, respectively. Moggi's lambda_C-models, for example, are not direct, because the category of program denotations is constructed as the Kleisli category of a monad. We call our models `direct lambda_C-models'. The main result is, loosely speaking, that each lambda_C-model generates a direct lambda_C-model, and each direct lambda_C-model arises in this way. We shall make this precise by showing that the category of direct lambda_C-models is reflective in the category of lambda_C-models. From this we shall deduce that we can replace lambda_C-models by direct lambda_C-models without losing or gaining generality. We shall also see that the category of direct lambda_C-models is equivalent to the category of lambda_C-models that fulfil the equalizing requirement. Moreover, we shall see that we can describe our direct lambda_C-models with universally quantified equations, which helps reasoning about programs and models. Finally, we shall see that direct lambda_C-models reveal two kinds of well-behaved programs which are not obvious from lambda_C-models.


This report is available in the following formats:

Previous | Index | Next