اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدWiring diagrams as normal forms for computing in symmetric monoidal categories
125
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Applications of category theory often involve symmetric monoidal categories (SMCs), in which abstract processes or operations can be composed in series and parallel. However, in 2020 there remains a dearth of computational tools for working with SMCs. We present an unbiased approach to implementing symmetric monoidal categories, based on an operad of directed, acyclic wiring diagrams. Because the interchange law and other laws of a SMC hold identically in a wiring diagram, no rewrite rules are needed to compare diagrams. We discuss the mathematics of the operad of wiring diagrams, as well as its implementation in the software package Catlab.
قيم البحث
اقرأ أيضاً
We use Luries symmetric monoidal envelope functor to give two new descriptions of $infty$-operads: as certain symmetric monoidal $infty$-categories whose underlying symmetric monoidal $infty$-groupoids are free, and as certain symmetric monoidal $inf
ty$-categories equipped with a symmetric monoidal functor to finite sets (with disjoint union as tensor product). The latter leads to a third description of $infty$-operads, as a localization of a presheaf $infty$-category, and we use this to give a simple proof of the equivalence between Luries and Barwicks models for $infty$-operads.
Milners bigraphs are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the pi-calculus and the Ambient calculus. This paper is only concerned with bigraphical syn
tax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs BBig(K), whose main features are (1) the presence of relative pushouts (RPOs), which makes them well-behaved w.r.t. bisimulations, and that (2) the so-called structural equations become equalities. Examples of the latter include, e.g., in pi and Ambient, renaming of bound variables, associativity and commutativity of parallel composition, or scope extrusion for restricted names. Also, bigraphs follow a scoping discipline ensuring that, roughly, bound variables never escape their scope. Here, we reconstruct bigraphs using a standard categorical tool: symmetric monoidal closed (SMC) theories. Our theory enforces the same scoping discipline as bigraphs, as a direct property of SMC structure. Furthermore, it elucidates the slightly mysterious status of so-called links in bigraphs. Finally, our category is also considerably larger than the category of bigraphs, notably encompassing in the same framework terms and a flexible form of higher-order contexts.
Indexed symmetric monoidal categories are an important refinement of bicategories -- this structure underlies several familiar bicategories, including the homotopy bicategory of parametrized spectra, and its equivariant and fiberwise generalizations.
In this paper, we extend existing coherence theorems to the setting of indexed symmetric monoidal categories. The most central theorem states that a large family of operations on a bicategory defined from an indexed symmetric monoidal category are all canonically isomorphic. As a part of this theorem, we introduce a rigorous graphical calculus that specifies when two such operations admit a canonical isomorphism.
A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of languages. T
he Arrow abstraction is an approximation, but we argue that it does not capture the right properties. A faithful abstraction is Symmetric Monoidal Categories (SMCs), but,so far,it hasnt been convenient to use. We show how the advent of linear typing in Haskell lets us bridge this gap. We provide a library which lets us program in SMCs with linear functions instead of SMC combinators. This considerably lowers the syntactic overhead of the EDSL to be on par with that of monadic DSLs. A remarkable feature of our library is that, contrary to previously known methods for categories, it does not use any metaprogramming.
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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
