Resourceful Traces for Commuting Processes

TL;DR

This paper introduces a new graphical framework for effectful categories by considering commuting traces as transformations, enabling better modeling of resource exchange in side-effecting computational systems.

Contribution

It presents a novel presentation of effectful categories using resourceful traces, extending the graphical calculus and constructing the commuting tensor product for free effectful categories.

Findings

New graphical calculus for effectful categories

Construction of commuting tensor product for resourceful traces

Enhanced modeling of resource exchange in effectful systems

Abstract

We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic (i.e., mere names) but transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for effectful categories (also known as generalised Freyd categories), a well-known algebraic structure in the semantics of side-effecting computation. Like the usual representation of traces as graphs, our notion of presentation gives rise to a graphical calculus for effectful categories. We use our presentations to give a construction of the commuting tensor product of free effectful categories, capturing the combination of systems in which the actions of each must commute with one another, while still permitting exchange of resources