联合幺半群：在树中寻找单纯集和标号代数图
United Monoids: Finding Simplicial Sets and Labelled Algebraic Graphs in Trees
摘要：
图和各种类似图的组合结构，如前序和超图，在编程中无处不在。这篇文章的重点是用纯函数式程序设计语言（如Haskell）表示图。有几种现有的方法;最近开发的方法之一是“代数图”方法（2017）。它使用代数数据类型来表示图形，并吸引了用户，包括来自行业的用户，因为它强调等式推理，并通过消除内部不变量来消除常见的一类错误。以前的代数图公式不支持边标签，这是一个严重的实际限制。在本文中，我们重新设计了主要的代数数据类型，并消除了这一限制。我们遵循一个相当标准的方法，用边标签的半环来参数化数据结构。新的公式更一般，也更简单：在以前的工作中使用的两个操作组成图，现在可以从一个单一的操作，通过固定半环参数为零和1，分别获得。通过用不同的半环对新的数据类型进行实例化，并对由此产生的表达式树进行解释，我们发现了一种不寻常的代数结构，我们称之为“united monoid”，即一对单位元素重合的monoid。我们相信，这是值得研究的联合幺半群在其充分的一般性，超越了图形，促使他们的发现。为此，我们用一组最小公理来统一么半群，证明一些基本定理，并讨论几个值得注意的例子。我们通过在开源 *algebraic-graphs* 库中实现该方法来验证所提出的方法。我们的理论贡献是支持的证明，包括在文件中，也已在Agda机器检查。通过扩展支持边标签的代数图，我们使它们适合于更大的一类可能的应用。通过对联合幺半群的研究，为这一领域的进一步研究提供了理论基础。
英文摘要：
Graphs and various graph-like combinatorial structures, such as preorders and hypergraphs, are ubiquitous in programming. This paper focuses on representing graphs in a purely functional programming language like Haskell. There are several existing approaches; one of the most recently developed ones is the "algebraic graphs" approach (2017). It uses an algebraic data type to represent graphs and has attracted users, including from industry, due to its emphasis on equational reasoning and making a common class of bugs impossible by eliminating internal invariants. The previous formulation of algebraic graphs did not support edge labels, which was a serious practical limitation. In this paper, we redesign the main algebraic data type and remove this limitation. We follow a fairly standard approach of parameterising a data structure with a semiring of edge labels. The new formulation is both more general and simpler: the two operations for composing graphs used in the previous work can now be obtained from a single operation by fixing the semiring parameter to zero and one, respectively. By instantiating the new data type with different semirings, and working out laws for interpreting the resulting expression trees, we discover an unusual algebraic structure, which we call "united monoids", that is, a pair of monoids whose unit elements coincide. We believe that it is worth studying united monoids in their full generality, going beyond the graphs which prompted their discovery. To that end, we characterise united monoids with a minimal set of axioms, prove a few basic theorems, and discuss several notable examples. We validate the presented approach by implementing it in the open-source *algebraic-graphs* library. Our theoretical contributions are supported by proofs that are included in the paper and have also been machine-checked in Agda. By extending algebraic graphs with support for edge labels, we make them suitable for a much larger class of possible applications. By studying united monoids, we provide a theoretical foundation for further research in this area.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
