Search

In the graphical calculus of planar string diagrams, equality is generated by exchange moves, which swap the heights of adjacent vertices. We show that left- and right-handed exchanges each give strongly normalizing rewrite strategies for connected string diagrams. We use this result to give a linear-time solution to the equivalence problem in the connected case, and a quadratic solution in the general case. We also give a stronger proof of the Joyal-Street coherence theorem, settling Selinger's conjecture on recumbent isotopy.

Goyeneche et al recently proposed a notion of orthogonality for quantum Latin squares, and showed that orthogonal quantum Latin squares yield quantum codes. We give a simplified characterization of orthogonality for quantum Latin squares, which we show is equivalent to the existing notion. We use this simplified characterization to give an upper bound for the number of mutually orthogonal quantum Latin squares of a given size, and to give the first examples of orthogonal quantum Latin squares that do not arise from ordinary Latin squares. We then discuss quantum Latin isometry squares, generalizations of quantum Latin squares recently introduced by Benoist and Nechita, and define a new orthogonality property for these objects, showing that it also allows the construction of quantum codes. We give a new characterization of unitary error bases using these structures.

We give a scheme for interpreting shaded tangles as quantum programs, with the property that isotopic tangles yield equivalent programs. We analyze many known quantum programs in this way—including entanglement manipulation and error correction—and in each case present a fully-topological formal verification, yielding in several cases substantial new insight into how the program works. We also use our methods to identify several new or generalized procedures.

We give a tight scheme for teleporting a quantum state between two parties whose reference frames are misaligned by an action of a finite symmetry group. Unlike previously proposed schemes, ours requires no additional tokens or data to be passed between the participants; the same amount of classical information is transferred as for ordinary quantum teleportation, and the Hilbert space of the entangled resource is of the same size. In the terminology of Peres and Scudo, our protocol relies on classical communication of unspeakable information.

We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. This is an extended abstract for arXiv:1601.05372.

We prove coherence theorems for Frobenius pseudomonoids and snakeorators in monoidal bicategories. As a consequence we obtain a 3d notation for proofs in nonsymmetric multiplicative linear logic, with a geometrical notion of equivalence, and without the need for a global correctness criterion or thinning links. We argue that traditional proof nets are the 2d projections of these 3d diagrams.

We give a mathematical analysis of a new type of classical computer network architecture, intended as a model of a new technology that has recently been proposed in industry. Our approach is based on groubits, generalizations of classical bits based on groupoids. This network architecture allows the direct execution of a number of protocols that are usually associated with quantum networks, including teleportation, dense coding and secure key distribution.

This article introduces Globular, an online proof assistant for the formalization and verification of proofs in higher-dimensional category theory. The tool produces graphical visualizations of higher-dimensional proofs, assists in their construction with a point-and- click interface, and performs type checking to prevent incorrect rewrites. Hosted on the web, it has a low barrier to use, and allows hyperlinking of formalized proofs directly from research papers. It allows the formalization of proofs from logic, topology and algebra which are not formalizable by other methods, and we give several examples.

This paper explores the use of 2-categorical technology for describing and reasoning about complex quantum procedures. We give syntactic definitions of a family of complementary measurements, and of quantum key distribution, and show that they are equivalent. We then show abstractly that either structure gives a solution to the Mean King problem, which we also formulate 2-categorically.

We show that a pair of complementary dagger-Frobenius algebras, equipped with a self-conjugate comonoid homomorphism onto one of the algebras, produce a nontrivial unitary morphism on the product of the algebras. This gives an abstract understanding of the structure of an oracle in a quantum computation, and we apply this understanding to develop a new algorithm for the deterministic identification of group homomorphisms into abelian groups. We also discuss an application to the categorical theory of signal-flow networks.

There are two ways to describe the interaction between classical and quantum information categorically: one based on completely positive maps between Frobenius algebras, the other using symmetric monoidal 2-categories. This paper makes a first step towards combining the two. The integrated approach allows a unified description of quantum teleportation and classical encryption in a single 2-category, as well as a universal security proof applicable simultaneously to both scenarios.