Reasoning with !-graphs
<p>The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of indu...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2013
|
| Subjects: |
| _version_ | 1826316450310127616 |
|---|---|
| author | Merry, A |
| author2 | Abramsky, S |
| author_facet | Abramsky, S Merry, A |
| author_sort | Merry, A |
| collection | OXFORD |
| description | <p>The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories.</p> <p>String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string <em>graphs</em> has provided a combinatorial formalisation of string diagrams, laying the foundations for this project.</p> <p>The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning.</p> <p>This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation – and structures to encode it – to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs.</p> <p>This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.</p> |
| first_indexed | 2024-03-07T07:46:41Z |
| format | Thesis |
| id | oxford-uuid:416c2e6d-2932-4220-8506-50e6b403b660 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-12-09T03:45:20Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | oxford-uuid:416c2e6d-2932-4220-8506-50e6b403b6602024-12-07T17:05:20ZReasoning with !-graphsThesishttp://purl.org/coar/resource_type/c_db06uuid:416c2e6d-2932-4220-8506-50e6b403b660Theory and automated verificationProgram development and toolsMathematical logic and foundationsApplications and algorithmsQuantum theory (mathematics)Computer science (mathematics)EnglishOxford University Research Archive - Valet2013Merry, AAbramsky, SCoecke, B<p>The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories.</p> <p>String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string <em>graphs</em> has provided a combinatorial formalisation of string diagrams, laying the foundations for this project.</p> <p>The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning.</p> <p>This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation – and structures to encode it – to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs.</p> <p>This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.</p> |
| spellingShingle | Theory and automated verification Program development and tools Mathematical logic and foundations Applications and algorithms Quantum theory (mathematics) Computer science (mathematics) Merry, A Reasoning with !-graphs |
| title | Reasoning with !-graphs |
| title_full | Reasoning with !-graphs |
| title_fullStr | Reasoning with !-graphs |
| title_full_unstemmed | Reasoning with !-graphs |
| title_short | Reasoning with !-graphs |
| title_sort | reasoning with graphs |
| topic | Theory and automated verification Program development and tools Mathematical logic and foundations Applications and algorithms Quantum theory (mathematics) Computer science (mathematics) |
| work_keys_str_mv | AT merrya reasoningwithgraphs |