论文标题
联合单型：在树上找到简单的集合和标记为代数图
United Monoids: Finding Simplicial Sets and Labelled Algebraic Graphs in Trees
论文作者
论文摘要
图和各种图形的组合结构（例如预订和超图）在编程中无处不在。本文着重于在Haskell（例如Haskell）纯粹功能的编程语言中代表图。现有的方法有几种；最近发达的方法之一是“代数图”方法（2017）。它使用代数数据类型来表示图形，并吸引了包括行业在内的用户，因为它强调了方程推理并通过消除内部不变性来使不可能的常见错误类别。 代数图的先前公式不支持边缘标签，这是一个严重的实际限制。在本文中，我们重新设计了主要代数数据类型并删除此限制。我们遵循一种相当标准的方法，即用边缘标签半分析数据结构。新的公式既更加通用，更简单：现在可以通过将半度参数固定到零和一个操作来从单个操作中获得以上作品中使用的图形的两个操作。 通过使用不同的半段实例化新数据类型，并制定法律来解释所得的表达树，我们发现了一种不寻常的代数结构，我们称之为“联合型单体”，即一对单位元素重合的单型肌体。我们认为，值得在其全部一般性上研究联合的单脚体，这超出了促使他们发现的图表。为此，我们以最少的公理集表征了联合的单体，证明了一些基本的定理，并讨论了几个值得注意的例子。 我们通过在开源 *代数图库中实现了介绍的方法。我们的理论贡献得到了论文中包含的证据的支持，并且也已在AGDA中进行了机器检查。通过扩展代数图并支持边缘标签，我们使它们适合于更大类可能的应用程序。通过研究联合MONOIDS，我们为该领域的进一步研究提供了理论基础。
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.
