EPSRC logo

Details of Grant 

EPSRC Reference: EP/V001612/1
Title: Nominal String Diagrams
Principal Investigator: Ghica, Professor DR
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Chapman University IOHK Kyoto University
Statebox.IO B.V. University of Oxford University of Pisa
Department: School of Computer Science
Organisation: University of Birmingham
Scheme: Standard Research
Starts: 01 December 2020 Ends: 31 May 2024 Value (£): 429,879
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
20 May 2020 EPSRC ICT Prioritisation Panel May 2020 Announced
Summary on Grant Application Form
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.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.bham.ac.uk