When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.
When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.
In the last years, quantum computational logics have been developed in order to describe the logical setting of quantum computation [1]. An important challenge is the development of proof theoretical tools for quantum computation, so that the physical process of computation can correspond to a logical process of computation. In particular, the challenge is that quantum computational speed up, due to superposition and entanglement, can find an explanation in terms of logical proofs. The object of our research is a sequent calculus developed in the framework of basic logic, that is a logical platform to study extensional logics, including quantum logics [2, 3]. In basic logic, logical connectives and their rules are the result of importing suitable links at the metalevel into the object level. We suppose that a particular kind of dynamics between the object level and the metalevel is created when considering a quantum system rather than a classical one. This is due to a specific treatment of variables, that, in our view, can create the logical setting for a holistic, rather than compositional, treatment of information, proper of entangled states [4]. Then we develop a predicative sequent calculus. In it, superposition is built by quantifying a propo-sition, associated with a quantum system, on a first order domain determined by the experiments on such system. Then a convenient treatment of variables can create dynamically entangled states in logical
This thesis is a study of the construction and representation of typed models of quantum mechanics for use in quantum computation. We introduce logical and graphical syntax for quantum mechanical processes and prove that these formal systems provide sound and complete representations of abstract quantum mechanics. In addition, we demonstrate how these representations may be used to reason about the behaviour of quantum computational processes. Quantum computation is presently mired in low-level formalisms, mostly derived directly from matrices over Hilbert spaces. These formalisms are an obstacle to the full understanding and exploitation of quantum effects in informatics since they obscure the essential structure of quantum states and processes. The aim of this work is to introduce higher level tools for quantum mechanics which will be better suited to computation than those presently employed in the field. Inessential details of Hilbert space representations are removed and the informatic structures are presented directly. Entangled states are particularly important in this treatment, as is appropriate, since entanglement is a fundamental driver of quantum computation. The benefits two-fold: as well as producing foundational tools for the study of quantum computation this work also connects quantum mechanics to mainstream areas of computer science such as categorical logic, type theory, program language semantics, and rewriting. We describe, following Abramsky and Coecke, how quantum mechanics may be carried out without reference to Hilbert space, in a strongly compact closed category. In particular we show how to freely construct a categorical model of abstract quantum mechanics from an arbitrary category. We introduceMultiplicative Categorical Quantum Logic (mCQL), a sequent calculus whose proof rules capture the structure of compact closed categories. This sequent calculus is interpreted in a freely generated compact closed category, and its semantics is sound with respect to cut elimination. We define an equivalent graphical syntax, similar to linear logic’s proof-nets, and prove that these proof-nets provide a full and faithful representation of any freely generated compact closed category. Further analysis of the structure of quantum states which correspond to mCQL proofs using multiplicative linear logic shows that the linear type system describes the quantum entanglement found in such states. We show that the entanglement present in these states is always of a particularly simple form: collections of entangled pairs. In order to tackle arbitrary entanglement, we generalise the work of Kelly and Laplaza to give a representation theorem for the free compact closed category by a polycategory. Such categories are shown to be equivalent to a generalised system of proof-nets whose axioms may have more than one premise
We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various linear operators. As an example we sketch an analysis of the teleportation protocol.
Recently we proved that there are two non-isomorphic models of the calculus of quantum logic corresponding to an infinite-dimensional Hilbert space representation: an orthomodular lattice and a weakly orthomodular lattice. We also discovered that there are two non-isomorphic models of the calculus of classical logic: a distributive lattice (Boolean algebra) and a weakly distributive lattice. In this work we consider implications of these results to a quantum simulator which should mimic quantum systems by giving precise instructions on how to produce input state, how to evolve them, and how to read off the final states. We analyze which conditions quantum states of a quantum computer currently obey and which they should obey in order to enable full quantum computing, i.e., proper quantum mathematics. In particular we find several new conditions which lattices of Hilbert space subspaces must satisfy.
In the study of quantum computation, data is represented in terms of linear operators which form a generalized model of probability, and computations are most commonly described as products of unitary transformations, which are the transformations which preserve the quality of the data in a precise sense. This naturally leads to "unitary circuit models", which are models of computation in which unitary operators are expressed as a product of "elementary" unitary transformations. However, unitary transformations can also be effected as a composition of operations which are not all unitary themselves: the "one-way measurement model" is one such model of quantum computation. In this thesis, we examine the relationship between representations of unitary operators and decompositions of those operators in the one-way measurement model. In particular, we consider different circumstances under which a procedure in the one-way measurement model can be described as simulating a unitary circuit, by considering the combinatorial structures which are common to unitary circuits and two simple constructions of one-way based procedures. These structures lead to a characterization of the one-way measurement patterns which arise from these constructions, which can then be related to efficiently testable properties of graphs. We also consider how these characterizations provide automatic techniques for obtaining complete measurement-based decompositions, from unitary transformations which are specified by operator expressions bearing a formal resemblance to path integrals. These techniques are presented as a possible means to devise new algorithms in the one-way measurement model, independently of algorithms in the unitary circuit model.
This thesis considers various paradigms of quantum computation in an attempt to understand the nature of the underlying physics. A standard approach is to consider unitary computation on pure input states, such that the outcome of the computation is determined by single computational basis measurement on the output state. It has been shown that there exists equivalent models of computation, such as measurement based quantum computing (MBQC), which provide insight into the role of entanglement and measurement. Furthermore, constraining or relaxing available resources can directly impacts the power of the computation, allowing one to gauge their role in the process. Here, we first extend known constructions such as Matrix Product States, MBQC and the oneclean qubit model to a mixed state formalism, in an attempt to develop computational models where noise acting on the physical resources, as might be experienced in laboratory settings, may be mapped to logical noise on the computation. Next, we introduce Measurement-Based Classical Computing, an essentially classical model of computation, wherein the complexity hard wired into probability distributions generated via quantum means yields surprising non classical results. Finally, we consider postselection the ability to discard displeasing measurement outcomes and argue that it may be used in a tame way, which does not provide a dramatic increase in computational power. From here, we develop a new Hamiltonian, based on a circuit to Hamiltonian construction, presenting evidence of QMA-hardness.