Gatlab.jl：用广义代数理论进行范畴的符号计算

Gatlab.jl: Symbolic computing with categories using generalized algebraic theories

Gatlab.jl：用广义代数理论进行范畴的符号计算

https://act2023.github.io/papers/paper28.pdf

Catlab.jl 框架旨在通过 Julia 编程语言中高效、可复用的软件实现，揭示范畴论的基本抽象。这些抽象随后可用于构建特定领域的建模框架和面向用户的应用程序。

范畴计算可以采取多种形式。近年来，Catlab 开发团队聚焦于组合计算，创建了一种高效、内存中的范畴数据库实现 [10, 9]；同时也关注数值计算，通过与数值求解器的接口，实现了量化的函子语义 [7, 2]。尽管符号计算（即以计算机代数系统风格进行的范畴计算）始终是我们愿景的一部分，但迄今为止尚未得到充分发展。在本演示中，我们展示了一项早期但颇具前景的工作：将符号计算集成到 Catlab 的核心之中。我们正在一个名为 Gatlab.jl 的新软件包中开发这一功能。

Gatlab 受到 Cartmell 提出的广义代数理论（Generalized Algebraic Theories, GATs）的启发。GATs 是一种将代数理论与依赖类型相结合的逻辑系统 [4, 5]。与普通代数理论不同，GATs 具有足够的表达能力，可以形式化范畴的理论，以及大多数带有额外结构的范畴理论，例如幺半范畴（monoidal categories）以及具有选定积或极限的范畴。与同样具有表达能力的本质代数理论（essentially algebraic theories）[6, 1, §3.D] 和有限极限草图（finite limit sketches）[3] 等逻辑系统相比，GATs 拥有一种直观的语法，使得范畴论的定义与其教科书中的形式非常相似。

作为一个简单例子，读者将能认出下面 GAT 中对范畴的定义。

事实上，自 Catlab 项目创立之初，GATs 就已被实现，并在其中发挥了两个主要作用：一是作为组织原则，二是作为符号语法。在第一个作用中，应用范畴论中大量出现的范畴结构被系统地记录为 GATs。随后，特定的 Julia 类型和函数被声明为这些 GATs 的实例。例如，非负整数和数值矩阵就是双积范畴（biproduct categories）理论的一个实例。此外，给定一个 GAT，Catlab 会自动为该 GAT 中的表达式树生成 Julia 类型，从而为范畴中的对象和态射提供有用的符号数据结构。这两种作用都可以看作是对 GATs 的模型定义：实例是基于任意 Julia 代码的模型，而符号表达式则是自由模型（free models）或初始模型（initial models）。

利用元编程，我们便能实现从一个理论到另一个理论的、正确性由构造保证（correct-by-construction）的 Julia 实例迁移。在上述例子中，任何笛卡尔范畴的有效实例都会自动给出一个有效的透镜幺半范畴（monoidal category of lenses）。

转向第二个角色（符号推理），Gatlab 将通过将 GAT 表达式与 e-graphs（等式图）集成，提供 GAT 中的自动等式推理。e-graphs 将经典的并查集（union-find）数据结构从集合元素上的等价关系，扩展到表达式树上的同余关系，从而在一个单一的数据结构中高效地表示大量表达式之间的等式关系 [8, 11]。作为第一个例子，将等式饱和（equality saturation）过程应用于一个范畴的有限呈现，将能枚举（可能不会终止）该范畴中所有不同的态射。我们还将使用 e-graphs 高效地实现以可表函子的余极限（colimits of representables）形式给出的 C-集（C-sets），从而以符号方式补充范畴数据库的组合实现。

传统上，组合计算、符号计算和数值计算分别属于不同的软件系统，甚至不同的编程语言。Catlab 的目标是在一个统一的框架内整合这三种计算范式，该框架依据范畴论原则设计，用于对范畴论结构进行计算。Gatlab 中所展示的这项正在进行的工作，朝着实现这一愿景又迈出了重要一步。

原文链接：https://act2023.github.io/papers/paper28.pdf