| EPSRC Reference: |
EP/V001612/1 |
| Title: |
Nominal String Diagrams |
| Principal Investigator: |
Ghica, Professor DR |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| 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: |
|
| 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 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
|
|
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 |