QPL 2018 Program

We first summarize recently found nonlocal games (with finite number of classical questions and answers) whose optimal winning probability can only be attained as a limit of strategies using arbitrarily high dimensional entangled states.

Then, we focus on one such game, an explicit three-player game with very few classical questions and answers. This game is based on the coherent state exchange game introduced in arXiv:0804.4118, which in turns is based on embezzlement of entanglement due to van Dam and Hayden. We discuss the main ideas behind each of these ingredients, and how they can be put together to obtain a quantitative tradeoff in the winning probability vs the dimension of the entangled state shared by the players.

Joint work with Zhengfeng Ji and Thomas Vidick, arXiv:1802.04926.

The advent of quantum computing has challenged classical conceptions of which problems are efficiently solvable in our physical world. This raises the general question of what broad relationships exist between physical principles and computation. This tutorial will explore this question in the the operationally-defined framework of generalised probabilistic theories. To begin, the limits on computational power imposed by simple physical principles will be explored. After this, we shall investigate whether post-quantum interference is a resource for post-quantum computation. The tutorial will end with a conjecture asking whether quantum theory is optimal for computation in the landscape of generalised probabilistic theories satisfying a single physical principle.

In this talk I will give a gentle introduction to quantum surface codes, and to how the ZX calculus may be used as a high-level design and compilation language for them. I will show how using the ZX calculus simplifies an understanding of how the codes work, and in particular gives immediate access to the connection between 2D and 3D codes. Looking particularly at the operations of lattice surgery, I show how they form a direct model for the generators of the calculus in terms of 'splitting' and 'merging' operations. Interpreting the calculus in this operational way means coming to grips with probabilistic procedures, and I look at ways we can deal with this within ZX. Finally I show how having the calculus as a graphial language for error correction pays off in the compilation problem for quantum processes, and show how we get new operational procedures for protocols, including magic state distillation, from equational rewriting of the ZX diagrams.

Quipper is a functional programming language for quantum computation which has been used to implement various elaborate quantum algorithms. At the moment, Quipper is implemented as an embedded language, whose host language is Haskell. One of the disadvantages to Quipper being an embedded language is that the Haskell type system, while providing many type-safety properties, is not in general strong enough to ensure the full type-safety of quantum programs.

The Proto-Quipper language provides a foundation for the development of a stand-alone (i.e., non-embedded) version of Quipper. Like Quipper, Proto-Quipper acts as a circuit description language and provides the ability to treat circuits as data in order to manipulate them as a whole. However, Proto-Quipper is also designed to “enforce the physics”, in the sense that its type system would detect, at compile-time, programming errors that could lead to ill-formed or undefined circuits.

I will start my talk with a brief introduction to quantum computing and a discussion of the design principles behind Quipper. I will then present Proto-Quipper and discuss open problems.

One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however still unclear. In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loops and recursion is possible. To this aim, we first propose a classical, typed, reversible language with lists and fixpoints. We then extend this language to the closed quantum domain (without measurements) by allowing linear combinations of terms and restricting fixpoints to structurally recursive fixpoints whose termination proofs match the proofs of convergence of sequences in infinite-dimensional Hilbert spaces. We additionally give an operational semantics for the quantum language in the spirit of algebraic lambda-calculi.

The talk will be based on arXiv:1804.00952.

Embedded quantum circuit languages like Quipper, LiQUi|⟩, and ProjectQ let programmers express high-level algorithms using host language libraries and features like recursion and data structures. But how can we verify the correctness of embedded quantum circuits without reasoning about the semantics of the entire host language? QWIRE (pronounced “choir”) is a quantum circuit language embedded in Coq, a dependently-typed programming language and interactive theorem prover. QWIRE both has the benefits of an embedded language and can be formally verified inside Coq itself. In this talk I will present the theory and semantics of QWIRE and show how to formally verify the correctness of quantum programs using QWIRE’s denotational semantics.

We will discuss the requirements for programming languages for quantum computers and highlight the differences with programming languages for classical computers. Then we will see how these new requirements are addressed in Q#. This talk will also serve as an introduction to Q#.

Although quantum computing is now a decades-old field, there are still many low-hanging opportunities for improving the projected costs of quantum algorithms by orders of magnitude. For example, when designing an efficient quantum algorithm one can often identify nearly-classical subproblems. Efficient classical circuits for these subproblems translate into efficient quantum circuits for the original algorithm.

This talk will discuss a concrete example of the quantum-to-classical-and-back approach bearing fruit. I will show that preparing a particular type of superposition is equivalent to fitness proportionate selection (a classical task where one has a population of items with associated fitnesses and wishes to sample items with twice as much fitness twice as often). I will then explain an efficient classical algorithm for fitness proportionate selection, and translate it back into the quantum domain to produce the 'subprepare' oracle from arXiv:1805.03662, which prepares (and unprepares) superpositions with hardcoded coefficients 100x more efficiently than previous work.

Many experiments in the field of quantum foundations seek to adjudicate between quantum theory and speculative alternatives to it. This requires one to analyze the experimental data in a manner that does not presume the correctness of the quantum formalism. The mathematical framework of generalized probabilistic theories (GPTs) provides a means of doing so. We present a scheme for determining what GPTs are consistent with a given set of experimental data. It proceeds by performing tomography on the preparations and measurements in a self-consistent manner, i.e., without presuming a prior characterization of either. We illustrate the scheme by analyzing experimental data for a large set of preparations and measurements on the polarization degree of freedom of a single photon. We find that the smallest and largest GPT state spaces consistent with our data are a pair of polytopes, each approximating the shape of the Bloch Sphere and having a volume ratio of 0.977 ± 0.001, which provides a quantitative bound on the scope for deviations from quantum theory. We also demonstrate how our scheme can be used to bound the extent to which nature might be more nonlocal than quantum theory predicts, as well as the extent to which it might be more or less contextual. Specifically, we find that the maximal violation of the CHSH inequality can be at most 1.3% ± 0.1 greater than the quantum prediction, and the maximal violation of a particular noncontextuality inequality cannot differ from the quantum prediction by more than this factor on either side.