We argue that a realistic model for quantum computations should be general with respect to measurements, and complete with respect to the information flow between the quantum and classical worlds. We discuss two alternative models for general and complete quantum computations based on probability distributions of quantum state vectors and on density matrices with classical outputs. We show that both models can be structured using a generalization of monads called arrows.
We argue that a realistic model for quantum computations should be general with respect to measurements, and complete with respect to the information flow between the quantum and classical worlds. We discuss two alternative models for general and complete quantum computations based on probability distributions of quantum state vectors and on density matrices with classical outputs. We show that both models can be structured using a generalization of monads called arrows.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and measurement. The effectful part can be modelled using a generalisation of monads called arrows. We express the resulting executable model of quantum computing in the Haskell programming language using its special syntax for arrow computations. However, the embedding in Haskell is not perfect: a faithful model of quantum computing requires type capabilities that are not directly expressible in Haskell.
Quantum computing is an emerging technology that, currently, has the challenge of developing programming languages, according to the rules of quantum mechanics, to support the creation, analysis, modeling and simulation of high-level quantum algorithms. Particularly, the focus is on the investigation of new semantic models to develop programming languages for quantum computing. In this context, one alternative is to use the semantic model of monads and arrows that abstracts both pure and mixed quantum states and also can express measures. This model however, was originally implemented as a library for the functional language Haskell, which not every programmer is family. This way, this study aims to provide a universal tool for high-level quantum programming, providing a library for Java. This library was implemented using the new features of closures present in the version 8 of the JDK (Java Development Kit), already available in developers preview. In addition, we present a specific syntax for the library to facilitate the development of quantum algorithms with a clearly structured notation. This syntax is described in a notation similar to the do-notation of Haskell and operates in conjunction with a parser implemented by ANTLR tool.
This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally\nverified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the “Quantum IO Monad”, this framework is designed following a structural approach as given by a categorical model of quantum computation.
We present a framework for representing quantum entities in Haskell. States and operators are functional objects, and their semantics is defined --- as far as possible --- independently of the base in the Hilbert space. We construct effectively the tensor states for composed systems, and we present a toy model of quantum circuit toolbox. We conclude that functional languages are right tools for formal computations in quantum physics. The paper focuses mainly on the representation, not on computational problems.
The quantum IO monad is a purely functional interface to quantum programming implemented as a Haskell library. At the same time it provides a constructive semantics of quantum programming. The QIO monad separates reversible ( i.e ., unitary) and irreversible ( i.e ., probabilistic) computations and provides a reversible let operation ( ulet ), allowing us to use ancillas (auxiliary qubits) in a modular fashion. QIO programs can be simulated either by calculating a probability distribution or by embedding it into the IO monad using the random number generator. As an example we present a complete implementation of Shor's algorithm. 5.1 Introduction We present an interface from a pure functional programming language, Haskell, to quantum programming: the quantum IO monad, and use it to implement Shor's factorization algorithm. The implementation of the QIO monad provides a constructive semantics for quantum programming, i.e ., a functional program that can also be understood as a mathematical model of quantum computing. Actually, the Haskell QIO library is only a first approximation of such a semantics; we would like to move to a more expressive language that is also logically sound. Here we are thinking of a language such as Agda (Norell 2007), which is based on Martin Löf's type theory. We have already investigated this approach of functional specifications of effects in a classical context (Swierstra and Altenkirch 2007, 2008; Swierstra 2008). At the same time the QIO monad provides a high-level interface to a hypothetical quantum computer.
The aim of this paper is to introduce a general model of quantum computation, the quantum calculus: both unitary transformations and projective measurements are allowed; furthermore a complete classical control, including conditional structures and loops, is available. Complementary to its operational semantics, we introduce a pure denotational semantics for the quantum calculus. Based on probabilistic power domains [Jones, C. and G. D. Plotkin, A probabilistic powerdomain of evaluations, in: LICS, 1989, pp. 186–195. URL http://homepages.inf.ed.ac.uk/gdp/publications/Prob_Powerdomain.pdf], this pure denotational semantics associates with any description of a computation in the quantum calculus its action in a mathematical setting. Adequacy between operational and pure denotational semantics is established. Additionally to this pure denotational semantics, an observable denotational semantics is introduced. Following the work by Selinger, this observable denotational semantics is based on density matrices and super-operators. Finally, we establish an exact abstraction connection between these two semantics.