Enhanced Formal Reasoning for Algebraic Network Theory

Lead Research Organisation: University College London
Department Name: Computer Science

Abstract

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.

Planned Impact

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).

Publications

10 25 50
 
Description Diagrammatic algebraic theory are an increasingly relevant research area of theoretical computer science, whose aim is to provide a mathematical framework to reason uniformly about different kinds of networks. This project is about developing new methodologies to reason about diagrammatic theories, and at the same time broaden the scope of this approach to cover new applications.

We can list four main findings of the project at this stage:

Finding #1 (Methods): a sound and complete implementation of rewriting in diagrammatic theories in which there are multiple Frobenius structures (results published and presented at LICS'18).

Finding #2 (Methods): a modular characterisation of cartesian algebraic theories (published in JLAMP, 2018) and of theories of relations (published in LMCS, 2018) using distributive laws and other composition operation on diagrammatic algebras.

Finding #3 (Applications): a novel diagrammatic algebra for concurrent systems, which encompasses Petri nets. Remarkably, this algebra is essentially the same used in previous work to model linear dynamical systems, and thus suggests new connections between concurrency theory and control theory. These results were published and presented at POPL'19.

Finding #4 (Applications): the PI wrote with Prof. Bart Jacobs a chapter of a forthcoming book on the foundations of probabilistic programming, published by Cambridge University Press. It's not a properly new finding, but it is a significant step in the process of disseminating our research on diagrammatic techniques for Bayesian probability to a much wider audience.

Finding #5 (Tools): a new software for assisted diagrammatic reasoning called CARTOGRAPHER (http://cartographer.id/). The development of CARTOGRAPHER rests on the rewriting techniques developed in Finding#1. An overview of the tool was accepted for publication and presented at CALCO'19.
Exploitation Route Findings #1 and #2 advance our understanding of distributive laws and diagram rewriting: they will be pivotal in further developing CARTOGRAPHER, a tool for assisted diagrammatic reasoning that was created by the project's team.

Finding #3 enables new forms of compositional reasoning about concurrent systems, which are yet to be explored and understood in full. One way forward is extending this framework to model more core scenarios of concurrency such as mutual exclusion. There are very promising preliminary results on this thread appearing at LICS'19, CONCUR'19 and FoSSaCS'20.

Finding #4 will make our research on Bayesian probability more popular in the probabilistic programming community. Feedback by individuals in that area show that the language we propose is perceived as more flexible, expressive and semantically clear than the traditional formalisms of probability theory, so the hope is that it is taken up by practitioners.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description This is a theoretical project and its short-term impact is mostly academic. Nonetheless, the compositional approach to Petri nets presented in the publication at POPL'19 has already attracted the interest of Statebox, a startup company that intends to use the findings of this research area to develop blockchain technology (https://statebox.org/). In particular, the way in which Petri nets are modelled in our work shows promise in improving the algorithms that are currently being developed at Statebox. Similarly, the newly developed tool CARTOGRAPHER (http://cartographer.id/) is attracting the interested of practitioners and we are currently working on expanding its features.
First Year Of Impact 2019
Sector Digital/Communication/Information Technologies (including Software)
 
Description Rewriting theory of Frobenius structures 
Organisation Radboud University Nijmegen
Country Netherlands 
Sector Academic/University 
PI Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Collaborator Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Impact Scientific articles, presentations in international conferences and workshops
Start Year 2018
 
Description Rewriting theory of Frobenius structures 
Organisation University of Pisa
Department Department of Computer Science
Country Italy 
Sector Academic/University 
PI Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Collaborator Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Impact Scientific articles, presentations in international conferences and workshops
Start Year 2018
 
Description Rewriting theory of Frobenius structures 
Organisation University of Southampton
Department School of Electronics and Computer Science Southampton
Country United Kingdom 
Sector Academic/University 
PI Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Collaborator Contribution Research expertise, writing scientific articles, dissemination in seminars, conferences and workshops
Impact Scientific articles, presentations in international conferences and workshops
Start Year 2018
 
Description String diagrams for probabilistic computation and causal inference 
Organisation Radboud University Nijmegen
Country Netherlands 
Sector Academic/University 
PI Contribution Research expertise, writing of scientific articles and a book chapter, dissemination in seminars, workshops and conferences, feedback from practitioners at UCL.
Collaborator Contribution Research expertise, writing of scientific articles and a book chapter, dissemination in seminars, workshops and conferences, feedback from local practitioners at Radboud University Nijmegen.
Impact Journal articles, book chapter, invitation to organise a special issue of the Journal of Approximate Reasoning (Elsevier) as a guest editor.
Start Year 2018
 
Title cartographer --- a tool for string diagrammatic reasoning 
Description See overview at http://drops.dagstuhl.de/opus/volltexte/2019/11448 
Type Of Technology Webtool/Application 
Year Produced 2019 
Impact Started collaboration with Statebox Inc., which is interested in developing and exploiting the tool at the industrial scale. 
URL http://drops.dagstuhl.de/opus/volltexte/2019/11448
 
Description Organisation of international workshop on 'Compositional Methods for Network Diagrams and Component-Based Systems' 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact This edition of the Bellairs workshop series brought together scientists whose work in diverse fields (including quantum theory, control theory, concurrency, circuit theory, database theory, Bayesian probability and natural language processing) takes place within a common mathematical framework, based on monoidal category theory and inspired by programming language semantics.

Each of the participants gave a seminar and there was ample space for discussion. New scientific collaborations started at the workshop. Also, postgraduate students were present at the workshop and received a thorough training on the state of the art in the field.
Year(s) Of Engagement Activity 2018
URL http://zanasi.com/fabio/bellairs18.html