Showing 1–2 of 2 results for author: Quick, D
-
A first-order logic for string diagrams
Authors:
Aleks Kissinger,
David Quick
Abstract:
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been larg…
▽ More
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic called with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
△ Less
Submitted 2 May, 2015;
originally announced May 2015.
-
Tensors, !-graphs, and non-commutative quantum structures (extended version)
Authors:
Aleks Kissinger,
David Quick
Abstract:
!-graphs provide a means of reasoning about infinite families of string diagrams and have proven useful in manipulation of (co)algebraic structures like Hopf algebras, Frobenius algebras, and compositions thereof. However, they have previously been limited by an inability to express families of diagrams involving non-commutative structures which play a central role in algebraic quantum information…
▽ More
!-graphs provide a means of reasoning about infinite families of string diagrams and have proven useful in manipulation of (co)algebraic structures like Hopf algebras, Frobenius algebras, and compositions thereof. However, they have previously been limited by an inability to express families of diagrams involving non-commutative structures which play a central role in algebraic quantum information and the theory of quantum groups. In this paper, we fix this shortcoming by offering a new semantics for non-commutative !-graphs using an enriched version of Penrose's abstract tensor notation.
△ Less
Submitted 4 March, 2015;
originally announced March 2015.
