复合信号流理论综述|代数|信号|定理|流图|语法

A Survey of Compositional Signal Flow Theory

复合信号流理论综述

https://inria.hal.science/hal-03325995/document

摘要

信号流图是线性动力系统的组合模型，在控制理论和工程中发挥着基础性作用。在本综述中，我们概述了一系列工作 [15, 3, 18, 16, 31, 17, 10, 11, 13, 63, 51]，这些工作发展了这些结构的组合理论，并探讨了由此方法产生的几个引人注目的见解。特别是，字符串图（string diagrams）——一种用于图形模型的范畴语法——的使用，使得人们能够从传统的信号流图组合处理方法转向代数刻画。在此框架内，信号流图随后可以被视为一种成熟的（可视化）编程语言，并配备了重要的元理论性质，例如完备的公理化系统和完全抽象定理。此外，字符串图所提供的抽象视角揭示出，那些用于建模线性动力系统的相同代数结构，也可用于解释多种不同类型的模型，如电路和 Petri 网。

在这方面，我们的工作是对组合网络理论（compositional network theory）（参见例如 [1, 59, 20, 23, 21, 29, 49, 28, 2, 5, 6, 32, 9, 30, 4, 24, 26, 37, 12, ?]）的一项贡献；这是一个新兴的多学科研究计划，旨在对不同种类的计算模型进行统一的组合研究。

关键词： 信号流图 · 组合语义 · 范畴论 · 字符串图

1 字符串图作为资源敏感语法

后一种描述特别具有启发性，因为它强调了有限积的核心作用，这暴露了一个关于语法旨在表达的内容的笛卡尔性（cartesianity）的潜在假设。特别是，作用域内的变量可以被多次使用，或者根本不被使用。因此，我们操作的数据是经典的（classical）：它可以被随意复制和丢弃。也许不那么明显的是对签名定义的事后辩护：所有运算都表示恰好有一个输出的函数。任何具有两个输出的运算都可以通过丢弃适当的输出简单地分解为两个单输出运算。因此，通过允许除 1 以外的余元数（coarities）来使签名的定义更加宽松，并不会增加表现力。

当底层数据不是经典的时候，什么样的语法概念是合适的？或者如果我们想要表示非函数实体（例如关系）呢？一种在这种意义上更具表现力，但仍保留其递归规范及相关结构归纳原则的语法？

答案是用自由 PROPs [44, 41] 取代具有积的自由范畴。

与 (1) 不同，元数和余元数不在 BNF 中处理，而是通过 (3) 的附加结构以及如下所示的相关排序规则来处理。我们只考虑具有类型的项，如果类型存在，则它是唯一的。

Prop 的定律识别出了所有且恰好那些具有相同底层连通性的项。其口号是“只有拓扑结构才重要”。这意味着，在 Σ Σ 上的自由 prop 中，我们不需要用虚线框来破坏我们的图表，并且字符串图无歧义地表示了项（在 prop 定律的意义下）。尽管如此，我们仍然可以访问由 (2) 和 (3) 给出的低级表示，其中具体代表的选择不影响结果。

此外，我们的图表作为自由 prop 的箭头这一事实意味着它们的行为类似于经典语法。事实上，正如我们所见，它们具有递归定义，并享有类似的结构归纳原则。

2 信号流图演算

本文的主题是一种特定的字符串图语法，称为信号流图演算。我们将看到，正如其名所示，这种语法适用于对信号流图进行代数推理；信号流图是控制理论和工程中一种众所周知的基础结构（参见例如 [58, 45]）。

固定一个半环 R R，信号流图演算的幺半签名如下：

例 2. 考虑下面的两个电路。

2.1 反馈与经典信号流图

注 1. 读者可能已经在 (5) 中识别出了迹（trace）[38] 的结构。事实上，用带迹幺半范畴（traced monoidal categories）[34] 来建模带有反馈的系统是一种传统。这些结构的代数核心也在迭代理论 [8] 和 Stefanescu 的网络代数 [60] 的背景下被研究过。就信号流图这一更具体的设定而言，先前的范畴方法大多基于余代数理论 [55, 7, 46]。此处提出的字符串图方法（起源于 [15]，随后在 [3] 中被独立提出）的一个显著特征是采用了更抽象的框架，该框架包含了比经典信号流图（它们构成子范畴）更多的电路图。正如我们将在第 4 节和第 5 节中看到的那样，这种增加的一般性是以使操作分析变得更加微妙为代价的。其回报是一种更初等的语法 (4)，它不包含任何用于递归的原语，并且有可能实现一种简洁的公理化系统（第 3.1 节），该系统基于诸如双幺半群（bimonoids）和弗罗贝尼乌斯半群（Frobenius monoids）等众所周知的代数结构。

3 指称语义

在这里，我们为电路配备了一种指称语义（denotational semantics），即为每个电路分配一个适当数学宇宙中的元素。

指称语义为电路 c c 分配一个轨迹（trajectories）关系，该关系对应于 c c 的所有可能执行。同样，对于人们可能视为“执行”的内容也有不同的选择，这为我们提供了语义模型的另一个维度。文献中主要研究的两种情况是：过去有限、未来无限的执行——等价于假设执行从 0 初始化的寄存器开始——以及双无限轨迹，等价于（额外）考虑寄存器在任何时刻都可以持有任意初始值的执行。在引入了电路的形式操作语义后，我们将在注 5 中使这些观测更加精确。

过去有限、未来无限轨迹的集合是 k k 上的洛朗级数（Laurent series）域。事实上，洛朗级数 σ σ 可以被理解为一个流（stream），即 k k-元素的无限序列

我们可以以一种与轨迹无关的方式来定义指称语义：

3.1 交互霍普夫代数：电路的等式理论

如图 1所示，该等式理论由以下“模块”组成：

在第一个模块中，黑色结构和白色结构均构成交换半群（commutative monoids）和交换余幺半群（comonoids），分别刻画了加法和复制的性质。
在第二个模块中，白色幺半群与黑色余幺半群以双幺半群（bimonoid）的形式进行交互。正如 [41] 所示，双幺半群是幺半群与余幺半群相互作用的两种规范方式之一。

注 4（Kleene 定理）。 定理 3 的最后一点可以被视为正则语言 Kleene 定理的类比：它提供了对有理行为的语法刻画。所表示的关系是性质特别良好的函数，因为它们实际上并不需要洛朗级数的全部一般性：任何有理多项式都会生成一个有限幂级数，而无需“有限的过去”。（正统）信号流图与有理矩阵之间的对应关系是众所周知的（参见例如 [54]）：在此，我们给出了这一刻画的范畴论及字符串图论解释，其中“输入”、“输出”和流向等概念都是衍生出来的。

我们还要提到，定理 3 的第 1 点似乎是一个民间结果（folklore result），以各种形式普遍出现在文献中 [42, 36, 52, 48, 41, 63]。

4 操作语义

就像编程语言一样，指称语义只是赋予电路语法形式化意义的一种方式。在本节中，我们采取不同的视角，将电路视为基于状态的机器，其逐步执行过程即为操作语义。

在更深层次上，例 6 表明操作语义并非旨在对所有电路都可执行：顺序组合的规则隐式地对中间值 v v 进行了存在量词量化，从而导致了潜在的无界非确定性。令人满意地理解这一现象是下一节的主题。作为初步观察，值得注意的是，如果将限制放宽到无限计算，那么例 6 中概述的不匹配就会消失，并且我们在操作等价性和指称等价性之间建立了完美的对应关系。

为了陈述这一结果，我们引入一个预备概念。按照控制理论中的惯例，我们考虑轨迹（trajectories）：即可能从过去开始的迹（traces）。

注 5. 我们特意使用了与指称语义中相同的术语“轨迹”（trajectories）：事实上，从初始状态开始的计算与我们在第 3 节中遇到的洛朗级数之间存在着密切的联系。

事实上，任何端口上的观测序列显然都是一个洛朗级数——任何计算都可以平凡地（即具有 0 次观测）无限地向过去延续，正如定义 6 中的 (10) 所反映的那样。人们可以推广计算的概念，使其不必从初始化状态开始：在这种情况下，相应的轨迹概念 (10) 可能是一个真正的双无限序列，即 σ σ 在过去可能是无限的。更多细节请参见 [31, 30]。

5 可实现性

鉴于例 6，人们可能会问常见的死锁情况（如 (9) 中的情况）以及需要从过去开始的计算（如 (8) 中的情况）有多普遍。事实证明，当考虑 adheres to 经典信号流图概念的电路子类的操作语义时，这些问题是可以避免的。

5.1 信号流的组合性与方向性

因此，电路、其代数理论及其组合语义可以被视为一种真正的信号流过程代数，既可用作规范（specifications）语言，也可用作（可执行的）实现（implementations）语言。事实上，该语言适用于形式化方法技术，如细化（refinement），参见 [10]。

6 仿射扩展

工程师通常不区分线性和仿射（affine）系统，因为研究这两者的数值方法实质上是相同的。然而，从我们的角度来看，这种区分很重要，因为为了表达仿射行为，我们需要扩展信号流图演算以及迄今为止阐述的主要结果。这种扩展被证明极其有趣，因为一方面，它使得能够对具有更丰富行为模式的系统进行建模，例如第 7 节中的电流和电压源或第 8 节中的互斥；另一方面，它允许定义上下文等价（contextual equivalence），并将定理 4 转化为一个恰当的完全抽象结果（full abstraction result）（定理 8）。

6.1 完全抽象

仿射扩展的第一个回报是能够为电路图制定上下文等价（contextual equivalence）的概念，从而得出一个完全抽象结果（full abstraction result）。

为此，我们首先将操作语义扩展到语法。这相当于用以下内容扩充图 2 中的规则：

7 电路

采用抽象且非常初等的电路语法的一个主要优势在于，信号流图变成了其中可以研究的计算模型之一。在本节中，我们将聚焦于电路，展示如何在中对它们进行建模。在下一节中，我们将简要说明另一种不同的模型——Petri 网——如何也能得到类似的描述。

基础电气工程专注于开放线性电路分析。

正如我们所见，这是在仿射演算中表示空关系的方式。串联电流源（第一列，最后一行）的情况也是如此。

注 8. 关于在仿射电路图中编码电路的更多细节，读者可参阅 [13]。Baez 和 Coya [37, 26] 给出了类似的语义，他们建立在 Baez、Erbele 和 Fong [3, 6] 以及 Rosebrugh、Sabadini 和 Walters [53] 的工作之上。然而，这些工作仅考虑无源线性电路，即不含电压源和电流源的电路。

8 从控制理论到并发

我们已经表明，信号流图演算允许对一类重要的行为（线性动力系统）进行公理化，从而捕捉了一个众所周知的既有组合模型（信号流图）。该方法是组合式的，允许开放系统的语法表示并强调其代数性质，但同时又是图形化的，强调其连接拓扑和组合性质。

从历史上看，对这些方面的不同侧重导致了并发系统分析中不同的研究脉络。一方面，我们有进程演算（process calculi）[47, 56, 35] 提出的代数方法。另一方面，存在并发行为的图形模型传统，例如 Petri 网（参见例如 [50]）。

因此，信号流图演算似乎可以作为进程演算和图形模型所提供的视角之间的中间地带。这促使我们 [11] 使用与信号流理论中分析线性行为相同的图解方法来分析并发系统。

最令人惊讶的是，从线性行为过渡到并发行为时，设置可能基本保持不变：人们可以使用语法 (4) 的相同生成元，唯一显著的变化是通过一组不同的信号来建模其行为，即从域 k k 过渡到自然数半环 N N。

为了解释这一点，我们展示了来自 [13] 和 [11] 的两个例子。

这些观察结果已在资源演算（resources calculus）[51, 11] 中得到结晶：其语法与信号流图演算相同，但信号宇宙被固定为 N N。这种切换迫使人们从线性关系转向加法关系，并因此改变公理化系统 [11]。在 [13] 中，证明了无状态连接器的代数 [20] 可以很容易地编码到资源演算的（仿射扩展）中。[11] 展示了资源演算内对 Petri 网的扩展研究。这提供了一种深刻的理解，即将 Petri 网视为线性动力系统（但是在 N N 上），以及一种优雅的组合操作语义。相反，指称语义似乎具有挑战性，肯定值得进一步研究。

9 本研究与 IFIP AICT 600 - IFIP 60 周年庆典专刊

本文所述的研究与两个 TC1 工作组的兴趣相交叉：IFIP-WG 1.3 系统规范基础组和 IFIP-WG 1.8 并发理论组。它也涉及 TC2 的主题，与 IFIP-WG 2.2 编程概念的形式描述相关。首先，信号流图是一种简单但普遍的计算模型。这里描述的二维方法足够灵活，能够使字符串图语法既表达形式规范又表达实现。公理化特征意味着前者可以以有原则的方式转化为后者。此外，我们给出的操作语义是一种并发进程代数，并且——在仿射扩展中——我们探讨了其对 Petri 网语义研究的影响，Petri 网是并发的经典模型。最后，对指称方法和操作方法之间交互的强调——重点关注组合性——源于形式编程语言语义的研究，但在理论计算机科学中正变得越来越重要。

原文链接：https://inria.hal.science/hal-03325995/document