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.

Because the project has a significant theoretical component, our realistic expectation for short-term impact is within the academic community. Still, academic impact will be particularly broad, as the diagrammatic theories that our project will inform are found across really diverse disciplines: we make a few examples of this diversity in the "Academic Beneficiaries" section of Je-S and in the "Background" section of the "Call for Support".

As our proposal shares the mathematical background of these theories, our formal tools will be immediately applicable, empowering diagrammatic reasoning and making the algebraic approach more appealing as a unifying framework in which diverse systems can be studied compositionally. This work will make algebraic theories of diagrams easier to design, implement and reason with in a mathematically rigorous manner. We will not only foster research in areas where such theories are already established, but also promote the approach in new areas, such as Bayesian inference.

In the longer term, we expect the proposed work to have impact beyond academia, more specifically in the way in which industrial software for component-based system modelling is designed. Indeed, algebraic network theory is a foundation for systems with interacting components, and we put particular emphasis in devising formal methodologies that are both scalable (the contribution of modular techniques) and oriented to implementation (the contribution of rewriting techniques). These characteristics work towards making theory-driven methods applicable in an industrial context. As our theory is based on a diagrammatic language, it will inform graphical programming environments (such as SIMULINK and its extension STATEFLOW), offering new possibilities for diagrammatic reasoning and its validation. An intriguing ramification is the one concerning probabilistic systems, on which our work will offer an original perspective (WP6) that may stimulate new directions for software design.

A last point to mention is the impact of the project on the general public. Diagrammatic languages are worth researching for conceptual reasons (the emphasis on resource-sensitivity, compositionality and connectivity) but their pedagogical significance is easily overlooked. In many cases diagrams convey in a simpler way than text unintuitive phenomena that appear in (quantum, concurrent) computation. The theoretical development of diagrammatic languages will foster their use in the research community and thus make scientific discoveries accessible to a broader audience. This is already happening for instance in quantum theory, which in Oxford is taught with graphical reasoning (cf. "Picturing Quantum Processes", Coecke and Kissinger, Cambridge University Press 2017).