1. The GHZ/W-Calculus Contains Rational Arithmetic. Bob Coecke, Aleks Kissinger, Alex Merry, and Shibdas Roy. pdf | abstract »
    Graphical calculi provide an intuitive, compositional way to express and manipulate quantum states and processes. They also provide a bridge to automated techniques for reasoning and computation via graph rewriting. The power of these calculi stems from the fact that they subsume a wide range of symmetries in the structure of quantum operations such as the Choi-Jamiolkowski isomorphism. One such calculus takes the GHZ and W states as its basic generators. Here we show that this language allows one to encode standard rational arithmetic, with the GHZ state as multiplication, the W state as addition, the Pauli X gate as multiplicative inversion, and the Pauli Z gate as additive inversion.
  2. Open Graphs and Monoidal Theories. Lucas Dixon, Aleks Kissinger. arXiv:1011.4114 | abstract »
    String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks, and many other compositional structures. The distinguishing feature of these diagrams is that edges need not be connected to vertices at both ends, and these unconnected ends can be interpreted as the inputs and outputs of a diagram. In this paper, we give a concrete construction for string diagrams using a special kind of typed graph called an open-graph. While the category of open-graphs is not itself adhesive, we introduce the notion of a selective adhesive functor, and show that such a functor embeds the category of open-graphs into the ambient adhesive category of typed graphs. Using this functor, the category of open-graphs inherits “enough adhesivity” from the category of typed graphs to perform double-pushout (DPO) graph rewriting. A salient feature of our theory is that it ensures rewrite systems are “type-safe” in the sense that rewriting respects the inputs and outputs. This formalism lets us safely encode the interesting structure of a computational model, such as evaluation dynamics, with succinct, explicit rewrite rules, while the graphical representation absorbs many of the tedious details. Although topological formalisms exist for string diagrams, our construction is discreet, finitary, and enjoys decidable algorithms for composition and rewriting. We also show how open-graphs can be parameterised by graphical signatures, similar to the monoidal signatures of Joyal and Street, which define types for vertices in the diagrammatic language and constraints on how they can be connected. Using typed open-graphs, we can construct free symmetric monoidal categories, PROPs, and more general monoidal theories. Thus open-graphs give us a handle for mechanised reasoning in monoidal categories.
  3. Open Graphs and Computational Reasoning. Lucas Dixon, Ross Duncan, Aleks Kissinger. In Proceedings DCM 2010. arXiv:1007.3794 | abstract »
    We present a form of algebraic reasoning for computational objects which are expressed as graphs. Edges describe the flow of data between primitive operations which are represented by vertices. These graphs have an interface made of half-edges (edges which are drawn with an unconnected end) and enjoy rich compositional principles by connecting graphs along these half-edges. In particular, this allows equations and rewrite rules to be specified between graphs. Particular computational models can then be encoded as an axiomatic set of such rules. Further rules can be derived graphically and rewriting can be used to simulate the dynamics of a computational system, e.g. evaluating a program on an input. Examples of models which can be formalised in this way include traditional electronic circuits as well as recent categorical accounts of quantum information.
  4. The compositional structure of multipartite quantum entanglement. Bob Coecke, Aleks Kissinger. arXiv:1002.2540 | abstract »
    While multipartite quantum states constitute a (if not the) key resource for quantum computations and protocols, obtaining a high-level, structural understanding of entanglement involving arbitrarily many qubits is a long-standing open problem in quantum computer science. In this paper we expose the algebraic and graphical structure of the GHZ-state and the W-state, as well as a purely graphical distinction that characterises the behaviours of these states. In turn, this structure yields a compositional graphical model for expressing general multipartite states. We identify those states, named Frobenius states, which canonically induce an algebraic structure, namely the structure of a commutative Frobenius algebra (CFA). We show that all SLOCC-maximal tripartite qubit states are locally equivalent to Frobenius states. Those that are SLOCC-equivalent to the GHZ-state induce special commutative Frobenius algebras, while those that are SLOCC-equivalent to the W-state induce what we call anti-special commutative Frobenius algebras. From the SLOCC-classification of tripartite qubit states follows a representation theorem for two dimensional CFAs. Together, a GHZ and a W Frobenius state form the primitives of a graphical calculus. This calculus is expressive enough to generate and reason about arbitrary multipartite states, which are obtained by “composing” the GHZ- and W-states, giving rise to a rich graphical paradigm for general multipartite entanglement.
  5. Interacting Frobenius Algebras and the Structure of Multipartite Entanglement. Bob Coecke, Aleks Kissinger. Research report PRG-RR-09-12. pdf | abstract »
    Providing a generic description of entanglement in n-qubit systems is a long-standing open problem in quantum information science. A structural scheme for representing arbitrary multipartite entangled states will yield a deeper understanding of how they behave and interact as computational components within more general computational schemes and protocols. Here we provide such a description…
  6. Exploring a Quantum Theory with Graph Rewriting and Computer Algebra. Aleks Kissinger. In proceedings of Calculemus 2009. Spinger, 2009. pdf | springerlink | abstract »
    Graphical languages provide a powerful tool for describing the behaviour of quantum systems. While the use of graphs vastly reduces the complexity of many calculations, manual graphical manipulation quickly becomes untenable for large graphs or large numbers of graphs. To combat this issue, we are developing a tool called Quantomatic, which allows automated and semi-automated explorations of graph rewrite systems and their underlying semantics. We emphasise in this paper the features of Quantomatic that interact with a computer algebra system to discover graphical relationships via the unification of matrix equations. Since these equations can grow exponentially with the size of the graph, we use this method to discover small identities and use those identities as graph rewrites to expand the theory.
  7. Graph Rewrite Systems for Classical Structures in †-Symmetric Monoidal Categories. Masters thesis, 2008. pdf | abstract »
    This paper introduces several related graph rewrite systems derived from known identities on classical structures within a †-symmetric monoidal category. First, we develop a rewrite system based on a single classical structure, and use it to develop a proof of the so-called “spider-theorem,” where a connected graph containing a single classical structure can be uniquely determined by the number of inputs and outputs (i.e. it can be rewritten as a graph resembling an n-legged spider). These spiders are shown to be the normal forms of graphs containing a single classical structure. Next, complementary classical structures are introduced, as well as a new rewrite system on graphs of red and green spiders. A proof of convergence is given for a limited two-colour rewrite system, as well as insights into ways to approach normalisation in a more powerful rewrite system.
  8. Graph Rewriting for Classical Structures. Ross Duncan, Lucas Dixon, Aleks Kissinger. Poster presented at QICS 2008. pdf | abstract »
    Complementary classical structures correspond concretely to copy and delete operations over a pair of mutually unbiased bases. When acting as the generators of a †-symmetric monoidal category, they provide a powerful computational primitive, with a simple graphical representation. We have shown that the induced graph rewrite system is well-behaved and lends itself to automation.
  9. Lopol: A Deductive Database Approach to Policy Analysis and Rewriting. Aleks Kissinger, John C. Hale. In proceedings of the Second Annual SELinux Symposium, 2006. pdf | slides | abstract »
    This paper presents a method for deductive database-driven analysis of Security-Enhanced Linux policies. First, it discusses how directives in an SELinux policy can be normalized and encoded as logical relations. Next, the paper describes how to use these relations in conjunction with inference rules to perform a number of simple analyses. The techniques used to detect security characteristics within a policy can then be applied to automated policy rewriting, where those characteristics (i.e. security goals) are actually projected onto the policy to generate a new one. The paper closes by discussing the use of a logical ruleset as a high-level language, allowing a policy writer to quickly tailor a large default policy (such as strict, targeted, or refpolicy) to the specific needs of a system or a class of systems.

Links