Feedback for linearly distributive categories: traces and fixpoints

[摘要] 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. (C) 2000 Elsevier Science B.V. All rights reserved. MSC. 03B70; 03G30; 19D23.

[发布日期] 2000-12-01

[效力级别]  Proceedings Paper