一句话:通过仿射连接子扩展图形线性代数,给出图形仿射代数在自然数模与域上模两类语义下的完备公理化。
图形线性代数是用于组合式推理线性计算设备的图解语言。本文为其引入仿射连接子,提出图形仿射代数,以刻画更丰富的仿射行为。该扩展虽简单却颇具表达力:当语义域为自然数模时可建模互斥等模式,当语义域为某类域上模时可建模非无源电子元件。作者的主要技术贡献是针对这两类解释给出完整的公理化,即建立可靠且完备的等式理论。案例研究进一步表明,图形仿射代数可刻画电路以及无状态连接子演算——一种面向分布式系统的协调语言。
Graphical linear algebra is a diagrammatic language allowing to reason compositionally about different types of linear computing devices. In this paper, we extend this formalism with a connector for affine behaviour. The extension, which we call graphical affine algebra, is simple but remarkably powerful: it can model systems with richer patterns of behaviour such as mutual exclusion-with modules over the natural numbers as semantic domain-or non-passive electrical components-when considering modules over a certain field. Our main technical contribution is a complete axiomatisation for graphical affine algebra over these two interpretations. We also show, as case studies, how graphical affine algebra captures electrical circuits and the calculus of stateless connectors-a coordination language for distributed systems.