技术摘要：一种用于残余过程行为的 Stone–Čech 收集语义

1. 问题陈述

无限计算不仅由其执行的动作序列所刻画，还留下了（在每次转换后剩余待执行的）残余过程（residual processes）序列。虽然有限计算或进入简单循环的计算已被充分理解，但无限执行可能表现出复杂的长期行为：

• 稳定发散（Stable divergence）： 稳定于单个过程或有限循环。
• 混合递归（Mixed recurrence）： 无限次地返回某些状态，同时也访问着一个无界的全新状态序列。
• 逃逸（Escape）： 离开观测空间的所有有限部分（例如，并行组件数量的无界增长），且没有任何单一的残余过程会再次出现。

挑战在于提供一种统一的语义形式来处理这些多样化的残余尾部（residual tails）。标准的极限集对于非紧空间（其中序列可能没有极限）会失效；而简单的递归计数也无法捕捉“逃逸”行为。此外，该语义必须在观测下具有鲁棒性：由于完整的语义对象过于庞大而无法直接检查，它必须在连续观测（如资源计数器或模态谓词）下表现良好。

2. 方法论

本文构建了一种过滤的 Stone–Čech 收集语义。核心方法论是将无限执行视为观测流，并将其渐近行为映射到观测空间的 Stone–Čech 紧化中。

2.1 构造过程

• 过滤时间（Filtered Time）： 一个运行（run）被定义为一个映射 $a: T \to X$，其中 $T$ 是配备了适当过滤器 $\mathcal{F}$（指定“大”集合）的时间索引集，$X$ 是 Tychonoff 观测空间。
• Stone–Čech 含义： 该运行的含义是紧集：
  $$M^F_X(a) = \beta a[\text{Ext}(\mathcal{F})] = \bigcap_{F \in \mathcal{F}} \text{cl}_{\beta X} a[F] \subseteq \beta X$$
  这里，$\text{Ext}(\mathcal{F})$ 是 $T$ 上扩展 $\mathcal{F}$ 的超滤子，$\beta a$ 是 $a$ 到紧化空间的连续扩展。
• 解释：
  • 对于顺序时间（$T=\mathbb{N}$）且使用余有限过滤器（cofinite filter）的情况，这产生了 $\beta X$ 中的尾部簇集（tail-cluster set）。
  • 如果 $X$ 是离散且有限的，则 $M^F_X(a)$ 是无限次访问的状态集合。
  • 如果 $X$ 是离散且无限的（例如 $\mathbb{N}$），其含义可以包含点在剩余部分 $X^* = \beta X \setminus X$ 中，代表向无穷大的“逃逸”。

2.2 观测解读

该语义旨在通过连续观测 $f: X \to Y$ 来进行读取。通过函子性（functoriality），观测运行的含义是原始含义的像：
$$M^F_Y(f \circ a) = \beta f[M^F_X(a)]$$

• Clopen 观测： 对于 $X$ 中的 clopen 集 $C$，包含关系 $M^F_X(a) \subseteq \text{cl}_{\beta X} C$ 对应于最终真（eventual truth）（运行最终处于 $C$ 中），而非空交集则对应于递归（recurrence）（运行无限次访问 $C$）。
• 资源观测： 整值资源映射（例如统计并行组件的数量）可以通过将紧致含义映射到自然数的剩余部分（$\mathbb{N}^*$）来检测无界逃逸。

2.3 处理非确定性与公平性

• 非确定性： 该语义区分了运行敏感型含义（一个紧集的集合，每个执行对应一个）和扁平化含义（所有渐近点的并集）。
• 公平性： 公平性和进展假设通过加强时间过滤器来处理。公平含义是通过将容许的超滤子限制为包含特定进展集的超滤子来计算的。
• 关系属性： 为了保留同时观测之间的相关性（例如两个过程并行运行），该构造紧化的是乘积空间 $\beta(X_1 \times \dots \times X_k)$，而不是单个含义的乘积。

3. 关键贡献与结果

3.1 通用理论

1. 尾部不变性（Tail Invariance）： 含义对于在不在过滤器中的任何时间集合上的运行变化是不变的（例如，改变流中的有限个项）。
2. 函子性： 连续观测与构造过程交换，允许从单一紧致对象中导出有限商、模态逻辑和资源映射。
3. 时序逻辑： 该构造为时序模态提供了直接的拓扑解读：$\Box_\infty A$（最终真）和 $\Diamond_\infty A$（递归）分别对应于紧化中的集合包含和交集。

3.2 对 CCS（通信顺序进程演算）的应用

本文将该框架应用于 CCS，其中无限执行被视为结构同构类过程的流。

• 行为分类： 该语义区分了：
  • 稳定发散： 单元素集合（例如 $A \xrightarrow{a} A$）。
  • 有限递归发散： 有限集合（例如在 $P$ 和 $Q$ 之间交替）。
  • 无界残余增长： 完全包含在剩余部分 $\beta \text{CCS} \setminus \text{CCS}$ 中的集合（例如 $G \xrightarrow{a} G|G \xrightarrow{a} G|G|G \dots$）。
  • 混合行为： 主成分（recurrent）与非主成分（escaping）的组合。
• 残余尾部定律（Residual-Tail Laws）： 本文证明了对于有限前缀选择包装器（形式为 $\alpha_1.P_1 + \dots + \alpha_k.P_k$ 的过程），其渐近残余含义是各叶子节点含义的并集。有限前缀和守卫展开（guarded unfoldings）不会影响尾部含义。
• 定律的边界： 本文表明，这些定律对于任意 CCS 上下文不是同余关系。具体而言，并行组合与同步可以使得有限前缀在被消耗前变得相关（例如，前缀 $a.0$ 可以与环境同步以启用一个循环，而 $0$ 则不能）。因此，这是一种“残余尾部”语义，而非完整的上下文等价。

3.3 计算接口

由于 $\beta X$ 是不可数的且不是有效可枚举的，本文通过有限观测商提供了一个计算接口：

• 一个有限的布尔代数过程谓词会诱导出一个有限商空间。
• 紧致含义在该有限空间中的像正是递归抽象状态的集合。
• 对于有限转移图，这可以简化为强连通分量（SCC）分析。在“边公平”（edge-fair）约定下，公平含义对应于可达的终端 SCC。
• 资源可观测性： 无界逃逸可以通过观察资源映射（例如过程大小）趋于无穷大来检测，这对应于紧致含义落在 $\mathbb{N}$ 的 Stone–Čech 剩余部分。

4. 重要性与主张

本文声称提供了一种用于残余过程行为的统一、紧凑的收集语义，该语义：

1. 泛化了递归： 它涵盖了普通的递归（有限空间）和极限集（紧致空间），同时扩展到了发生“逃逸”的非紧致空间。
2. 统一了观测： 它将有限商、模态逻辑和资源测量视为单一语义对象的连续像，确保了不同抽象层级之间的一致性。
3. 澄清了尾部等价性： 它为何时可以擦除有限前缀（在尾部中）建立了精确的法则，并明确指出了并行组合破坏此等价性的边界。
4. 支持计算： 它在抽象、不可计算的紧致对象与具体的、有限的验证技术（SCC 分析）及资源监控之间架起了桥梁。

该构造被呈现为一种语义载体：紧致对象本身并不直接被检查，但其投影（通过观测）为分析、公平性检查和无限行为的验证提供了有效的接口。