Rewriting modulo isotopies in pivotal linear $(2,2)$-categories
本文研究了线性~ $(2,2)$范畴中代数公理集的模改写问题。本文引入了线性$(3,2)$ -模测谎图的结构,作为线性$(2,2)$ -范畴的模代数公理重写系统的表示.我们引入了一个符号计算方法,以计算线性基的向量空间的$2$细胞的这些类别。特别是,我们使用$1$ -胞元上的双附加给出的合痕关系和$2$ -胞元上的循环条件作为公理来研究关键$2$ -范畴的情况,我们重写了模。利用这种构造性方法,我们恢复了仿射定向Brauer线性~ $(2,2)$ -范畴中的正规序点定向Brauer图的基.
2019-06-10 math.CT
Homotopy theory of stricter $n$-categories
本研究基于正则有向复形理论定义更严格$n$-范畴,推导其Gray积与纬垂稳定性等性质,构建folk模型结构并证明其与图解集模型结构的右转移关系,丰富了高维范畴同伦理论工具。
2025-09-30 math.AT math.CT
Rewriting in higher dimensional linear categories and application to the affine oriented Brauer category
本文介绍了线性幺半范畴范畴的重写理论。这些范畴是我们将定义为线性(n,p)范畴的一个特例。我们还将定义线性(n,p)-多道图,线性适应的n-多道图,目前线性(n - 1,p)-范畴。然后,我们专注于线性(3,2)-多道图给出线性幺半范畴的介绍。最后我们给出了这个理论在线性(3,2)-多道生理记录图中的应用,利用van Ostroom定义的重写性质:递减性,用一种新的方法证明了AOB范畴上的一个基定理。
2016-03-01 math.CT math.RT
Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
我们提出了一个语义置换等价的高阶重写。这种语义发生在Carnival闭2-范畴中,并被证明是合理的和完备的。
2013-09-20 cs.LO cs.PL math.CT
Representable diagrammatic sets as a model of weak higher categories
发展Kapranov和Voevodsky的想法,我们介绍了一个模型的基础上有向复合体,组合表示粘贴图的弱欧米茄范畴。我们建议这是一个方便的框架,更高的维度重写。我们定义的图形集上的一类有向复合体提出粘贴图与球形边界的预层。图集有结构面和退化运算,但没有结构复合。我们定义了一个概念的等价细胞在一个图解集,并说,一个图解集是可表示的,如果所有粘贴图与球形边界连接到单个细胞-他们的弱复合材料-由一个高维等价细胞。本文发展了可表示图集的基本理论,证明了图集的等价单元满足期望的性质。我们研究了严格ω-范畴的神经作为RDSs,证明了2-截断RDSs等价于双范畴。最后,我们连接的组合学的图解集和单纯集,并证明了一个版本的同伦假设的“groupoidal”RDS:存在一个几何实现函子的图解集,诱导同构的组合和经典的同伦群,它有一个同伦右逆。
2019-09-17 math.CT
A Constructive Proof of Coherence for Symmetric Monoidal Categories Using Rewriting
对称的幺半范畴是一个范畴,它具有一个结合的和交换的(二元)积和一个作为积的单位的对象。事实上,这些性质只适用于满足某些相干条件的自然同构。相干定理证明了所有包含左、右幺半群、结合子和辫子的线性图的交换性。利用基于重写的同伦方法证明了对称幺半范畴范畴的凝聚性。在这个范围内,我们详细介绍了拉丰的字符串图重写系统,提出了这些理论的同构的收敛性证明。
2017-07-18 math.CT
Data Structures for Topologically Sound Higher-Dimensional Diagram Rewriting
本文提出了拓扑可靠的高维图表重写模型“图表集”的计算实现,设计了任意维度图表良构形状的数据结构并解决了其同构问题,定义了相应的类型理论,并在 Python 库 rewalt 中实现了全部算法与可视化。
2023-07-31 cs.DS cs.LO math.CT
Diagrammatic Hochschild cohomology via cohomology of categories, and incidence algebras
本文通过范畴上同调与 incidence 代数的上同调研究图状 Hochschild 上同调,探讨了 Gerstenhaber-Schack 复合体与 Baues-Wirsching 猜想的联系,并计算了有限滤子 simplicial 复合物的图状 Hochschild 上同调。
2025-12-17 math.AT math.CT math.RA
An Infinitary Model of Diagrammatic Calculus in Unbiased Monoidal Categories
本文通过引入本质上抵抗同痕形变的结构,将无穷张量积和超限复合相干地引入图式形式体系,从而扩展了幺半范畴的弦图理论,构建了无穷幺半范畴模型。
2023-04-07 math.CT
Rewriting Graphically with Symmetric Traced Monoidal Categories
我们研究的超图,我们称之为接口线性超图的变体,其目的是创建一个健全的和完整的图形语言的对称跟踪幺半范畴类(STMCs)适合图重写。特别是,我们感兴趣的是重写的分类设置与笛卡尔结构,如数字电路。这些与以前的语言不兼容,其中使用紧凑的封闭或Frobenius结构来构造迹,因为将这些与笛卡儿积结合可能导致退化图。相反,我们必须考虑将跟踪构造为原子操作的方法。有界线性超图是一种正则超图,其中每个顶点都是一条边的源和目标,并带有一条额外的有界边。自由生成的STMC的态射被解释为接口的线性超图,直到同构(健全性)。此外,任何线性超图都是唯一STMC态射的表示,直到范畴的方程理论(完全性)。这建立了接口线性超图作为一个合适的组合语言STMC。然后,我们将展示如何将粘合剂类别的理论应用到我们的图形语言中,这意味着广泛的STMCs的等式属性可以指定为图形重写系统。数字电路的图形语言作为一个案例研究。
2021-03-19 math.CT
Equivalences in diagrammatic sets
本文提出图示集中的等价概念,通过合取弱可逆性定义,并开发了处理弱单位和单位子结构的方法,以区别于严格ω-范畴。
2025-12-22 math.AT math.CT
Rewriting for Symmetric Monoidal Categories with Commutative (Co)Monoid Structure
本文研究弦图重写中比完整 Frobenius 结构更弱的交换幺半群结构,并通过超图双推出重写的可靠且完备解释刻画了模去交换幺半群等式的弦图重写。
2025-01-30 cs.LO math.CT
ViCAR: Visualizing Categories with Automated Rewriting in Coq
ViCAR 是一个 Coq 库,提供幺半范畴定义、一致性验证、引理策略及字符串图可视化,支持图形化推理与自动重写。
2025-09-25 cs.PL math.CT
Diagrammatic Categories which arise from Representation Graphs
本文利用群表示图构造图示范畴,并证明在显式判据下该范畴的商范畴等价于由有限多个不可约模的张量积构成的模范畴满子范畴。
2025-02-07 math.CO math.CT math.RT
Coherence in monoidal track categories
我们引入同伦的方法重写的基础上更高的维度类别证明的一致性结果的代数结构的类别。我们将(对称)幺半范畴的连贯性问题表示为迹范畴的非球面性问题,并利用多道生理记录仪上的重写方法来解决,将其推广到更一般的连贯性问题,即迹范畴中的三维字问题,包括辫状幺半范畴的情况.
2010-12-01 math.CT
Computing Critical Pairs in 2-Dimensional Rewriting Systems
词上的重写系统在幺半群的研究中是非常有用的。在好的情况下,它们给出了幺半群的有限表示,允许计算机对其进行操作。更妙的是,当呈现是合流的和终止的时,它们为呈现幺半群的元素提供了一个规范表示的概念。测谎仪是这种呈现概念的更高维度的推广,从monoid的设置到n-范畴的更一般的设置。在这里,我们感兴趣的是证明合流的测谎仪提出2类,这可以被看作是一个概括的长期重写系统。为此,我们提出了一个适应的通常算法计算临界对。有趣的是,这个框架比术语重写系统丰富得多,需要一个新的理论框架来表示关键对,基于紧凑的2类上下文。
2010-04-19 cs.FL math.CT
Homotopies in Multiway (Non-Deterministic) Rewriting Systems as $n$-Fold Categories
我们研究抽象的多路重写系统,这是原型结构的Wolfram模型的形式主义的代数和成分属性。我们证明了存在更高的同伦在这一类的重写系统,同伦映射诱导适当的重写规则从一个抽象的规则空间的所有可能的规则。此外,我们表明,一个多路重写系统同伦顺序$n$可以自然地形式化为$n$ -折叠范畴,使(通过可逆重写关系包含适当的逆态射)的无限极限,这种结构产生一个${\infty}$ -广群。通过Grothendieck的同伦假设,这个${\infty}$ -广群因此继承了形式同伦空间的结构。最后,我们如何同伦多路系统的计算框架可能会被用于正式连接到同伦空间上的模型相关的物理可能会被实例化的一些意见。
2021-11-25 cs.DM cs.LO math-ph
Polygraphs: From Rewriting to Higher Categories
本专著以Polygraphs(多图)为统一概念,结合同伦代数视角在严格高维范畴下研究重写理论,分低维应用与高维同伦两部分,推广了代数结构连贯性结果。
2025-09-04 cs.LO math.CT
Lax Distributivity and a Characterization of Abelian Categories
Institute of Mathematics, The Czech Academy of Sciences(捷克科学院数学研究所);Institute of Mathematics, University of Technology(理工大学数学研究所)
研究阿贝尔范畴的特征,核心方法是通过余宽松代数、宽松代数及宽松混合重写规则,主要贡献是给出了阿贝尔范畴基于此的一种刻画及相关理论。
2026-07-29 math.CT
A diagrammatic approach to symmetric lenses
透镜是用于保持一对系统之间一致性的数学结构。在他们正在进行的研究计划中,Johnson和Rosebrugh试图将对称晶状体的治疗与非对称晶状体的跨度统一起来。本文通过用Mealy态射表示传播操作,给出了范畴间对称透镜的一种图解方法。本文的主要结果是通过在hom-category之间构造一个显式的伴随三元组,证明了对称透镜的双范畴与非对称透镜的跨距双范畴是局部伴随的.
2021-01-26 math.CT
Structures and Diagrammatics of Four Dimensional Topological Lattice Field Theories
Crane和Frenkel提出了三角化4-流形的状态和不变量,他们定义并使用了一种新的代数结构,称为Hopf范畴。Crane和Yetter研究了Hopf范畴,并给出了一些使用群上循环的例子,这些群上循环与有限群的Drinfeld double相关。本文利用Crane-Yetter上循环作为Boltzmann权定义了三角化四维流形的状态和不变量。我们的不变量推广了Dijkgraaf和Witten定义的三维不变量和通过霍普夫代数定义的不变量。我们提出了图解的方法来研究这种不变量,说明了霍普夫类别之间的连接和移动到三角剖分。
1998-06-05 math.CT math.GT
A Critical Pair Enumeration Algorithm for String Diagram Rewriting
Johns Hopkins University(约翰霍普金斯大学);University of Washington(华盛顿大学);University of Technology of Compiègne(贡比涅技术大学);Universidad Nacional de Córdoba(科尔多瓦国立大学);Tallinn University of Technology(塔林理工大学);University of São Paulo(圣保罗大学);National Institute of Informatics(日本国立情报学研究所);Ochanomizu University(御茶水女子大学)
本文提出了一种用于字符串图重写的自动化关键对枚举算法,适用于无弗罗贝尼乌斯结构的对称张量范畴。
2026-03-10 cs.DS math.CT
The Algebra of Open and Interconnected Systems
在这里,我们开发的范畴理论工具,理解网络风格的图形语言。典型的网络式图形语言是电路的图形语言;其他例子包括信号流图、马尔可夫过程、自动机、Petri网、化学反应网络等。其关键特征是这种语言由许多具有多个(输入/输出)终端的组件组成,每个终端可能标有某种类型,然后可以沿着这些终端连接在一起,形成一个更大的网络。这些组件在标记的顶点之间形成超边,因此这种语言的图形成超图。我们通过引入超图范畴的概念来形式化组合结构。网络风格的图解语言和它们的语义因此形成超图范畴,并且语义解释给出超图函子。本文的第一部分发展了超图范畴理论。特别是,我们介绍了装饰cospans和相关的工具。装饰cospans允许直接从图形语言中构建超图类别:输入,输出及其组成由cospans建模,而“装饰”指定组件本身。然而,并不是所有的超图范畴都可以通过修饰的余跨距来构造。装饰相关性是一个更强大的版本,它允许构造所有超图范畴和超图函子。这些通常对于从图到语义构建图形语言和函子的语义类别很有用。为了说明这些原则,本论文的第二部分详细介绍了线性时不变动力系统和无源线性网络的应用。
2016-09-17 math.CT
Rewriting techniques for relative coherence
该研究拓展代数结构相干性的重写证明方法,覆盖部分相干性与笛卡尔结构两类情形,构建抽象及项重写系统层面的重写技术与定理,可推导幺半范畴等的相干定理。
2025-07-23 math.CT
Left-Linear Rewriting in Adhesive Categories
本文研究粘合范畴中左线性重写规则的因果独立性问题,提出新的独立性刻画,识别良态重写系统类别,并证明Church-Rosser性质及规范等价证明的存在性,扩展了粘合框架可建模的形式化体系范围。
2024-07-08 cs.LO math.CT math.LO
Rewriting Modulo Traced Comonoid Structure
本文提出了一种基于迹余幺半群结构的图重写方法,用于描述具有延迟和反馈的顺序电路等式理论。
2026-01-01 cs.LO math.CT
The diagrammatic presentation of equations in categories
本文定义了精确表示“同解”的范畴图等价,并证明图范畴沿该等价的局部化与切片范畴沿初始函子的局部化同构,且推广至局部可展示 2-范畴。
2024-01-22 math.CT
Identities among relations for higher-dimensional rewriting systems
我们推广的概念之间的关系,众所周知的介绍组,介绍n-类别的测谎仪的身份。每个测谎仪,我们关联一个轨道n-类,广义的概念,交叉模块组,以定义关系之间的身份的自然系统。我们涉及的事实,这个自然系统是非线性生成的,测谎仪有有限的推导类型。
2010-04-07 math.AT math.CT math.KT
Surface Diagrams for Frobenius Algebras and Frobenius-Schur Indicators in Grothendieck-Verdier Categories
该研究为Grothendieck-Verdier范畴建立三维曲面图演算,推广刚性幺半范畴的Frobenius代数性质,引入高阶Frobenius-Schur示性数并证明其等价不变性,配套提供图形证明助手辅助文件。
2025-05-19 math.CT math.QA
Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing
这项工作是关于图形语言,它们如何被表示,以及它们反过来可以用来表示什么。更具体地说,它侧重于字符串图的表示和应用。字符串图用于表示一组进程,用“盒子”表示,带有多个(类型化的)输入和输出,用“线”表示。如果我们允许将输入和输出连接在一起,我们就可以直观地表示过程的复杂组合,形式化为幺半范畴中的态射。[...]本论文的第一个主要贡献是介绍了一个离散版本的字符串图称为字符串图。字符串图形成了一个部分粘合类别,因此可以使用双推出图重写来操纵它们。此外,我们展示了如何字符串图模重写系统可以用来构建免费的对称跟踪和紧凑的闭范畴monoidal签名。第二个贡献是图形语言在量子信息论中的应用。我们使用的混合物的图解和代数技术证明一个新的分类结果强互补的可观。[...]我们还介绍了一个图形语言的多体纠缠,并说明了一个简单的图形公理,区分两个最大纠缠的三方量子比特状态:GHZ和W。[...]第三个贡献是作者开发的两个软件工具的描述,以实现这里描述的大部分理论内容。第一个工具是Quantity,这是一个桌面应用程序,用于构建字符串图和图形理论,以及可视化地执行自动图形重写。第二个是QuantoCoSy,它使用一种称为猜想合成的程序来执行完全自动化的模型驱动理论创建。
2012-03-22 cs.AI math.CT quant-ph
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Monoidal代数结构由可以具有多个输出以及多个输入的操作组成,其在许多领域中具有应用,包括范畴代数、程序设计语言语义、表示论、代数量子信息和量子群。字符串图提供了一种方便的图形语法,用于正式推理这种结构,同时避免了基于术语的方法的许多技术挑战。Quantification是一个工具,支持使用字符串图(半)自动构造等式证明。我们简要地概述了Quantity的重写引擎的理论基础,然后给出了一个概述的核心功能和架构,并给出了一个简单的例子项目,计算交换双代数的范式。
2015-10-13 cs.LO cs.MS math.CT
String Diagrammatic Trace Theory
本文将幺半范畴中的形式语言理论扩展至多类对称情形,通过引入对称幺半自动机统一了 Mazurkiewicz 迹语言与 Zielonka 异步自动机,并利用字符串图推导迹的串行化。
2023-06-28 cs.FL math.CT
Diagrammatic Differentiation for Quantum Machine Learning
Department of Computer Science, University of Oxford(牛津大学计算机科学系);Cambridge Quantum Computing Ltd.(Cambridge Quantum Computing Ltd.(剑桥量子计算有限公司))
我们介绍了张量微积分的图解微分一般化的对偶数建设从钻机monoidal类别。应用这ZX图,我们展示了如何计算图解的梯度的线性映射相对于一个相位参数。对于参数化的量子线路,我们在许多变分量子算法的基础上得到了著名的参数移动规则。然后,我们将我们的方法扩展到混合经典量子线路的自动微分,使用气泡图来编码任意非线性算子。此外,图表差异化在DisCoPy(monoidal categories的Python库)中有一个开源实现。经典量子线路的图形梯度可以使用PyZX库简化,并通过tket编译器在量子硬件上执行。这为利用弦图的结构和量子机器学习的计算能力的许多实际应用打开了大门。
2021-09-18 cs.LG math.CT quant-ph
String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
弦图是一种强大而直观的图形语法,起源于对对称monoidal范畴的研究。在过去的几年中,它们已经在各种计算结构的建模中得到应用,在计算机科学、物理学、控制理论、语言学和生物学等领域。在许多这样的提议中,所描述的系统的转换被建模为图的重写规则。这些发展需要弦图重写的数学基础:尽管术语的重写理论是很好理解的,但弦图的二维性质带来了额外的挑战。这项工作系统化和扩展了一系列最近的会议论文奠定了这样的基础。作为第一步,我们专注于重写系统的情况下,具有Frobenius代数的弦图解理论。这种情况普遍存在于各种方法中:例如,在线性动力系统的代数语义中,弗罗贝纽斯结构模拟电路的布线;在分类量子力学中,它们模拟相互作用的量子可观测量。我们的工作介绍了一个组合的解释弦图重写模Frobenius结构,在双推出超图重写。此外,我们证明了这种解释是健全的和完整的。在最后一部分中,我们还看到,该方法可以推广到模型重写模多个Frobenius结构。作为概念的证明,我们展示了如何从这些结果中得出一个终止策略的相互作用双代数,一个重要的重写理论在量子电路和信号流图的研究。
2022-02-03 cs.LO math.CT
Higher-dimensional categories with finite derivation type
我们研究收敛(终止和合流)表示的n-范畴。利用测谎仪(或computad)的概念,我们介绍了同伦性质的有限导子类型的n-范畴,推广了一个由Squier介绍的词重写系统。我们通过使用临界分支的概念来刻画此属性。特别地,我们定义了n-范畴具有有限导子型的充分条件。通过实例,我们提出了几种基于2-范畴导子的3-多道生理记录仪收敛表示的研究方法。
2009-10-20 math.AT math.CT math.KT
Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
本文为e-graph给出半格富集笛卡尔范畴的范畴论语义,将其推广至幺半范畴,提出e-hypergraph作为态射的可靠完备组合表示,并实现了适用于这类结构的DPO重写。
2025-05-20 cs.LO math.CT
Rule Algebras for Adhesive Categories
本文证明双推重写在黏合范畴中沿重叠的规则顺序组合具有自然结合性,并定义了规则代数,在具有初始对象时得到单位代数,为随机DPO重写系统中统计矩的计算提供了规范表示。
2020-07-02 cs.DM cs.LO math.CO
Rewriting modulo symmetric monoidal structure
对于对称幺半范畴范畴(SMC)的术语,弦图是一种强大而直观的图形语法。它们在计算机科学中有许多应用,并且在其他领域,如物理学和控制理论中变得越来越相关。在许多这样的方法中,一个重要的角色是由图的方程理论,通常作为重写规则定向和应用。本文对这种形式的改写作了全面的论述。我们解释图组合类型超图,并建立精确的对应关系图重写模的SMCs的法律,一方面和双推出(DPO)重写的超图,受一个健全的条件称为凸性,另一方面。这一结果依赖于一个更一般的特征定理,在其中,我们表明,类型超图DPO重写相当于图重写模的SMCs的法律选择一个特殊的Frobenius结构。我们说明了我们的方法与终止的非交换双积分理论的证明。
2016-02-23 cs.LO math.CT
Some notes on diagram chasing and diagrammatic proofs in category theory
图追踪是范畴论和同调代数中常用的证明方法。它涉及到元素理论的方法,以显示某些属性举行的交换图表。当第一次处理阿贝尔范畴时,人们可以使用图解方法而不依赖于元素的概念。然而,不断地操纵各种图的泛性质可能相当麻烦。也就是说,我们认为,为了推动范畴论的发展,在两种观点之间进行对比仍然是重要的。我们把我们的范围集中在短五引理,更基本的图引理之一,并提出了一个快速的相关主题的阐述。此外,我们利用拉回的泛性质对短五引理给出了一个新颖的证明。
2020-10-28 math.CT
Lax monoidality for products of enriched higher categories
本文证明松弛 $\mathbb{E}_{n+1}$-幺半函子可诱导富集 $\infty$-范畴间的松弛 $\mathbb{E}_n$-幺半函子,并基于 Boardman--Vogt 张量积给出将图示构造推广至 $\mathcal{O}$-幺半范畴的准则。
2023-05-24 math.AT math.CT
(Op)lax natural transformations, twisted quantum field theories, and "even higher" Morita categories
在高阶范畴的背景下定义扭曲的量子场论的挑战的动机,我们开发了一个一般的框架宽松和oplax变换和它们的更高的类似物之间的强$(\infty, n)$ -函子。我们构造了一个双$(\infty,n)$ -范畴,它是由控制所需语义的目标$(\infty, n)$ -范畴构建的。我们定义(op)lax变换为函子到它的部分,并且(op)lax扭曲场论是域论之间的对称monoidal(op)lax自然变换。证明了松弛平凡扭曲相对域论与绝对域论是相同的。作为第二个应用,我们利用$\mathcal{C}$中的高阶态射将对称Monoidal $(\infty, n)$范畴$\mathcal{C}$中的$E_d$ -代数的高阶Morita范畴推广到$(\infty, n+d)$ -范畴.
2016-01-26 math.AT math.CT
A new criterion for $\mathcal{M}, \mathcal{N}$-adhesivity, with an application to hierarchical graphs
粘着范畴为重写理论的代数方法提供了一个抽象的框架,其中许多一般性的结果可以被改写和统一证明。然而,检查模型是否满足粘附性属性有时远非立即。在本文中,我们提出了一个新的标准给出了一个充分条件$\mathcal{M}, \mathcal{N}$ -adhesivity,原来的概念的adhesivity的推广。我们将其应用到几个现有的类别,特别是层次图,一种形式主义,是出了名的难以适应的模具代数方法重写和各种替代的定义浮动。
2022-06-15 cs.LO math.CT math.LO
Super rewriting theory and nondegeneracy of odd categorified sl(2)
本文将高维重写理论推广到超范畴,建立幺半超范畴与2-超范畴的重写工具,并借此证明量子 sl(2) 奇范畴化的非退化猜想,进而给出奇2-范畴上 dg-结构的分类。
2021-01-30 math.CT math.QA math.RT
String Diagrams For Double Categories and Equipments
幺半范畴的一个流行的图形演算使得计算变得直观和有触觉。复杂的图表追逐可以在几张图片中表达,并通过玩鞋带发现。Joyal和Street对这种演算的可靠性的证明说,图的任何变形,弦的任何弯曲,都描述了相同的态射。本文将图演算推广到双范畴和前向设备上,将弦图解方法引入形式范畴论。我们的主要定理证明了这种微积分声音的帮助道森和帕雷的结果组成的双重类别。
2018-03-02 math.CT
Diagrammatic category theory
本文提出用弦图直观表示范畴论基本概念(如泛性质、极限、Kan扩张等)的证明,并介绍计算(余)端的方法,帮助初学者直观理解范畴论基础。
2024-07-18 math.CT
Cubical coherent confluence, $ω$-groupoids and the cube equation
本文提出立方收缩和立方多面体解析,通过拼接立方相干单元证明了新曼引理、丘奇-罗斯塞尔定理和斯皮尔定理,并推导了立方定律,展示了收敛重写系统生成无环立方群oid的性质。
2025-12-10 cs.LO math.CT
String Diagrams for Closed Symmetric Monoidal Categories
本文提出了一种基于扩展字符串图的图形语言,用于闭合对称单调oidal范畴,通过括号线显式表示内部同态,并通过示例展示了其在范畴论、逻辑和编程语言语义中的应用。
2025-12-06 cs.LO math.CT
Interacting Monoidal Structures with Applications in Computing
本文在$n$重幺半范畴中定义$n$重幺半群与余幺半群对象,给出通信协议及布尔半环模代数等实例,服务于并发理论与更高维重写。
2024-11-06 cs.LO math.CT
UC, Categorically: Rigorous Diagrammatic Proofs
Input Output;University College London(伦敦大学学院);University of Bath(巴斯大学);University of Edinburgh(爱丁堡大学)
本文运用范畴论的字符串图技术,对静态系统的通用可组合性(UC)框架进行严谨的范畴论处理,扩展其适用范围并修正疏漏,同时保持等价性与表达能力。
2026-08-06 cs.CR cs.LO math.CT
Higher-dimensional subdiagram matching
本文研究高维图重写中的子图匹配问题,在 diagrammatic sets 框架下提出任意维度的匹配算法,并证明在无环性条件下可将超多项式复杂度改进为多项式复杂度,同时分析了维度 4 的困难。
2023-04-18 cs.DS cs.LO math.CT
Programs as Diagrams: From Categorical Computability to Computable Categories
这是一本教科书/专著的草稿,使用弦图介绍了可计算性理论。介绍性章节已经作为研究生和本科生课程讲授,并通过8年的课堂讲稿演变。后面的章节包含新的想法和结果有关范畴的可计算性和一些第一步到可计算范畴理论。计算的基本范畴观是基于具有程序求值器的monoidal范畴,称为 *monoidal计算机 *。这种分类结构可以看作是一种称为Run的单指令图形化程序设计语言,其唯一的指令称为RUN。这个版本:改进了文本,将最后一章移至下一卷。(The最终版本将继续大量的练习和锻炼,但这个版本已经严重退化的图形,以满足大小界限。)
2023-03-28 cs.LO math.CT
Collages of String Diagrams
该研究提出弦图拼贴作为粘合多个幺半范畴的图示语法,将其解释为带基点的双模profunctor,并给出了双模范畴、函子盒及内部图的弦图三类应用示例。
2023-12-14 cs.LO math.CT