EPSRC Reference: 
EP/V001612/1 
Title: 
Nominal String Diagrams 
Principal Investigator: 
Ghica, Dr DR 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
School of Computer Science 
Organisation: 
University of Birmingham 
Scheme: 
Standard Research 
Starts: 
01 July 2020 
Ends: 
30 June 2023 
Value (£): 
429,879

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 

Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
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 onedimensional (term) and twodimensional (graph) syntax, exploiting the existence of shared mathematical structures (called 'monoidal categories'). However, the onedimensional 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 nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

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 