paper

To: types@dcs.gla.ac.uk
Subject: paper
From: Dusko Pavlovic <duskop@cogs.susx.ac.uk>
Date: Sun, 7 Jul 1996 17:52:27 +0100 (BST)
Approved: types@dcs.gla.ac.uk

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Dear Types,

The following preprint of mine (to appear in MSCS) is available via

	http://www.cogs.susx.ac.uk/users/duskop/index.html

-- Dusko Pavlovic


	CATEGORICAL LOGIC OF NAMES AND ABSTRACTION
	IN ACTION CALCULI 

Abstract.

Milner's action calculus implements abstraction in monoidal
categories, so that familiar lambda-calculi can be subsumed together
with the pi-calculus and the Petri nets. Variables are generalised to
*names*: only a restricted form of substitution is allowed.

In the present paper, the well-known categorical semantics of the
lambda-calculus is generalised to the action calculus. A suitable
functional completeness theorem for symmetric monoidal categories is
proved: we determine the conditions under which the abstraction is
definable. Algebraically, the distinction between the variables and
the names boils down to the distinction between the transcendental and
the algebraic elements. The former lead to polynomial extensions, like
e.g. the ring Z[x], the latter to algebraic extensions like
Z[\sqrt{2}] or Z[i].

Building upon the work of P.~Gardner, we introduce *action
categories*, and show that they are related to the static action
calculus exacly as cartesian closed categories are related to the
lambda-calculus. Natural examples of this structure arise from
allegories and cartesian bicategories. On the other hand, the free
algebras for any commutative Moggi monad form an action category. The
general correspondence of action calculi and Moggi monads will be
worked out in a sequel to this work.