In this short paper we present the main features of a new quantum programming language proposed recently by Peter Selinger which gives a good idea about the difficulties of constructing a scalable quantum computer. We show how some of these difficulties are related to the contextuality of quantum observables and to the abstract and statistical character of quantun theory (QT). We discuss also, in some detail, the statistical interpretation (SI) of QT and the contextuality of observables indicating the importance of these concepts for the whole domain of quantum information.
In this short paper we present the main features of a new quantum programming language proposed recently by Peter Selinger which gives a good idea about the difficulties of constructing a scalable quantum computer. We show how some of these difficulties are related to the contextuality of quantum observables and to the abstract and statistical character of quantun theory (QT). We discuss also, in some detail, the statistical interpretation (SI) of QT and the contextuality of observables indicating the importance of these concepts for the whole domain of quantum information.
Several domains [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004; B. Coecke and K. Martin. A partial order on classical and quantum states. Technical report, PRG-RR-02-07, 2002; Ph. Jorrand and S. Perdrix. Towards a quantum calculus. In To appear in Proceedings of the 4th International Workshop on Quantum Programming Languages, ENTCS, 2006; P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] can be used to define the semantics of quantum programs. Among them Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004] has introduced a semantics based on probabilistic power domains, whereas the one by Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] associates with every program a completely positive map. In this paper, we mainly introduce a semantical domain based on admissible transformations, i.e. multisets of linear operators. In order to establish a comparison with existing domains, we introduce a simple quantum imperative language (QIL), equipped with three different denotational semantics, called pure, observable, and admissible respectively. The pure semantics is a natural extension of probabilistic (classical) semantics and is similar to the semantics proposed by Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004]. The observable semantics, à la Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004], associates with any program a superoperator over density matrices. Finally, we introduce an admissible semantics which associates with any program an admissible transformation. These semantics are not equivalent, but exact abstraction [P. Cousot. Types as abstract interpretations. In POPL, pages 316–331, 1997] or interpretation relations are established between them, leading to a hierarchy of quantum semantics.
. Quantum computers take advantage of interfering quantum alternatives in order to handle problems that might be too time consuming with algorithms based on classical logic. Developing quantum computers requires new ways of thinking beyond those in the familiar classical world. To help in this thinking, we give a description of the foundational ideas that hold in all of our successful physical models, including quantum theory. Our emphasis will be on the proper interpretation of our theories, and not just their statements. Our tact will be to build on the concept of information, which lies central to the operation of not just computers, but the Universe. For application to quantum computing, the essence of quantum theory is given, together with special precautions and limitations. Introduction. Having a grasp on the ideas behind a theory helps to apply it correctly, to understand its limitations, and to generate new ideas. Getting a firm hold on quantum theory is not an easy task, because our experiences and even our genetic predispositions have been developed in a world in which quantum effects are largely washed out. Remarkably, our predilection for finding logic behind the behavior of what we observe, including that of electrons and atoms, has led us to quantum theory, a description of nature that is hard for us to conceptualize, but is logical, accurate, and explains a wide variety of phenomena with only a few statements and input. As background to quantum theory and quantum computing, an attempt is made here to give the primitive notions and essential observations that underlie current physical theories, so that foundational ideas are explicit, and a common language is established. In our description, information storage and transfer is made central. A short description of quantum theory follows, and then applied to quantum computing, focusing on what the theory says, and particularly does not say, in areas where conceptual difficulties have arisen. Physical theory and reality. A physical theory is a logical model capable of making predictions of what we observe. It is judged by its accuracy in matching measurements, and by its economy, i.e. whether the proposed theory has only a few relationships and input data needed for its ability to explain observations over a wide realm.
In this talk, I will give an overview of some recent progress and current challenges in the design of quantum programming languages. Unlike classical programs, which can in principle be debugged by stopping the program at critical moments and examining the contents of variables, quantum programs are not amenable to traditional debugging because the state of a quantum system cannot usually be examined in a meaningful way. Therefore, we need other methods for ensuring the correctness of quantum programs, such as formal verification. For this reason, I advocate the use of strongly typed, functional programming languages for quantum computing. As far as functional quantum programming languages are concerned, there is currently a relatively wide gap between theory and practice. On the one hand, we have languages with strong theoretical foundations, such as the quantum lambda calculus, which operate at a relatively low level of abstraction and lack many features that would be useful to practical quantum programmers. On the other hand, we have practical functional quantum programming languages such as Quipper, which is implemented as an embedded language in Haskell, has many high-level features, and has been used in large-scale projects, but lacks a theoretical basis and a strong type system [Green et al., 2013; Green et al., 2013; Green et al., 2013; Smith et al., 2014]. We have recently attempted to narrow this gap through a family of languages called Proto-Quipper, which are designed to offer Quipper-like features while having sound theoretical foundations [Ross, 2015; Rios and Selinger, 2018]. I will give an overview of Quipper and its most useful features, report on the progress we made with formalizing fragments of Quipper, and outline several of the still remaining challenges.
Recent developments in the mathematical foundations of quantum mechanics have brought the theory closer to that of classical probability and statistics. On the other hand, the unique character of quantum physics sets many of the questions addressed apart from those met classically in stochastics. Furthermore, concurrent advances in experimental techniques and in the theory of quantum computation have led to a strong interest in questions of quantum information, in particular in the sense of the amount of information about unknown parameters in given observational data or accessible through various possible types of measurements. This scenery is outlined (with an audience of statisticians and probabilists in mind).
Contextuality is a key distinguishing feature between classical and quantum physics. It expresses a fundamental obstruction to describing quantum theory using classical concepts. In turn, understood as a resource for quantum computation, it is expected to hold the key to quantum advantage. Yet, despite its long recognised importance in quantum foundations and, more recently, in quantum computation, the structural essence of contextuality has remained somewhat elusive - different frameworks address different aspects of the phenomenon, yet their precise relationship often remains unclear. This issue already looms large at the level of the Bell-Kochen-Specker theorem: while traditional proofs proceed by showing the nonexistence of valuations, the notion of state-independent contextuality in the marginal approach allows to prove contextuality from seemingly weaker assumptions. In the light of this, and at the absence of a unified mathematical framework for Kochen-Specker contextuality, the original algebraic approach has been widely abandoned, in favour of the study of contextual correlations. Here, we reinstate the algebraic perspective on contextuality. Concretely, by building on the novel concept of context connections, we reformulate the algebraic relations between observables originally postulated by Kochen and Specker, and we explicitly demonstrate their consistency with the notion of state-independent contextuality. In the present paper, we focus on the new conceptual ideas and discuss them in the concrete setting of spin-1 observables, specifically those in the example of [S. Yu and C.H. Oh, Phys. Rev. Lett., 108, 030402 (2012)]; in a companion paper, we generalise these ideas, obtain a complete characterisation of Kochen-Specker contextuality and provide a detailed comparison with the related notions of contextuality in the marginal and graph-theoretic approach.