Feedback for linearly distributive categories: Traces and fixpoints (Q1588062): Difference between revisions

A new approach to understanding the ``geometry of interaction'' (that is, the computational aspects of cut-elimination in linear logic) is presented. Two previous categorical approaches to this problem were given by either using fixed points [\textit{S. Abramsky} and \textit{R. Jagadeesan}, Inf. Comput. 111, No. 1, 53-119 (1994; Zbl 0803.03014)] or trace operators [\textit{A. Joyal, R. Street} and \textit{D. Verity}, Math. Proc. Camb. Philos. Soc. 119, No. 3, 447-468 (1996; Zbl 0845.18005)], although both approaches were proved equivalent in that a category with a traced product is precisely a category with fixed points. In this paper, the notion of trace operator on a linearly distributive category is introduced, and the possibility that an object may have several trace structures is explored introducing a notion of compatibility. This approach to the construction of Abramsky and Jagadeesan [loc. cit.] leads to a linearly distributive category in which traces become canonical. Finally, the relationship between the notion of trace introduced in the paper, and fixpoints operators is investigated, showing that an object admits a fixpoint combinator precisely when it admits a trace and is a cocommutative comonoid.