Paper Announcement: Control Categories and Duality

[Peter Selinger <selinger@math.lsa.umich.edu>]

Dear Category Theorists,

The paper "Control Categories and Duality: on the Categorical
Semantics of the Lambda-Mu Calculus" is now available from

 http://www.math.lsa.umich.edu/~selinger/papers.html
 http://hypatia.dcs.qmw.ac.uk/author/SelingerP

This is a revised and improved version of a paper I presented at
MFPS'98.

Let me briefly summarize the part of the paper that I think will be
the most interesting to category theorists; the actual abstract is
appended at the end.

Consider a category C with distributive finite products and coproducts
and a distinguished object R, such that all exponentials of the form
R^A exist. Let R^C denote the full subcategory of C consisting of
objects of the form R^A. It is an old observation that R^C is
cartesian-closed. This observation is at the heart of continuation
passing style (CPS) interpretations of programming languages with
control operators, and it has been used recently by Hofmann and
Streicher to give a sound and complete categorical model of Parigot's
lambda-mu calculus.  (The lambda-mu calculus generalizes the
simply-typed lambda calculus; it is a proof term calculus for
propositional classical logic).

In this paper, I give an independent, algebraic characterization of
the structure of categories of the form R^C. By "independent", I mean
that it does not depend on an ambient category C, and by "algebraic",
that it is given in terms of operations and equations only.  The
crucial structure that R^C has, besides cartesian closure, is an
operation called "classical disjunction" that takes R^A and R^B to
R^(AxB). This operation is functorial in each argument, but not
bifunctorial; it forms a premonoidal structure in the sense of Power
and Robinson. Abstracting from R^C, I define the class of "control
categories", which are cartesian-closed categories with a premonoidal
structure and suitable axioms. The presence of an operation which is
not bifunctorial leads to some interesting twists, as one has to be a
bit careful about how one defines concepts such as weak
structure-preserving functors and equivalences of categories.

The main theorem is a structure theorem, which shows that every
control category is equivalent to a category of the form R^C (and, of
course, vice versa).

An algebraic class of categories calls out for an internal language. I
prove that the call-by-name lambda-mu calculus (with product and
disjunction types) forms an internal language for control
categories. Thus, these categories can be considered as models for (a
certain kind of) proof theory of classical logic.  Also, the
call-by-value lambda-mu-calculus forms an internal language for the
dual class of co-control categories. As a consequence of this
categorical duality, it follows that there is a syntactic duality
between the call-by-name and the call-by-value calculus, i.e., there
are mutually inverse translations between call-by-name and
call-by-value that preserve the categorical (and also the operational)
semantics.  Such dualities have been observed in a different setting
by Filinski. In the case of the lambda-mu calculus, such a syntactic
duality was conjectured by Streicher and Reus.

Comments are welcome.

Best wishes, -- Peter Selinger

----------------------------------------------------------------------

ABSTRACT: 

We give a categorical semantics to the call-by-name and call-by-value
versions of Parigot's lambda-mu calculus with disjunction types. We
introduce the class of control categories, which combine a
cartesian-closed structure with a premonoidal structure in the sense
of Power and Robinson.  We prove, via a categorical structure theorem,
that the categorical semantics is equivalent to a CPS semantics in the
style of Hofmann and Streicher. We show that the call-by-name
lambda-mu calculus forms an internal language for control categories,
and that the call-by-value lambda-mu calculus forms an internal
language for the dual co-control categories. As a corollary, we obtain
a syntactic duality result: there exist syntactic translations between
call-by-name and call-by-value which are mutually inverse and which
preserve the operational semantics.  This answers a question of
Streicher and Reus.