Enhanced Formal Reasoning for Algebraic Network Theory

图解语言被用于科学的不同领域，以说明和研究基于交互组件的系统。在突出系统各部分之间的连接和资源交换方面，图形的表现优于文本信息。这使得图语言在分析计算机物理系统、并发系统和量子系统中的微妙相互作用时特别有效。近年来，代数网络理论作为一个统一的数学框架出现，其中图语言被赋予完全形式化的地位，并使用代数程序语义的组合方法进行研究。如今，代数方法在量子理论、语言学、并发理论以及信号处理、电路和数字电路的分析等领域都有应用。这一提议旨在使这一框架内的图解推理更具可扩展性、数学健壮性和更易于实现。我们的方法是基于重写技术和模块化技术的集成，重写技术强调图解推理的算法方面，模块化技术更适合于证明吸引人的数学性质。由此产生的技术-打算取两个世界的最好-然后将被应用于代数网络理论的及时应用领域，包括量子过程的图解演算、信号处理电路和贝叶斯网络。

Diagrammatic languages are used in diverse fields of science to specify and study systems based on interacting components. Graphics outperforms textual information in highlighting connectivity and resource-exchange between parts of a system. This makes diagrammatic languages particularly effective in the analysis of subtle interactions as those found in cyber-physical, concurrent and quantum systems.In recent years "algebraic network theory" emerged as a unifying mathematical framework in which diagrammatic languages are given a completely formal status and are studied using the compositional methods of algebraic program semantics. Nowadays the algebraic approach founds application in fields as diverse as quantum theory, linguistics, concurrency theory and the analysis of signal processing, electrical and digital circuits. This proposal aims at making diagrammatic reasoning within this framework more scalable, mathematically robust and easier to implement. Our approach is based on the integration of rewriting techniques, which emphasise the algorithmic aspects of diagrammatic reasoning, and modular techniques, which are more adapted to prove appealing mathematical properties. The resulting technology - which intends to take the best from the two worlds - will be then applied to timely areas of application for algebraic network theory, including diagrammatic calculi for quantum processes, signal processing circuits and Bayesian networks.