Nominal String Diagrams

Notations are the formal manifestation of thought. Conventionally, the established idea of 'notation' is one dimensional, as a sequence of symbols; but the last decade has seen a very exciting development: formal two dimensional notations, based on graphs.

"String diagrams" represent a mathematical connection between one-dimensional (term) and two-dimensional (graph) syntax, exploiting the existence of shared mathematical structures (called 'monoidal categories'). However, the one-dimensional manifestation of a string diagram, as it emerges from the mathematical theory, is not always the most practical or most convenient for people to manipulate.

Graph languages have been developed independently in other contexts, for example digital circuit specifications, from rather different principles. The popularity of these notations suggests that in some sense they more appealing, yet these notations lack structure and are difficult to reason about mathematically. Graphical programming languages have been proposed numerous times and for a long time, but they consistently failed to reach the mainstream of programming. These recurring attempts testify to the fact that such languages are attractive, yet their failure shows that getting them right is not exactly easy. The mathematical structure of programming languages also has diagrammatic and graphical counterparts, but these have not been yet studied enough. These are "hierarchical" structures in which diagram graphs can nest or can even be used as labels of nodes in other graphs.

In this proposal we aim to reconcile both kinds of notations, as emerging from the mathematics of string diagrams and from the practicalities of circuit and system design. The key idea that can bring these two together is the concept of 'name'. Names, used as labels, can greatly simplify certain term representations of graphs and make algorithmic processing of such terms easier. The mathematical theory of names ('nominal theory') is subtle, but by now quite well understood. We believe that nominal theory can bring together term and graph manipulation, via rewriting, in an elegant and effective way. And we further believe that this unify theory will lead to new insights into theoretical (and practical) models of digital circuits and other kind of systems.

Zanasi is an expert in the theoretical aspects of string diagrams, Silva is an expert in nominal techniques, and Ghica is an expert in practical applications of string diagrams to language and circuit analysis.

This research is foundational, aiming ultimately at designing better syntactical mechanisms unifying one-dimensional (term) and two-dimensional (graph) formalisms. Additionally, we plan to mathematically understand this synthesis of the two notations using nominal techniques, category theory, and graph rewriting.

Therefore the main impact we expect is on knowledge. We will maximise this impact by involving four leading international researchers (from UK, Italy, USA, and Japan) as collaborators, as well as two companies. One of the companies (IOHK) will be involved exclusively with impact generation.

The research will also have an impact on People. The project will employ two full time research fellows which will gain valuable training in the areas covered by the grant, as well as research skills in general. University of Birmingham has ear-marked one PhD studentship to work in association with this project, therefore training another young researcher. University of Birmingham will also hire three undergraduate research interns for the duration of the summer, training them into leading-edge research-oriented software development.

Our project is forward-looking and is set to address in a principled way realistic problems that are likely to become economically relevant in the future, as recognised by the letter of support from our industry partners, Statebox Inc and IOHK.

In order to enhance economic impact in the medium and long term we will develop existing contacts with companies such as Xilinx, Altera, Jane Street and Facebook to promote our diagrammatic tools for software and hardware analysis and synthesis.