復(fù)合信號流理論綜述

A Survey of Compositional Signal Flow Theory

復(fù)合信號流理論綜述

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

摘要

信號流圖是線性動(dòng)力系統(tǒng)的組合模型，在控制理論和工程中發(fā)揮著基礎(chǔ)性作用。在本綜述中，我們概述了一系列工作 [15, 3, 18, 16, 31, 17, 10, 11, 13, 63, 51]，這些工作發(fā)展了這些結(jié)構(gòu)的組合理論，并探討了由此方法產(chǎn)生的幾個(gè)引人注目的見解。特別是，字符串圖（string diagrams）——一種用于圖形模型的范疇語法——的使用，使得人們能夠從傳統(tǒng)的信號流圖組合處理方法轉(zhuǎn)向代數(shù)刻畫。在此框架內(nèi)，信號流圖隨后可以被視為一種成熟的（可視化）編程語言，并配備了重要的元理論性質(zhì)，例如完備的公理化系統(tǒng)和完全抽象定理。此外，字符串圖所提供的抽象視角揭示出，那些用于建模線性動(dòng)力系統(tǒng)的相同代數(shù)結(jié)構(gòu)，也可用于解釋多種不同類型的模型，如電路和 Petri 網(wǎng)。

在這方面，我們的工作是對組合網(wǎng)絡(luò)理論（compositional network theory）（參見例如 [1, 59, 20, 23, 21, 29, 49, 28, 2, 5, 6, 32, 9, 30, 4, 24, 26, 37, 12, ?]）的一項(xiàng)貢獻(xiàn)；這是一個(gè)新興的多學(xué)科研究計(jì)劃，旨在對不同種類的計(jì)算模型進(jìn)行統(tǒng)一的組合研究。

關(guān)鍵詞： 信號流圖 · 組合語義 · 范疇論 · 字符串圖

1 字符串圖作為資源敏感語法

后一種描述特別具有啟發(fā)性，因?yàn)樗鼜?qiáng)調(diào)了有限積的核心作用，這暴露了一個(gè)關(guān)于語法旨在表達(dá)的內(nèi)容的笛卡爾性（cartesianity）的潛在假設(shè)。特別是，作用域內(nèi)的變量可以被多次使用，或者根本不被使用。因此，我們操作的數(shù)據(jù)是經(jīng)典的（classical）：它可以被隨意復(fù)制和丟棄。也許不那么明顯的是對簽名定義的事后辯護(hù)：所有運(yùn)算都表示恰好有一個(gè)輸出的函數(shù)。任何具有兩個(gè)輸出的運(yùn)算都可以通過丟棄適當(dāng)?shù)妮敵龊唵蔚胤纸鉃閮蓚€(gè)單輸出運(yùn)算。因此，通過允許除 1 以外的余元數(shù)（coarities）來使簽名的定義更加寬松，并不會(huì)增加表現(xiàn)力。

當(dāng)?shù)讓訑?shù)據(jù)不是經(jīng)典的時(shí)候，什么樣的語法概念是合適的？或者如果我們想要表示非函數(shù)實(shí)體（例如關(guān)系）呢？一種在這種意義上更具表現(xiàn)力，但仍保留其遞歸規(guī)范及相關(guān)結(jié)構(gòu)歸納原則的語法？

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

與 (1) 不同，元數(shù)和余元數(shù)不在 BNF 中處理，而是通過 (3) 的附加結(jié)構(gòu)以及如下所示的相關(guān)排序規(guī)則來處理。我們只考慮具有類型的項(xiàng)，如果類型存在，則它是唯一的。

Prop 的定律識別出了所有且恰好那些具有相同底層連通性的項(xiàng)。其口號是“只有拓?fù)浣Y(jié)構(gòu)才重要”。這意味著，在 Σ Σ 上的自由 prop 中，我們不需要用虛線框來破壞我們的圖表，并且字符串圖無歧義地表示了項(xiàng)（在 prop 定律的意義下）。盡管如此，我們?nèi)匀豢梢栽L問由 (2) 和 (3) 給出的低級表示，其中具體代表的選擇不影響結(jié)果。

此外，我們的圖表作為自由 prop 的箭頭這一事實(shí)意味著它們的行為類似于經(jīng)典語法。事實(shí)上，正如我們所見，它們具有遞歸定義，并享有類似的結(jié)構(gòu)歸納原則。

2 信號流圖演算

本文的主題是一種特定的字符串圖語法，稱為信號流圖演算。我們將看到，正如其名所示，這種語法適用于對信號流圖進(jìn)行代數(shù)推理；信號流圖是控制理論和工程中一種眾所周知的基礎(chǔ)結(jié)構(gòu)（參見例如 [58, 45]）。

固定一個(gè)半環(huán) R R，信號流圖演算的幺半簽名如下：

例 2. 考慮下面的兩個(gè)電路。

2.1 反饋與經(jīng)典信號流圖

注 1. 讀者可能已經(jīng)在 (5) 中識別出了跡（trace）[38] 的結(jié)構(gòu)。事實(shí)上，用帶跡幺半范疇（traced monoidal categories）[34] 來建模帶有反饋的系統(tǒng)是一種傳統(tǒng)。這些結(jié)構(gòu)的代數(shù)核心也在迭代理論 [8] 和 Stefanescu 的網(wǎng)絡(luò)代數(shù) [60] 的背景下被研究過。就信號流圖這一更具體的設(shè)定而言，先前的范疇方法大多基于余代數(shù)理論 [55, 7, 46]。此處提出的字符串圖方法（起源于 [15]，隨后在 [3] 中被獨(dú)立提出）的一個(gè)顯著特征是采用了更抽象的框架 ，該框架包含了比經(jīng)典信號流圖（它們構(gòu)成子范疇）更多的電路圖。正如我們將在第 4 節(jié)和第 5 節(jié)中看到的那樣，這種增加的一般性是以使操作分析變得更加微妙為代價(jià)的。其回報(bào)是一種更初等的語法 (4)，它不包含任何用于遞歸的原語，并且有可能實(shí)現(xiàn)一種簡潔的公理化系統(tǒng)（第 3.1 節(jié)），該系統(tǒng)基于諸如雙幺半群（bimonoids）和弗羅貝尼烏斯半群（Frobenius monoids）等眾所周知的代數(shù)結(jié)構(gòu)。

3 指稱語義

在這里，我們?yōu)殡娐放鋫淞艘环N指稱語義（denotational semantics），即為每個(gè)電路分配一個(gè)適當(dāng)數(shù)學(xué)宇宙中的元素。

指稱語義為電路 c c 分配一個(gè)軌跡（trajectories）關(guān)系，該關(guān)系對應(yīng)于 c c 的所有可能執(zhí)行。同樣，對于人們可能視為“執(zhí)行”的內(nèi)容也有不同的選擇，這為我們提供了語義模型的另一個(gè)維度。文獻(xiàn)中主要研究的兩種情況是：過去有限、未來無限的執(zhí)行——等價(jià)于假設(shè)執(zhí)行從 0 初始化的寄存器開始——以及雙無限軌跡，等價(jià)于（額外）考慮寄存器在任何時(shí)刻都可以持有任意初始值的執(zhí)行。在引入了電路的形式操作語義后，我們將在注 5 中使這些觀測更加精確。

過去有限、未來無限軌跡的集合是 k k 上的洛朗級數(shù)（Laurent series）域 。事實(shí)上，洛朗級數(shù) σ σ 可以被理解為一個(gè)流（stream），即 k k-元素的無限序列

我們可以以一種與軌跡無關(guān)的方式來定義指稱語義：

3.1 交互霍普夫代數(shù)：電路的等式理論

如圖 1所示，該等式理論由以下“模塊”組成：

• 在第一個(gè)模塊中，黑色結(jié)構(gòu)和白色結(jié)構(gòu)均構(gòu)成交換半群（commutative monoids）和交換余幺半群（comonoids），分別刻畫了加法和復(fù)制的性質(zhì)。
• 在第二個(gè)模塊中，白色幺半群與黑色余幺半群以雙幺半群（bimonoid）的形式進(jìn)行交互。正如 [41] 所示，雙幺半群是幺半群與余幺半群相互作用的兩種規(guī)范方式之一。

注 4（Kleene 定理）。 定理 3 的最后一點(diǎn)可以被視為正則語言 Kleene 定理的類比：它提供了對有理行為的語法刻畫。所表示的關(guān)系是性質(zhì)特別良好的函數(shù)，因?yàn)樗鼈儗?shí)際上并不需要洛朗級數(shù)的全部一般性：任何有理多項(xiàng)式都會(huì)生成一個(gè)有限冪級數(shù)，而無需“有限的過去”。（正統(tǒng)）信號流圖與有理矩陣之間的對應(yīng)關(guān)系是眾所周知的（參見例如 [54]）：在此，我們給出了這一刻畫的范疇論及字符串圖論解釋，其中“輸入”、“輸出”和流向等概念都是衍生出來的。

我們還要提到，定理 3 的第 1 點(diǎn)似乎是一個(gè)民間結(jié)果（folklore result），以各種形式普遍出現(xiàn)在文獻(xiàn)中 [42, 36, 52, 48, 41, 63]。

4 操作語義

就像編程語言一樣，指稱語義只是賦予電路語法形式化意義的一種方式。在本節(jié)中，我們采取不同的視角，將電路視為基于狀態(tài)的機(jī)器，其逐步執(zhí)行過程即為操作語義。

在更深層次上，例 6 表明操作語義并非旨在對所有電路都可執(zhí)行：順序組合的規(guī)則隱式地對中間值 v v 進(jìn)行了存在量詞量化，從而導(dǎo)致了潛在的無界非確定性。令人滿意地理解這一現(xiàn)象是下一節(jié)的主題。作為初步觀察，值得注意的是，如果將限制放寬到無限計(jì)算，那么例 6 中概述的不匹配就會(huì)消失，并且我們在操作等價(jià)性和指稱等價(jià)性之間建立了完美的對應(yīng)關(guān)系。

為了陳述這一結(jié)果，我們引入一個(gè)預(yù)備概念。按照控制理論中的慣例，我們考慮軌跡（trajectories）：即可能從過去開始的跡（traces）。

注 5. 我們特意使用了與指稱語義中相同的術(shù)語“軌跡”（trajectories）：事實(shí)上，從初始狀態(tài)開始的計(jì)算與我們在第 3 節(jié)中遇到的洛朗級數(shù)之間存在著密切的聯(lián)系。

事實(shí)上，任何端口上的觀測序列顯然都是一個(gè)洛朗級數(shù)——任何計(jì)算都可以平凡地（即具有 0 次觀測）無限地向過去延續(xù)，正如定義 6 中的 (10) 所反映的那樣。人們可以推廣計(jì)算的概念，使其不必從初始化狀態(tài)開始：在這種情況下，相應(yīng)的軌跡概念 (10) 可能是一個(gè)真正的雙無限序列，即 σ σ 在過去可能是無限的。更多細(xì)節(jié)請參見 [31, 30]。

5 可實(shí)現(xiàn)性

鑒于例 6，人們可能會(huì)問常見的死鎖情況（如 (9) 中的情況）以及需要從過去開始的計(jì)算（如 (8) 中的情況）有多普遍。事實(shí)證明，當(dāng)考慮 adheres to 經(jīng)典信號流圖概念的電路子類 的操作語義時(shí)，這些問題是可以避免的。

5.1 信號流的組合性與方向性

因此，電路、其代數(shù)理論及其組合語義可以被視為一種真正的信號流過程代數(shù)，既可用作規(guī)范（specifications）語言，也可用作（可執(zhí)行的）實(shí)現(xiàn)（implementations）語言。事實(shí)上，該語言適用于形式化方法技術(shù)，如細(xì)化（refinement），參見 [10]。

6 仿射擴(kuò)展

工程師通常不區(qū)分線性和仿射（affine）系統(tǒng)，因?yàn)檠芯窟@兩者的數(shù)值方法實(shí)質(zhì)上是相同的。然而，從我們的角度來看，這種區(qū)分很重要，因?yàn)闉榱吮磉_(dá)仿射行為，我們需要擴(kuò)展信號流圖演算以及迄今為止闡述的主要結(jié)果。這種擴(kuò)展被證明極其有趣，因?yàn)橐环矫妫沟媚軌驅(qū)哂懈S富行為模式的系統(tǒng)進(jìn)行建模，例如第 7 節(jié)中的電流和電壓源或第 8 節(jié)中的互斥；另一方面，它允許定義上下文等價(jià)（contextual equivalence），并將定理 4 轉(zhuǎn)化為一個(gè)恰當(dāng)?shù)耐耆橄蠼Y(jié)果（full abstraction result）（定理 8）。

6.1 完全抽象

仿射擴(kuò)展的第一個(gè)回報(bào)是能夠?yàn)殡娐穲D制定上下文等價(jià)（contextual equivalence）的概念，從而得出一個(gè)完全抽象結(jié)果（full abstraction result）。

為此，我們首先將操作語義擴(kuò)展到語法。這相當(dāng)于用以下內(nèi)容擴(kuò)充圖 2 中的規(guī)則：

7 電路

采用抽象且非常初等的電路語法的一個(gè)主要優(yōu)勢在于，信號流圖變成了其中可以研究的計(jì)算模型之一。在本節(jié)中，我們將聚焦于電路，展示如何在中對它們進(jìn)行建模。在下一節(jié)中，我們將簡要說明另一種不同的模型——Petri 網(wǎng)——如何也能得到類似的描述。

基礎(chǔ)電氣工程專注于開放線性電路分析。

正如我們所見，這是在仿射演算中表示空關(guān)系的方式。串聯(lián)電流源（第一列，最后一行）的情況也是如此。

注 8. 關(guān)于在仿射電路圖中編碼電路的更多細(xì)節(jié)，讀者可參閱 [13]。Baez 和 Coya [37, 26] 給出了類似的語義，他們建立在 Baez、Erbele 和 Fong [3, 6] 以及 Rosebrugh、Sabadini 和 Walters [53] 的工作之上。然而，這些工作僅考慮無源線性電路，即不含電壓源和電流源的電路。

8 從控制理論到并發(fā)

我們已經(jīng)表明，信號流圖演算允許對一類重要的行為（線性動(dòng)力系統(tǒng)）進(jìn)行公理化，從而捕捉了一個(gè)眾所周知的既有組合模型（信號流圖）。該方法是組合式的，允許開放系統(tǒng)的語法表示并強(qiáng)調(diào)其代數(shù)性質(zhì)，但同時(shí)又是圖形化的，強(qiáng)調(diào)其連接拓?fù)浜徒M合性質(zhì)。

從歷史上看，對這些方面的不同側(cè)重導(dǎo)致了并發(fā)系統(tǒng)分析中不同的研究脈絡(luò)。一方面，我們有進(jìn)程演算（process calculi）[47, 56, 35] 提出的代數(shù)方法。另一方面，存在并發(fā)行為的圖形模型傳統(tǒng)，例如 Petri 網(wǎng)（參見例如 [50]）。

因此，信號流圖演算似乎可以作為進(jìn)程演算和圖形模型所提供的視角之間的中間地帶。這促使我們 [11] 使用與信號流理論中分析線性行為相同的圖解方法來分析并發(fā)系統(tǒng)。

最令人驚訝的是，從線性行為過渡到并發(fā)行為時(shí)，設(shè)置可能基本保持不變：人們可以使用語法 (4) 的相同生成元，唯一顯著的變化是通過一組不同的信號來建模其行為，即從域 k k 過渡到自然數(shù)半環(huán) N N。

為了解釋這一點(diǎn)，我們展示了來自 [13] 和 [11] 的兩個(gè)例子。

這些觀察結(jié)果已在資源演算（resources calculus）[51, 11] 中得到結(jié)晶：其語法與信號流圖演算相同，但信號宇宙被固定為 N N。這種切換迫使人們從線性關(guān)系轉(zhuǎn)向加法關(guān)系，并因此改變公理化系統(tǒng) [11]。在 [13] 中，證明了無狀態(tài)連接器的代數(shù) [20] 可以很容易地編碼到資源演算的（仿射擴(kuò)展）中。[11] 展示了資源演算內(nèi)對 Petri 網(wǎng)的擴(kuò)展研究。這提供了一種深刻的理解，即將 Petri 網(wǎng)視為線性動(dòng)力系統(tǒng)（但是在 N N 上），以及一種優(yōu)雅的組合操作語義。相反，指稱語義似乎具有挑戰(zhàn)性，肯定值得進(jìn)一步研究。

9 本研究與 IFIP AICT 600 - IFIP 60 周年慶典專刊

本文所述的研究與兩個(gè) TC1 工作組的興趣相交叉：IFIP-WG 1.3 系統(tǒng)規(guī)范基礎(chǔ)組和 IFIP-WG 1.8 并發(fā)理論組。它也涉及 TC2 的主題，與 IFIP-WG 2.2 編程概念的形式描述相關(guān)。首先，信號流圖是一種簡單但普遍的計(jì)算模型。這里描述的二維方法足夠靈活，能夠使字符串圖語法既表達(dá)形式規(guī)范又表達(dá)實(shí)現(xiàn)。公理化特征意味著前者可以以有原則的方式轉(zhuǎn)化為后者。此外，我們給出的操作語義是一種并發(fā)進(jìn)程代數(shù)，并且——在仿射擴(kuò)展中——我們探討了其對 Petri 網(wǎng)語義研究的影響，Petri 網(wǎng)是并發(fā)的經(jīng)典模型。最后，對指稱方法和操作方法之間交互的強(qiáng)調(diào)——重點(diǎn)關(guān)注組合性——源于形式編程語言語義的研究，但在理論計(jì)算機(jī)科學(xué)中正變得越來越重要。

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