作为对称monoidal闭理论的绑定偶图
Binding bigraphs as symmetric monoidal closed theories
摘要：
米尔纳的双图是一个通用的框架，用于分布式和并发程序设计语言的推理。值得注意的是，它被设计为包含pi演算和Ambient演算。本文只关注双图语法：给定我们这里称之为双图签名K，Milner构造了一个双图BBig（K）的（前）范畴，其主要特征是（1）存在相对推出（RPOs），这使得它们相对于.互模拟，以及（2）所谓的结构方程成为等式。后者的例子包括，例如，在pi和Ambient中，绑定变量的重命名，并行组合的结合性和交换性，或限制名称的范围挤出。此外，bigraphs遵循一个作用域规则，确保绑定的变量不会脱离其作用域。在这里，我们使用一个标准的分类工具：对称monoidal封闭（SMC）理论重建双图。我们的理论强制执行相同的范围纪律作为双图，作为SMC结构的直接属性。此外，它还阐明了所谓的链接在双图中略显神秘的地位。最后，我们的范畴也比双图的范畴大得多，特别是包含在相同的框架内的术语和更高阶上下文的灵活形式。
英文摘要：
Milner's bigraphs are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the pi-calculus and the Ambient calculus. This paper is only concerned with bigraphical syntax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs BBig(K), whose main features are (1) the presence of relative pushouts (RPOs), which makes them well-behaved w.r.t. bisimulations, and that (2) the so-called structural equations become equalities. Examples of the latter include, e.g., in pi and Ambient, renaming of bound variables, associativity and commutativity of parallel composition, or scope extrusion for restricted names. Also, bigraphs follow a scoping discipline ensuring that, roughly, bound variables never escape their scope. Here, we reconstruct bigraphs using a standard categorical tool: symmetric monoidal closed (SMC) theories. Our theory enforces the same scoping discipline as bigraphs, as a direct property of SMC structure. Furthermore, it elucidates the slightly mysterious status of so-called links in bigraphs. Finally, our category is also considerably larger than the category of bigraphs, notably encompassing in the same framework terms and a flexible form of higher-order contexts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
