The ZX-calculus is a powerful framework for reasoning in quantum computing. It provides in particular a compact representation of matrices of interests. A peculiar property of the ZX-calculus is the absence of a formal sum allowing the linear combinations of arbitrary ZX-diagrams. The universality of the formalism guarantees however that for any two ZX-diagrams, the sum of their interpretations can be represented by a ZX-diagram. We introduce a general, inductive definition of the addition of ZX-diagrams, relying on the construction of controlled diagrams. Based on this addition technique, we provide an inductive differentiation of ZX-diagrams. Indeed, given a ZX-diagram with variables in the description of its angles, one can differentiate the diagram according to one of these variables. Differentiation is ubiquitous in quantum mechanics and quantum computing (e.g. for solving optimization problems). Technically, differentiation of ZX-diagrams is strongly related to summation as witnessed by the product rules. We also introduce an alternative, non inductive, differentiation technique rather based on the isolation of the variables. Finally, we apply our results to deduce a diagram for an Ising Hamiltonian.

Abstract Variational Quantum Algorithms are hybrid classical-quantum algorithms where classical and quantum computation work in tandem to solve computational problems. These algorithms create interesting challenges for the design of suitable programming languages. In this paper we introduce Qimaera, which is a set of libraries for the Idris 2 programming language that enable the programmer to implement hybrid classical-quantum algorithms where the full power of the elegant Idris language works in synchrony with quantum programming primitives. The two key ingredients of Idris that make this possible are (1) dependent types which allow us to implement unitary quantum operations; and (2) linearity which allows us to enforce fine-grained control over the execution of quantum operations so that we may detect and reject many physically inadmissible programs. We also show that Qimaera is suitable for variational quantum programming by providing implementations of two prominent variational quantum algorithms – QAOA and VQE.

The ZX-calculus is a powerful framework for reasoning in quantum computing. It provides in particular a compact representation of matrices of interests. A peculiar property of the ZX-calculus is the absence of a formal sum allowing the linear combinations of arbitrary ZX-diagrams. The universality of the formalism guarantees however that for any two ZX-diagrams, the sum of their interpretations can be represented by a ZX-diagram. We introduce a general, inductive definition of the addition of ZX-diagrams, relying on the construction of controlled diagrams. Based on this addition technique, we provide an inductive differentiation of ZX-diagrams. Indeed, given a ZX-diagram with variables in the description of its angles, one can differentiate the diagram according to one of these variables. Differentiation is ubiquitous in quantum mechanics and quantum computing (e.g. for solving optimization problems). Technically, differentiation of ZX-diagrams is strongly related to summation as witnessed by the product rules. We also introduce an alternative, non inductive, differentiation technique rather based on the isolation of the variables. Finally, we apply our results to deduce a diagram for an Ising Hamiltonian.

There exist several graphical languages for quantum information processing, like quantum circuits, ZX-calculus, ZW-calculus, and so on. Each of these languages forms a †-symmetric monoidal category (†-SMC) and comes with an interpretation functor to the †-SMC of finite-dimensional Hilbert spaces. In recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of how to extend these languages beyond pure quantum mechanics to reason about mixed states and general quantum operations, i.e., completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map that allows one to get rid of a quantum system, an operation that is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction , which transforms any †-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction, we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However, this construction fails for some fringe cases like Clifford+T quantum mechanics, as the category does not have enough isometries.

Different graphical calculi have been proposed to represent quantum computation. First the ZX-calculus [Coecke and Duncan, 2011], followed by the ZW-calculus [Hadzihasanovic, 2015] and then the ZH-calculus [Backens and Kissinger, 2018]. We can wonder if new ZX-like calculi will continue to be proposed forever. This article answers negatively. All those language share a common core structure we call Z^*-algebras. We classify Z^*-algebras up to isomorphism in two dimensional Hilbert spaces and show that they are all variations of the aforementioned calculi. We do the same for linear relations and show that the calculus of [Bonchi et al., 2017] is essentially the unique one.

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.

There exist several graphical languages for quantum information processing, like quantum circuits, ZX-Calculus, ZW-Calculus, etc. Each of these languages forms a dagger-symmetric monoidal category (dagger-SMC) and comes with an interpretation functor to the dagger-SMC of (finite dimension) Hilbert spaces. In the recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of the extension of these languages beyond pure quantum mechanics, in order to reason on mixed states and general quantum operations, i.e. completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map which allows one to get rid of a quantum system, operation which is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction, which transforms any dagger-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However this construction fails for some fringe cases like the Clifford+T quantum mechanics, as the category does not have enough isometries.

Recent completeness results on the ZX-calculus used a third-party language, namely the ZW-Calculus. As a consequence, these proofs are elegant, but sadly non-constructive. We address this issue in the following. To do so, we first describe a generic normal form for ZX-diagrams in any fragment that contains Clifford+T quantum mechanics. We give sufficient conditions for an axiomatisation to be complete, and an algorithm to reach the normal form. Finally, we apply these results to the Clifford+T fragment and the general ZX-calculus - for which we already know the completeness-, but also for any fragment of rational angles: we show that the axiomatisation for Clifford+T is also complete for any fragment of dyadic angles, and that a simple new rule (called cancellation) is necessary and sufficient otherwise.

Subshifts are sets of colorings of Z^d by a finite alphabet that avoid some family of forbidden patterns. We investigate here some analogies with group theory that were first noticed by the first author. In particular we prove several theorems on subshifts inspired by Higman’s embedding theorems of group theory, among which, the fact that subshifts with a computable language can be obtained as restrictions of minimal subshifts of finite type.

We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics -- also called the π/4-fragment of the ZX-Calculus -- was one of the main open questions in categorical quantum mechanics. We prove the completeness of this fragment using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the π/4-fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-called Clifford+T fragment. We focus here on the expressive power of this axiomatisation beyond Clifford+T Quantum mechanics. We consider the full pure qubit quantum mechanics, and mainly prove two results: (i) First, the axiomatisation for Clifford+T quantum mechanics is also complete for all equations involving some kind of linear diagrams. The linearity of the diagrams reflects the phase group structure, an essential feature of the ZX-calculus. In particular all the axioms of the ZX-calculus are involving linear diagrams. (ii) We also show that the axiomatisation for Clifford+T is not complete in general but can be completed by adding a single (non linear) axiom, providing a simpler axiomatisation of the ZX-calculus for pure quantum mechanics than the one recently introduced by Ng&Wang.

In many instances in first order logic or computable algebra, classical theorems show that many problems are undecidable for general structures, but become decidable if some rigidity is imposed on the structure. For example, the set of theorems in many finitely axiomatisable theories is nonrecursive, but the set of theorems for any finitely axiomatisable complete theory is recursive. Finitely presented groups might have an nonrecursive word problem, but finitely presented simple groups have a recursive word problem.

The ZX-Calculus is a powerful graphical language for quantum mechanics and quantum information processing. The completeness of the language -- i.e. the ability to derive any true equation -- is a crucial question. In the quest of a complete ZX-calculus, supplementarity has been recently proved to be necessary for quantum diagram reasoning (MFCS 2016). Roughly speaking, supplementarity consists in merging two subdiagrams when they are parameterized by antipodal angles. We introduce a generalised supplementarity -- called cyclotomic supplementarity -- which consists in merging n subdiagrams at once, when the n angles divide the circle into equal parts. We show that when n is an odd prime number, the cyclotomic supplementarity cannot be derived, leading to a countable family of new axioms for diagrammatic quantum reasoning.We exhibit another new simple axiom that cannot be derived from the existing rules of the ZX-Calculus, implying in particular the incompleteness of the language for the so-called Clifford+T quantum mechanics. We end up with a new axiomatisation of an extended ZX-Calculus, including an axiom schema for the cyclotomic supplementarity.

We prove that the maximum speed and the entropy of a one-tape Turing machine are computable, in the sense that we can approximate them to any given precision . This is counterintuitive, as all dynamical properties are usually undecidable for Turing machines. The result is quite specific to one-tape Turing machines, as it is not true anymore for two-tape Turing machines by the results of Blondel et al., and uses the approach of crossing sequences introduced by Hennie.

Subshifts of finite type are sets of colorings of the plane defined by local constraints. They can be seen as a discretization of continuous dynamical systems. We investigate here the hardness of deciding factorization, conjugacy and embedding of subshifts of finite type (SFTs) in dimension d > 1. In particular, we prove that the factorization problem is Sigma^0_3-complete and that the conjugacy and embedding problems are Sigma^0_1-complete in the arithmetical hierarchy.

In this paper, we study the structure of the set of tilings produced by any given tile-set. For better understanding this structure, we address the set of finite patterns that each tiling contains. This set of patterns can be analyzed in two different contexts: the first one is combinatorial and the other topological. These two approaches have independent merits and, once combined, provide somehow surprising results. The particular case where the set of produced tilings is countable is deeply investigated while we prove that the uncountable case may have a completely different structure. We introduce a pattern preorder and also make use of Cantor-Bendixson rank. Our first main result is that a tile-set that produces only periodic tilings produces only a finite number of them. Our second main result exhibits a tiling with exactly one vector of periodicity in the countable case.

We study the following decision problem: is the language recognized by a quantum finite automaton empty or nonempty? We prove that this problem is decidable or undecidable depending on whether recognition is defined by strict or nonstrict thresholds. This result is in contrast with the corresponding situation for probabilistic finite automata, for which it is known that strict andnonstrict thresholds both lead to undecidable problems.