超图重写与λ-演算的因果结构

超图重写与λ-演算的因果结构

Hypergraph rewriting and Causal structure of λ−calculus

https://arxiv.org/pdf/2409.01006

摘要

在本文中，我们首先用范畴论的术语研究超图重写，试图定义事件的概念并发展图重写中因果性的基础。我们在粘着范畴（adhesive categories）的双推out（double-pushout）重写框架内引入新颖的概念。其次，我们将研究λ-演算中事件的概念，在其中我们构造一个算法，以确定在满足某些条件的λ-表达式求值过程中事件之间的因果关系。最后，我们尝试将这一定义扩展到任意λ-表达式。

1 引言

在计算系统中，关于两个事件之间的关系出现了一个基本问题：具体来说，一个事件如何影响或导致另一个事件。计算机科学中因果性的概念最初由 Glynn Winskel [12] 探索，他引入了一个抽象框架来刻画事件及其之间的因果关系。从那时起，在理解因果性背后的结构方面取得了重大进展。因果性的重要性在动力系统中也很明显，正如爱因斯坦的广义相对论中所强调的那样，其中洛伦兹流形（Lorentzian manifold）的因果结构唯一地决定了时空的几何结构（模去一个缩放因子）。此外，理论物理学中的因果集理论（causal set theory）等领域为这一复杂主题提供了额外的见解。尽管有这些发展，但在特定计算系统中事件及其因果关系的明确描述尚未得到广泛研究。在本文中，我们首先通过考察超图重写背景下连续事件之间产生的事件概念和因果关系开始，并用范畴论的术语进行框架化。对于那些寻求进一步探索超图重写的人，Wolfram 物理项目 [5] 是一个极好的资源。值得注意的是，Wolfram 语言中提供了几个与超图重写相关的工具，如 [1] 中所演示。

我们将在下一节展示，上述所有内容都可以用范畴论的术语优雅地表述，这在文献中被称为双推出重写（double-pushout rewriting）。关于这一点的极好解释可以在文献 [7] 中找到。

2 超图重写的范畴论表述

我们称 H H 为图生成（graph production），或输出图。即使不满足无悬空边（no-dangling edge）条件，也是可以进行图重写的——我们可以构造切割图，然后粘合图 R R。然而，如果我们想在任意范畴中进行重写，那么双推出（double-pushout，简称 DPO）重写是首选的形式体系 [7]。一般来说，DPO 重写可以在粘着范畴（adhesive categories）中进行，这类范畴是指那些推出补（pushout complements）在同构意义下唯一的范畴。关于粘着范畴的简明介绍见 [8]。

定义（粘着范畴）：如果一个范畴 C C 满足以下条件，则称为粘着的（adhesive）：

• 它拥有沿单态射（monomorphisms）的推出（pushouts）
• 它拥有拉回（pullbacks）
• 沿单态射的推出是 Van-Kampen 方块

关于 Van-Kampen (VK) 方块的定义见 [8]。推出补的唯一性直接源于 VK 方块条件。我们可以证明我们的范畴 H H 是粘着的。我们首先证明我们的范畴是广延的（extensive）。

定义（广延范畴）：当一个范畴 C C 满足以下条件时，称为广延的（extensive）：

• 它拥有有限余积（finite coproducts）
• 它拥有沿余积注入（coproduct injections）的拉回
• 给定一个底行是余积的图，

3 因果性

两个不同的事件有可能应用于图 G G 的不同位置，然而导致同构的输出图。理想情况下，人们会希望区分这些图，为此不应使用双推出重写方法（因为推出补和推出仅在同构意义下被描述）。为了做到这一点，可以使用一个标记函数，将关于该事件的信息编码在输出图中。这将在下一节关于确定 λ λ-演算中因果关系的语境中看到。然而，对于因果性的初步讨论，考虑 H H 的同构类就足够了。此外，以下内容可以推广到任何粘着范畴（adhesive category），而在这些范畴中，典范标记（canonical labelling）是未知的。

4 λ-演算中的因果性

4.1 先前工作概述

从上文可以看出，集合上的因果关系不能是自反的。第二个关系明确指出，如果 x x 导致 y y ，那么 y y 不能导致 x x ，这在大多数物理和计算机系统中似乎是成立的（我们将在稍后讨论物理学中的因果性概念及其与我们在本文中使用的概念的关系）。Winskel 扩展了因果集的定义以区分并发事件和因果断开的事件。即，两个并发事件必须是因果断开的，但反过来不一定成立。例如，可能存在事件 A A 和 B B ，它们可能使用某些共同的“资源”，即两者不能同时发生，但谁也不 导致 谁。在超图重写的情况下，例如，2 个可以一起发生但具有非空接口图重叠的事件是因果断开的，但它们不能顺序发生，因为一个删除了另一个匹配中的一些顶点/边。所以它们不是并发的。在 [6] 中，并发定义如下：

第二个条件指出，如果一个有限的事件集 X X 都能发生在同一个计算历史中，那么这些事件的一个子集 Y Y 也能发生在同一个历史中，这是一个显而易见的陈述。Con 中所有元素均为有限子集这一要求源于有限原因公理。启用关系（enabling relation）被视为因果依赖关系的替代。

我们现在定义多路系统（multiway system）的概念，它由从单个 λ λ -表达式开始的所有可能的求值路径组成。多路系统在 Wolfram 物理项目 [5] 中无处不在。

5 未来工作

原文链接： https://arxiv.org/pdf/2409.01006