This paper describes the semantics of Quantum, a language that was specifically designed to control resource consumption of distributed computations, such as mobile agent style applications. In Quantum, computations can be driven by mastering their resource consumption. Resources can be understood as processors cycles, geographical expansion, bandwidth or duration of communications, etc. We adopt a generic view by saying that computations need energy to be performed. Quantum relies on three new primitives that deal with energy. The first primitive creates a tank of energy associated with a computation. Asynchronous notifications inform the user of energy exhaustion and computation termination. The other two primitives allow us to implement suspension and resumption of computations by emptying a tank and by supplying more energy to a tank. The semantics takes the form of an abstract machine with explicit parallelism and energy-related primitives. 1 Introduction Millions of computers ...
This paper describes the semantics of Quantum, a language that was specifically designed to control resource consumption of distributed computations, such as mobile agent style applications. In Quantum, computations can be driven by mastering their resource consumption. Resources can be understood as processors cycles, geographical expansion, bandwidth or duration of communications, etc. We adopt a generic view by saying that computations need energy to be performed. Quantum relies on three new primitives that deal with energy. The first primitive creates a tank of energy associated with a computation. Asynchronous notifications inform the user of energy exhaustion and computation termination. The other two primitives allow us to implement suspension and resumption of computations by emptying a tank and by supplying more energy to a tank. The semantics takes the form of an abstract machine with explicit parallelism and energy-related primitives. 1 Introduction Millions of computers ...
With the approaching end of Moore’s Law, where will not be possible to improve the capacity of silicon based processors, the quantum computing appear to be a good choice to provide a new era of computation. Quantum computing can be understood as the art of transform information encoded in the state of a quantum physical system. This encoding is through the quantum bits (qubits), which can be on superposition or entangled states, enabling to explore the property called quantum parallelism. In this work is discussed the creation of a quantum programming language implementing the object-oriented paradigm (OO), allowing manipulation of classes and objects, where the quantum effects are handled through a monadic approach, extending the Featherweight Java (FJ) proposal. This language is formally defined through the operational semantics, which allow the implementation in any language that provides closures. That language formalization enables us to create an interpreter, implementing the steps of lexical, syntactic and semantic analysis, focusing in the type system to embedded quantum computing concepts in a classical language. Several examples are provided in the text, showing ways to handle the monadic layer in order to perform transformations in quantum information.
Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.
The study of computational processes based on the laws of quantum mechanics has led to the discovery of new algorithms, cryptographic techniques, and communication primitives. This book explores quantum computation from the perspective of the branch of theoretical computer science known as semantics, as an alternative to the more well-known studies of algorithmics, complexity theory, and information theory. It collects chapters from leading researchers in the field, discussing the theory of quantum programming languages, logics and tools for reasoning about quantum systems, and novel approaches to the foundations of quantum mechanics. This book is suitable for graduate students and researchers in quantum information and computation, as well as those in semantics, who want to learn about a new field arising from the application of semantic techniques to quantum information and computation.
Quantum programming languages permit a hardware independent, high-level description of quantum algo rithms. In particular, the quantum lambda-calculus is a higher-order programming language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum lambda-calculus is a challenging problem that has attracted significant interest in the past few years. Several models have been proposed but for those that address the whole quantum λ-calculus, they either do not represent the dynamics of computation, or they lack the compositionality one often expects from denotational models. In this paper, we give the first compositional and interactive model of the full quantum lambda-calculus, based on game semantics. To achieve this we introduce a model of quantum games and strategies, combining quantum data with a representation of the dynamics of computation inspired from causal models of concurrent systems. In this model we first give a computationally adequate interpretation of the affine fragment. Then, we extend the model with a notion of symmetry, allowing us to deal with replication. In this refined setting, we interpret and prove adequacy for the full quantum lambda-calculus. We do this both from a sequential and a parallel interpretation, the latter representing faithfully the causal independence between sub-computations.
The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.