相关论文: Wiring diagrams as normal forms for computing in s…

We present a Rocq library for monoidal categories, which includes a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if they were strict, inferring MacLane isomorphims…

We introduce the wire calculus. Its dynamic features are inspired by Milner's CCS: a unary prefix operation, binary choice and a standard recursion construct. Instead of an interleaving parallel composition operator there are operators for…

Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we…

We build on the theory of ontology logs (ologs) created by Spivak and Kent, and define a notion of wiring diagrams. In this article, a wiring diagram is a finite directed labelled graph. The labels correspond to types in an olog; they can…

We explain the sense in which a warping on a monoidal category is the same as a pseudomonad on the corresponding one-object bicategory, and we describe extensions of this to the setting of skew monoidal categories: these are a…

Process theories provide a powerful framework for describing compositional structures across diverse fields, from quantum mechanics to computational linguistics. Traditionally, they have been formalized using symmetric monoidal categories…

We define a notion of symmetric monoidal closed (SMC) theory, consisting of a SMC signature augmented with equations, and describe the classifying categories of such theories in terms of proof nets.

We give a short topological proof of coherence for categorified non-symmetric operads by using the fact that the diagrams involved form the 1-skeleton of simply connected CW complexes. We also obtain a "one-step" topological proof of Mac…

Coherence theorems for covariant structures carried by a category have traditionally relied on the underlying term rewriting system of the structure being terminating and confluent. While this holds in a variety of cases, it is not a…

We introduce a new algebraic structure for multi-dimensional compositional embeddings, built on directional non-commutative monoidal operators. The core contribution of this work is this novel framework, which exhibits appealing theoretical…

An operad (this paper deals with non-symmetric operads)may be conceived as a partial algebra with a family of insertion operations, Gerstenhaber's circle-i products, which satisfy two kinds of associativity, one of them involving…

We give an alternate conception of string diagrams as labeled 1-dimensional oriented cobordisms, the operad of which we denote by Cob/O, where O is the set of string labels. The axioms of traced (symmetric monoidal) categories are fully…

We endow categories of non-symmetric operads with natural model structures. We work with no restriction on our operads and only assume the usual hypotheses for model categories with a symmetric monoidal structure. We also study categories…

We examine a variant of hypergraphs that we call interfaced linear hypergraphs, with the aim of creating a sound and complete graphical language for symmetric traced monoidal categories (STMCs) suitable for graph rewriting. In particular,…

The data for many useful bidirectional constructions in applied category theory (optics, learners, games, quantum combs) can be expressed in terms of diagrams containing "holes" or "incomplete parts", sometimes known as comb diagrams. We…

Applied category theory provides powerful mathematical tools for modelling processes and their composition. Symmetric monoidal categories, which involve series and parallel composition, are particularly well-suited for describing the…

We give a description of unital operads in a symmetric monoidal category as monoids in a monoidal category of unital $\Lambda$-sequences. This is a new variant of Kelly's old description of operads as monoids in the monoidal category of…

This paper introduces a new systematic algorithm for constructing periodic Euclidean weaving diagrams with combinatorial arguments. It is shown that such a weaving diagram can be considered as a specific type of four-regular periodic planar…

A wiring diagram is a labeled directed graph that represents an abstract concept such as a temporal process. In this article, we introduce the notion of a quasi-skeleton wiring diagram graph, and prove that quasi-skeleton wiring diagram…

We present a new model of computation, described in terms of monoidal categories. It conforms the Church-Turing Thesis, and captures the same computable functions as the standard models. It provides a succinct categorical interface to most…