arXiv subjects

Chad Nester

Publications and source records attributed to Chad Nester.

14 recordsLinked to original sources

arXiv2026

Override and Update in Restriction Categories

We study the override and update operators on partial functions from the perspective of restriction categories. We propose a definition of override restriction categories, in which both of the operators in question exist. We prove a number of results concerning these operators and their relationship to the structure of the ambient restriction category, as well as relating them to the existing literature on the override and update operators. We provide various examples of override restriction categories and in particular show that every classical restriction category is an override restriction category.

math.CT↗

arXiv2026

A Simple Categorical Calculus of Interacting Processes

We present a calculus that models a simple sort of process interaction. Our calculus consists of a collection of terms together with a rewrite relation, parameterised by an arbitrary multicategory whose morphisms we understand as non-interactive processes. We show that our calculus is confluent and terminating, and that terms modulo the induced convertibility relation form a virtual double category. We relate our calculus to the free cornering of a monoidal category, which is a double-categorical model of process interaction that is similar in spirit to the calculus presented herein. Precisely, we construct a functor from the virtual double category given by our calculus into the underlying virtual double category of the free cornering of the free monoidal category on the multicategory of non-interacting processes. If we think of the terms of our calculus as programs and the rewriting system as an operational semantics for these programs, this functor gives a sound denotational semantics for our calculus in terms of the free cornering.

math.CT↗

arXiv2026

Monoidal categories graded by partial commutative monoids

Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morphisms (such as the pure ones), forming a premonoidal category. This suggests seeing morphisms of an effectful category as carrying a grade that combines under the monoidal product in a partially defined manner. We axiomatize this idea with the notion of monoidal category graded by a partial commutative monoid (PCM). Monoidal categories arise as the special case of grading by the singleton PCM, and effectful categories arise from grading by a two-element PCM. Further examples include grading by powerset PCMs, modelling non-interfering parallelism for programs accessing shared resources, and grading by intervals, modelling bounded resource usage. We show that effectful categories form a coreflective subcategory of PCM-graded monoidal categories; introduce cartesian structure, recovering Freyd categories; and describe PCM-graded monoidal categories as monoids by viewing a PCM as a thin promonoidal category.

cs.LO↗

arXiv2025

A Structural Account of Combinatory Completeness

We give a general notion of combinatory completeness with respect to a faithful cartesian club and use it systematically to obtain characterisations of a number of different kinds of applicative system. Moreover, we characterise combinatory completeness of a given applicative system in terms of multicategory structure on its computable maps.

math.CT↗

arXiv2025

Dynamics and Coherence for the Free Cornering with Protocol Choice

We present a term rewriting system that models the dynamic aspects of the free cornering with protocol choice of a monoidal category, which has been proposed as a categorical model of process interaction. This term rewriting system is confluent and terminating in an appropriate sense. We use this machinery to prove a coherence theorem for the free cornering with protocol choice.

math.CT↗

arXiv2025

Resourceful Traces for Commuting Processes

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

cs.LO↗

arXiv2025

Elgot Categories and Abacus Programs

We introduce Elgot categories, a sort of distributive monoidal category with additional structure in which the partial recursive functions are representable. Moreover, we construct an initial Elgot category, the morphisms of which coincide with a lightly modified version of Lambek's abacus programs. The partial functions that are strongly representable in this initial Elgot category are precisely the partial recursive ones.

math.CT↗

arXiv2023

Protocol Choice and Iteration for the Free Cornering

We extend the free cornering of a symmetric monoidal category, a double categorical model of concurrent interaction, to support branching communication protocols and iterated communication protocols. We validate our constructions by showing that they inherit significant categorical structure from the free cornering, including that they form monoidal double categories. We also establish some elementary properties of the novel structure they contain. Further, we give a model of the free cornering in terms of strong functors and strong natural transformations, inspired by the literature on computational effects.

math.CT↗

arXiv2022

Cornering Optics

We show that the category of optics in a monoidal category arises naturally from the free cornering of that category. Further, we show that the free cornering of a monoidal category is a natural setting in which to work with comb diagrams over that category. The free cornering admits an intuitive graphical calculus, which in light of our work may be used to reason about optics and comb diagrams.

math.CT↗

arXiv2021

A Variety Theorem for Relational Universal Algebra

We develop an analogue of universal algebra in which generating symbols are interpreted as relations. We prove a variety theorem for these relational algebraic theories, in which we find that their categories of models are precisely the definable categories. The syntax of our relational algebraic theories is string-diagrammatic, and can be seen as an extension of the usual term syntax for algebraic theories.

math.CT↗

arXiv2021

Situated Transition Systems

We construct a monoidal category of open transition systems that generate material history as transitions unfold, which we call situated transition systems. The material history generated by a composite system is composed of the material history generated by each component. The construction is parameterized by a symmetric strict monoidal category, understood as a resource theory, from which material histories are drawn. We pay special attention to the case in which this category is compact closed. In particular, if we begin with a compact closed category of integers then the resulting situated transition systems can be understood as systems of double-entry bookkeeping accounts.

math.CT↗

arXiv2020

Functorial Semantics for Partial Theories

We provide a Lawvere-style definition for partial theories, extending the classical notion of equational theory by allowing partially defined operations. As in the classical case, our definition is syntactic: we use an appropriate class of string diagrams as terms. This allows for equational reasoning about the class of models defined by a partial theory. We demonstrate the expressivity of such equational theories by considering a number of examples, including partial combinatory algebras and cartesian closed categories. Moreover, despite the increase in expressivity of the syntax we retain a well-behaved notion of semantics: we show that our categories of models are precisely locally finitely presentable categories, and that free models exist.

cs.LO↗

arXiv2020

A Foundation for Ledger Structures

This paper introduces an approach to constructing ledger structures for cryptocurrency systems with basic category theory. Compositional theories of resource convertibility allow us to express the material history of virtual goods, and ownership is modelled by a free construction. Our notion of ownership admits an intuitive graphical representation through string diagrams for monoidal functors.

cs.LO↗

arXiv2020

Concurrent Process Histories and Resource Transducers

We identify the algebraic structure of the material histories generated by concurrent processes. Specifically, we extend existing categorical theories of resource convertibility to capture concurrent interaction. Our formalism admits an intuitive graphical presentation via string diagrams for proarrow equipments. We also consider certain induced categories of resource transducers, which are of independent interest due to their unusual structure.

cs.LO↗