一句话：提出带图，为有限双积的 rig 范畴给出可靠且完备的图解语言，并用于关系演算。
本文关注带有限双积的 rig 范畴：这类范畴具有两个 monoidal product，其中一个是 biproduct，另一个对前者满足分配律。作者提出 tape diagrams，一种可靠且完备的图解语言，可直观理解为“string diagrams 的 string diagrams”，用以在这些范畴中进行等式推理。该语言为 rig 范畴提供了图解演算，并给出其相对于范畴公理的可靠性与完备性。作者以 Tarski 关系演算的正片段为测试对象，说明该图解语言能有效刻画关系演算中的推理。结果表明，tape diagrams 能统一处理双积与分配结构，并为关系演算提供直观的图示推理方式。
Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test the effectiveness of our approach against the positive fragment of Tarski's calculus of relations.
@article{paperbot2108,
title = {Deconstructing the Calculus of Relations with Tape Diagrams},
author = {Filippo Bonchi and Alessandro Di Giorgio and Alessio Santamaria},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571257}
}