ABSTRACT
In the present paper, we develop the notion of a trace operator
on a linearly distributive category, which amounts to essentially
working within a subcategory (the "core") which has the same sort of
"type degeneracy" as a compact closed category. We also explore the
possibility that an object may have several trace structures,
introducing a notion of compatibility in this case. We show that
if we restrict to compatible classes of trace operators, an object may
have at most one trace structure (for a given tensor structure). We give
a linearly distributive version of the "geometry of interaction"
construction, and verify that we obtain a linearly distributive category
in which traces become canonical. We explore the relationship between
our notions of trace and fixpoint operators, and show that an object
admits a fixpoint combinator precisely when it admits a trace and is
a cocommutative comonoid. This generalises an observation of Hyland and
Hasegawa.
This paper is presented to Bill Lawvere on the occasion of his 60th birthday.