Functor String Diagrams: A Novel Approach to Flexible Diagrams for Applied Category Theory
本文提出函子弦图方法，解决传统幺半弦图无法准确表示函子等范畴构造的问题，并通过证明Yoneda引理和支撑神经电路图验证其理论与应用价值。
2024-06-26 math.CT
The Bénabou-Roubaud theorem via string diagrams
Mathematical Institute, Serbian Academy of Sciences and Arts（塞尔维亚科学与艺术协会数学研究所）
本文通过弦图证明了Bénabou-Roubaud定理，将单子与Grothendieck的降观点联系起来，等价于Janelidze和Tholen的特征化。
2026-01-12 math.CT
String Diagrams For Double Categories and Equipments
幺半范畴的一个流行的图形演算使得计算变得直观和有触觉。复杂的图表追逐可以在几张图片中表达，并通过玩鞋带发现。Joyal和Street对这种演算的可靠性的证明说，图的任何变形，弦的任何弯曲，都描述了相同的态射。本文将图演算推广到双范畴和前向设备上，将弦图解方法引入形式范畴论。我们的主要定理证明了这种微积分声音的帮助道森和帕雷的结果组成的双重类别。
2018-03-02 math.CT
String Diagrams for Optics
光学是用于组合数据访问的数据表示，透镜是一种流行的特殊情况。赫奇斯提出了一个透镜的图解演算，但在某种程度上，并没有推广到其他类别的光学。我们提出了一个演算，适用于所有的光学，而不仅仅是镜头，这是通过嵌入光学到他们的预层类别，自然功能字符串图。我们应用我们的演算的镜头的共同情况下，将其扩展到有效的镜头，并探讨如何在这种设置的法律的光学表现。
2020-05-12 math.CT
Context-Free Languages of String Diagrams
该研究定义幺半范畴中字符串图的上下文无关语言，统一词、树和超图的经典情形，并借助轮廓拼接伴随证明其可由正则语言经幺半函子表示。
2024-04-16 cs.FL math.CT
The Cost of Compositionality: A High-Performance Implementation of String Diagram Composition
字符串图是一种越来越流行的代数语言，用于分析不同研究领域的图形计算模型。而字符串图已被彻底研究的语义结构，少得多的关注已给予他们的算法属性，和有效的实现图形推理几乎是一个未探索的主题。这项工作旨在为这一方向做出贡献。我们介绍了一种数据结构表示字符串图的邻接矩阵。这种编码的主要优点是为图的合成和张量积提供了简单有效的算法。我们证明了它的有效性，表明这两个操作的复杂性是线性的字符串图的大小。此外，由于我们的方法是基于基本的线性代数运算，我们可以利用高度优化的实现，我们使用它来衡量性能的字符串图形操作通过几个基准。
2022-11-03 cs.PL math.CT
String diagrams for Strictification and Coherence
本文提出非严格幺半范畴弦图的生成元与关系表示，证明其正确性，并由此给出Mac Lane严格性定理与相干性定理的新图形证明，支持数字电路与编程语言等应用。
2024-10-28 math.CT
Promonads and String Diagrams for Effectful Categories
本文通过自由添加对象的幺半范畴弦图为有效范畴构造弦图，并证明有效范畴是promonad幺半双范畴中的伪幺半对象。
2024-05-01 cs.LO math.CT
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
Hybrid Quantum-Classical Machine Learning with String Diagrams
本文提出用带函子盒的弦图形式化描述混合量子-经典算法，通过松弛幺半函子刻画量子-经典接口与测量限制，为混合量子机器学习建立捕捉量子-经典交互特征的指称语义基础。
2024-07-04 math.CT quant-ph
String diagrams and categorification
这些是在2018年6月的量子仿射代数与集群代数，当前代数和分类的相互作用会议上给出的迷你课程的讲义。目标是向读者介绍幺半范畴的弦图技术，并强调它们在分类中的作用。
2019-05-02 math.CT math.RT
Tapes as Stochastic Matrices of String Diagrams
University of Pisa（比萨大学）
本文研究了子分布单子下的绳状图与随机矩阵的同构性，并利用该结果对概率布尔电路进行了公理化描述。
2026-01-04 cs.LO math.CT
String Diagrams for Closed Symmetric Monoidal Categories
Tallinn University of Technology（塔林理工大学）
本文提出了一种基于扩展字符串图的图形语言，用于闭合对称单调oidal范畴，通过括号线显式表示内部同态，并通过示例展示了其在范畴论、逻辑和编程语言语义中的应用。
2025-12-06 cs.LO math.CT
A layout algorithm for higher-dimensional string diagrams
本文提出了一种用于高维弦图的布局算法，通过引入新的范畴论工具 injectification 在有限偏序集范畴中递归生成几何元素的线性约束，并作为布局引擎在证明助手 homotopy.io 中实现了复杂高阶范畴对象的实用可视化。
2024-02-20 math.CT
Sheet diagrams for bimonoidal categories
双单子范畴（Bimonoidal categories）是具有两个单子结构的范畴，其中一个分布在另一个之上。我们正式定义了片图，一个图形演算的bimonoidal类别，是非正式介绍了Staton。片状图是在分支表面上绘制的字符串图，分支表面本身是一个拉伸字符串图。我们的主要结果是一个健全性和完备性定理的通常形式的图形演算：我们表明，表图形式的自由双单类的签名。
2020-12-19 math.CT
Rendering string diagrams recursively
本文提出通过折叠字符串图的顺序与并行组合代数表示递归计算布局，以二叉空间划分树维护右梯形轮廓不变量，并给出基于 Haskell 和 Diagrams 的实现及矩阵代数编译示例。
2024-04-03 cs.CG math.CT
Diagrammatic category theory
本文提出用弦图直观表示范畴论基本概念（如泛性质、极限、Kan扩张等）的证明，并介绍计算（余）端的方法，帮助初学者直观理解范畴论基础。
2024-07-18 math.CT
String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
弦图是一种强大而直观的图形语法，起源于对对称monoidal范畴的研究。在过去的几年中，它们已经在各种计算结构的建模中得到应用，在计算机科学、物理学、控制理论、语言学和生物学等领域。在许多这样的提议中，所描述的系统的转换被建模为图的重写规则。这些发展需要弦图重写的数学基础：尽管术语的重写理论是很好理解的，但弦图的二维性质带来了额外的挑战。这项工作系统化和扩展了一系列最近的会议论文奠定了这样的基础。作为第一步，我们专注于重写系统的情况下，具有Frobenius代数的弦图解理论。这种情况普遍存在于各种方法中：例如，在线性动力系统的代数语义中，弗罗贝纽斯结构模拟电路的布线;在分类量子力学中，它们模拟相互作用的量子可观测量。我们的工作介绍了一个组合的解释弦图重写模Frobenius结构，在双推出超图重写。此外，我们证明了这种解释是健全的和完整的。在最后一部分中，我们还看到，该方法可以推广到模型重写模多个Frobenius结构。作为概念的证明，我们展示了如何从这些结果中得出一个终止策略的相互作用双代数，一个重要的重写理论在量子电路和信号流图的研究。
2022-02-03 cs.LO math.CT
A first-order logic for string diagrams
用弦图进行方程推理提供了一种直观的方法来证明对称幺半范畴中态射之间的方程。这可以扩展到使用一个简单的图形语法来证明无限族的方程，称为！-方框符号虽然这确实大大增加了字符串图的证明能力，但以前超越等式推理的尝试在很大程度上是临时的，因为缺乏合适的逻辑框架来进行涉及！箱.在本文中，我们将等式推理扩展为！框到一个完全成熟的一阶逻辑，称为连接，含义和全称量化！-箱.这个逻辑，叫做！L，则足够丰富以适当地形式化归纳原理，箱.然后我们建立一个标准模型！并给出一个非交换双代数的定理的例子证明！L，这是无法通过等式推理单独获得的。
2015-05-02 cs.LO math.CT
String diagrams for traced and compact categories are oriented 1-cobordisms
我们给出了另一种概念的字符串图标记为1-维定向配边，我们表示的操作数的Cob/O，其中O是一组字符串标签。追踪（对称monoidal）范畴的公理完全由Cob/O编码，在这个意义上，对于不同的O，（Cob/O）-代数与具有不同对象集的追踪范畴之间存在等价性。这同样适用于紧（闭）范畴，区别在于O的方差。作为我们的主要定理的结果，我们仅仅根据monoidal范畴和紧范畴的特征给出了迹范畴的2-范畴的特征，而不涉及迹范畴的通常结构或公理。在附录中，我们给出了一个完整的证明，证明了具有强monoidal函子的幺半范畴范畴的2-范畴与其对象集是自由的具有严格函子的幺半范畴范畴的2-范畴之间的关系;对于跟踪范畴和紧范畴也是如此。
2016-09-19 math.CT
Equational reasoning with context-free families of string diagrams
字符串图提供了一种直观的语言，以图形方式表达相互作用的进程网络。弦图的离散表示，称为弦图，允许通过双推出重写进行机械化等式推理。然而，人们往往希望表达的不仅仅是单个方程，而是任意大小的图之间的整个方程族。为了做到这一点，我们定义了一类上下文无关文法，称为B-ESG文法，它适用于定义整个系列的字符串图，至关重要的是，字符串图重写规则。我们表明，这些语法的语言成员资格和匹配枚举问题是可判定的，因此，有一个算法重写字符串图根据B-ESG重写模式。我们还表明，它是可能的原因，在语法的水平，通过提供一个简单的方法，转换语法的字符串图重写，并显示受理的诱导B-ESG重写模式。
2015-10-13 cs.FL cs.LO math.CT
Graded String Diagrams for Imprecise Probability and Causal Intervention
University College London（伦敦大学学院）
本文提出了一种基于梯度字符串图的方法，用于建模不精确概率和因果干预，通过公理化呈现和案例研究展示了其应用。
2026-01-08 cs.LO math.CT
Quantitative Monoidal Algebra: Axiomatising Distance with String Diagrams
本文为弦图演算开发定量框架，在幺半范畴设定下通过 quantale 丰富化公理化弦图间距离，并应用于概率与线性系统分析。
2025-06-27 cs.LO math.CT
Category Theory Using String Diagrams
Fokkinga和Meertens的工作发展了一种计算方法来研究范畴论。该方案有许多优点，但在向等式推理风格的转变中牺牲了有用的类型信息。与之相比，传统的图粘贴证明保留了重要的类型信息，但很难表达分类证明的推理和发展。为了结合这两种观点的优势，我们建议使用字符串图，在范畴论社区的共同民俗，使我们能够保留类型信息，同时追求计算形式的证明。这些图形表示提供了一个拓扑的角度对分类证明，并默默地处理函性和自然条件，需要笨拙的簿记在更传统的符号。我们的方法主要是通过例子来进行，系统地将图形技术应用于范畴论的许多方面。我们开发了许多常见概念的字符串图解公式，包括双列，单子，Kan扩展，限制和colimits。我们描述可表示的函子图形化，并利用这些作为一个统一的源图形计算规则的许多范畴理论的概念。这些图形工具，然后用来明确证明许多标准的结果，在我们提出的图解风格。
2014-11-09 cs.LO math.CT
String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure
对称monoidal理论（SMTs）以一种使它们适合表达资源敏感系统的方式概括了代数理论，其中变量不能随意复制或丢弃。在SMT中，传统的树状术语被弦图所取代，弦图是一种拓扑实体，可以直观地认为是电线和盒子的图。最近，弦图作为一种图形语法越来越受欢迎，可以在不同的领域推理计算模型，包括程序设计语言语义学、电路理论、量子力学、语言学和控制理论。在应用中，通常将SMT中出现的方程实现为重写规则是方便的。这就提出了挑战，延长传统的长期重写理论，这已经发展为代数理论，弦图。在本文中，我们开发了一个数学理论的串图改写SMT。我们的方法利用了在本系列的第一篇论文中介绍的某些图的弦图重写和双推出（DPO）重写之间的对应关系。只有当SMT包含Frobenius代数结构时，这种对应才是合理的。在目前的工作中，我们将展示如何建立一个类似的对应任意SMT，一旦一个适当的概念DPO重写（我们称之为凸）被确定。作为概念证明，我们使用我们的方法来显示两个感兴趣的SMT的终止：Frobenius半代数和双代数。
2022-09-14 cs.LO math.CT math.LO
Data-Parallel Algorithms for String Diagrams
本文提出以ACSet结构化余跨度表示字符串图的数据并行算法，支持多种图操作，可映射为光学图，还实现了基于反向导数的梯度学习器符号计算，适用于多类硬件与语言场景。
2023-05-01 cs.PL math.CT
Bialgebraic Semantics for String Diagrams
图里和普洛特金的双代数语义是一种抽象的方法来指定一个系统的操作语义，通过它的语法（编码为单子）和它的动态（内函子）之间的分配律。这种设置有助于表明语义规范（余代数）满足期望的性质：特别是，它是合成的。在这项工作中，我们使用双代数方法来推导出字符串图的行为良好的结构性操作语义，这是一种越来越多地用于不同学科交互系统研究的图形语法。我们的分析依赖于代表二维操作的基础上弦图在各种类别作为一个单子，和他们的双代数语义的分配法在单子。作为一个概念的证明，我们提供了一个多功能的字符串图形语言，已被用来模拟信号流图（控制理论）和Petri网（并发理论）的双代数组成语义。此外，我们的方法揭示了两种不同的解释Frobenius方程的字符串图和两个同步机制的过程中，à la Hoare和à la米尔纳之间的对应关系。
2019-07-02 cs.LO cs.PL math.CT
Causal Inference by String Diagram Surgery
Radboud University（拉德堡德大学）；University College London（伦敦大学学院）
从观察到的相关性中提取因果关系是概率推理中一个不断发展的领域，起源于20世纪90年代初Pearl等人的开创性工作。本文开发了一个新的，面向分类的观点的基础上，明确区分语法（字符串图）和语义（随机矩阵），连接通过解释结构保持函子。识别因果效应的一个关键概念是干预，即一个变量被强制设置为一个特定的值，而不依赖于任何先前的倾向。我们表示这样的干预作为一个endofunctor的效果，执行“字符串图手术”的语法范畴内的字符串图。该图手术反过来又通过解释函子产生新的介入分布。虽然在一般情况下，没有办法纯粹从观察到的数据计算干预分布，我们表明，这是可能的，在某些特殊情况下，使用计算工具称为梳解体。我们展示了使用这种技术的一个著名的玩具的例子，在那里我们预测的因果关系吸烟对癌症的存在一个混淆的共同原因。开发这个具体的例子后，我们表明这种技术提供了简单的充分条件，计算干预措施，适用于各种情况下考虑的因果推理文献。
2019-07-28 cs.LG cs.LO math.CT
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
线性/非线性（LNL）模型，如Benton所描述的，合理地建模了与直觉线性逻辑密切相关的LNL项演算和LNL逻辑。每一个这样的模型诱导一个典型的丰富，我们显示健全模型的LNL λ演算弦图，介绍了里奥斯和塞林格（主要应用于量子计算）。我们对这种语言的抽象处理导致了比迄今为止提出的更简单的具体模型。我们还扩展了一般递归的语言，并证明合理性。最后，我们提出了一个充分的结果，对应于修改后的版本的本顿和Wadler的伴随演算与递归的语言的无干扰片段。
2018-04-25 cs.LO cs.PL math.CT
String Diagrams for Layered Explanations
本文提出一个基于分层 props 图形演算的范畴框架，统一解释系统生物学、电路理论和并发领域的模型，支持多精度层级呈现与部分解释，并为反事实模型的形式化推理奠定基础。
2023-07-31 cs.LO math.CT
Weakening and Iterating Laws using String Diagrams
本文用字符串图将迭代组合的结合性推广到三个单子的弱分配律，并给出新示例。
2023-02-20 cs.LO math.CT
Active Inference in String Diagrams: A Categorical Account of Predictive Processing and Free Energy
Quantinuum（昆蒂努姆）；Association for Mathematical Consciousness Science（数学意识科学协会）；Ludwig Maximilian University of Munich（慕尼黑路德维希-马克西米利安大学）；University of Bamberg（班贝格大学）；Topos Institute（托波斯研究所）；VERSES Research（VERSES研究院）
本文用字符串图与幺半范畴理论形式化预测处理与主动推断框架，图示推导了基于自由能最小化的主动推断公式，并证明自由能的组合性属性，为该领域提供了图形语言与简洁介绍。
2023-08-01 cs.AI cs.LO math.CT
String diagrams for game theory
本文提出了一个monoidal范畴，其态射是游戏（在博弈论的意义上，而不是游戏语义）和相关的图形语言。monoidal范畴的两个基本运算，即范畴合成和张量积，大致对应于游戏的顺序和同时合成。这导致了一个合成理论，在这个理论中，我们可以根据组成部分的相应属性来推理游戏的属性。特别是，我们给出了一个定义的纳什均衡，这是递归的因果结构的游戏。本文的关键技术思想是紧密基于博弈论中选择函数的应用，使用连续传球风格来推理球员选择的未来后果。此外，干净的分类基础为泛化提供了许多机会，例如学习代理。
2015-03-20 cs.GT cs.LO math.CT
Monoidal computer II: Normal complexity by string diagrams
在Monoidal Computer I中，我们引入了一个计算的范畴模型，其中关于可计算性的形式化推理由简单而流行的字符串图图形语言支持。在本文中，我们改进和扩展的计算模型，以支持正式的复杂性理论。这种形式化带来了前景的概念，正常的复杂性措施，它允许分解类似于克莱因的范式。这样的度量方法恰恰是那些评估程序复杂性并不需要比评估程序本身更多的资源的度量方法。因此，通常的时间和空间复杂度是正常的度量，而平均和随机复杂度度量不是。虽然不正常的措施，提供了重要的设计时间信息的算法，并为理论分析，正常的措施也可以在运行时间使用，作为实用的计算工具，例如设置边界的假设检验，归纳推理和算法学习。
2014-02-23 cs.CC cs.LO math.CT
String Diagrams for $λ$-calculi and Functional Computation
本教程以系统方式介绍高阶计算的字符串图与图语言，从范畴论概念的二维语法逐步深入到笛卡尔闭范畴，通过从范畴模型重构分层超图语法并探讨其在编程语言领域的应用。
2024-12-04 cs.LO cs.PL math.CT
Monoidal computer I: Basic computability by string diagrams
我们提出了一个新的计算模型，描述monoidal类别。它符合丘奇-图灵命题，并捕获了与标准模型相同的可计算函数。它提供了一个简洁的分类接口，其中大多数，免费的各种实现细节，使用的想法和结构，同时出现在计算和编程的语义研究。monoidal范畴语言的显著特征是，它得到了一个健全而完整的图形形式主义--弦图的支持，弦图为关于计算的抽象推理提供了一个具体而直观的界面。这种努力的最初动机和最终目标是通过采用隐藏从实践中出现的低级实现细节的方法，为计算资源的理论（例如单向函数和陷门函数）提供方便的高级程序设计语言。在本文中，我们为实现这一宏伟目标迈出了第一步，并勾勒出了实现这一目标的道路，这条道路将在正在编写的三篇后续论文中继续探讨。
2012-12-29 cs.LO math.CT
Causal models in string diagrams
Quantinuum（昆腾纽姆）
本文用弦图和范畴论形式化因果模型，提出cd-范畴中的图示化定义，统一处理干预、条件化与反事实，并论证图示化推理是因果推理最自然的方式。
2023-04-15 cs.LG cs.LO math.CT
Rewriting for Symmetric Monoidal Categories with Commutative (Co)Monoid Structure
本文研究弦图重写中比完整 Frobenius 结构更弱的交换幺半群结构，并通过超图双推出重写的可靠且完备解释刻画了模去交换幺半群等式的弦图重写。
2025-01-30 cs.LO math.CT
Pattern graph rewrite systems
弦图是推理物理过程、逻辑电路、张量网络和许多其他组成结构的强大工具。狄克逊、邓肯和基辛格介绍了弦图，弦图是弦图的组合表示，可以通过图重写系统对图解理论进行自动推理。在这个扩展的摘要中，我们展示了如何通过引入模式图来极大地扩展这种重写系统的能力，模式图提供了一种表达重写规则的无限族的方法，其中某些标记的子图，称为！框（“bangboxes”），在一条规则的两侧，可以复制任意次数或删除。在回顾了字符串图的形式主义，我们将展示如何字符串图可以扩展到模式图，以及如何模式图和模式重写规则可以实例化到具体的字符串图和重写规则。然后，我们提供的例子展示了图案图的表达能力，以及它们如何可以应用于研究相互作用的代数结构，是中央分类量子力学。
2014-04-01 cs.LO math.CT
Timing via Pinwheel Double Categories
该研究探讨了用时序过程理论弦图的构建方法，其基于风车双重范畴弦图，以双幺半群分次对称严格幺半群范畴为表示形式。
2025-04-17 cs.LO math.CT
DisCoPy: the Hierarchy of Graphical Languages in Python
DisCoPy是Python工具包，提供两种字符串图数据结构（层列表与超图余跨度），支持函子应用转换至数值计算，1.0版本实现大片段图等价及新语法。
2023-11-17 cs.MS math.CT
Categorified Path Calculus
本文将路径演算范畴化，提出基于双幺半范畴上矩阵双范畴的曲面图演算，并展示双积、对偶和dagger等结构如何丰富该演算，最终给出隐形传态协议的新图形化证明。
2023-07-06 math.CT quant-ph
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 Diagrams with Factorized Densities
Khoury College of Computer Science（胡里计算机学院）；Northeastern University（东北大学）；University of Amsterdam（阿姆斯特丹大学）
为满足概率程序与因果模型的组合式推理需求，该研究基于概率映射马尔可夫范畴相关工作，定义了结合分解联合密度与确定性映射的范畴，以衔接概率测度的范畴论描述与分解密度的常用操作定义。
2023-12-14 cs.LG cs.LO cs.PL
Lambek vs. Lambek: Functorial Vector Space Semantics and String Diagrams for Lambek Calculus
University of Oxford（牛津大学）
分布组合范畴（Distributional Compositional Categorical，DisCoCat）模型是一个为自然语言句子的意义提供组合语义的数学框架。它包括一个计算过程，用于构建句子的意义，给定它们在组合类型逻辑方面的语法结构，并给定它们的单词的经验推导的意义。对于在分布式向量空间模型中对单词的含义进行建模的特定情况，其实验预测（来自真实的大规模数据）优于其他经验验证的方法，这些方法可以为完整的句子构建向量。这一成功可以归因于概念动机的数学基础，通过整合定性成分类型逻辑和定量建模的意义范畴理论的数学框架。DisCoCat模型中使用的类型逻辑是Lambek的前群文法。预群类型形成一个posetal紧闭范畴，它可以通过函子的方式传递到向量空间、线性映射和张量积的紧闭结构上。紧凑封闭范畴中等式推理的图解形式可以解释为句子中词义的流动。前群简化了Lambek以前的类型逻辑，Lambek演算，它已被广泛用于形式化和推理各种语言现象。DisCoCat对前团体的明显依赖被视为一个缺点。本文针对这一问题，指出，人们也可以实现一个函式通道从原来的类型逻辑的Lambek，monoidal双闭范畴，向量空间，或任何其他模式的意义组织在monoidal双闭范畴。Baez和Stay给出了相应的字符串图演算，描述了词义的流动。
2013-02-02 cs.CL math.CT math.LO
