The Measurement Calculus

The Measurement Calculus

Abstract

Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion of measurement is the main driving force of computation. This is in contrast with the more traditional circuit model which is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer stands out as fundamental.

We develop a rigorous mathematical model underlying the one-way quantum computer and present a concrete syntax and operational semantics for programs, which we call patterns, and an algebra of these patterns derived from a denotational semantics. More importantly, we present a calculus for reasoning locally and compositionally about these patterns. We present a rewrite theory and prove a general standardization theorem which allows all patterns to be put in a semantically equivalent standard form. Standardization has far-reaching consequences: a new physical architecture based on performing all the entanglement in the beginning, parallelization by exposing the dependency structure of measurements and expressiveness theorems.

Furthermore we formalize several other measurement-based models e.g. Teleportation, Phase and Pauli models and present compositional embeddings of them into and from the one-way model. This allows us to transfer all the theory we develop for the one-way model to these models. This shows that the framework we have developed has a general impact on measurement-based computation and is not just particular to the one-way quantum computer.

One Introduction

The emergence of quantum computation has changed our perspective on many fundamental aspects of computing: the nature of information and how it flows, new algorithmic design strategies and complexity classes and the very structure of computational models. New challenges have been raised in the physical implementation of quantum computers. This paper is a contribution to a nascent discipline: quantum programming languages.

This is more than a search for convenient notation, it is an investigation into the structure, scope and limits of quantum computation. The main issues are questions about how quantum processes are defined, how quantum algorithms compose, how quantum resources are used and how classical and quantum information interact.

Quantum computation emerged in the early nineteen eighties with Feynman's observations about the difficulty of simulating quantum systems on a classical computer. This hinted at the possibility of turning around the issue and exploiting the power of quantum systems to perform computational tasks more efficiently than was classically possible. In the mid nineteen eighties Deutsch and later

Deutsch and Jozsa showed how to use superposition - the ability to produce linear combinations of quantum states - to obtain computational speedup. This led to interest in algorithm design and the complexity aspects of quantum computation by computer scientists. The most dramatic results were Shor's celebrated polytime factorization algorithm and Grover's sub-linear search algorithm. Remarkably one of the problematic aspects of quantum theory, the presence of non-local correlation - an example of which is called "entanglement" - turned out to be crucial for these algorithmic developments.

If efficient factorization is indeed possible in practice, then much of cryptography becomes insecure as it is based on the difficulty of factorization. However, entanglement makes it possible to design unconditionally secure key distribution. Furthermore, entanglement led to the remarkable - but simple - protocol for transferring quantum states using only classical communication; this is the famous so-called "teleportation" protocol. There continues to be tremendous activity in quantum cryptography, algorithmic design, complexity and information theory. Parallel to all this work there has been intense interest from the physics community to explore possible implementations.

On the other hand, only recently has there been significant interest in quantum programming languages; i.e. the development of formal syntax and semantics and the use of standard machinery for reasoning about quantum information processing. The first quantum programming languages were variations on imperative probabilistic languages and emphasized logic and program development based on weakest preconditions. The first definitive treatment of a quantum programming language was the flowchart language of Selinger. It was based on combining classical control, as traditionally seen in flowcharts, with quantum data. It also gave a denotational semantics based on completely positive linear maps. The notion of quantum weakest preconditions was developed later. Later people proposed languages based on quantum control. The search for a sensible notion of higher-type computation continues, but is problematic.

A related recent development is the work of Abramsky and Coecke where they develop a categorical axiomatization of quantum mechanics. This can be used to verify the correctness of quantum communication protocols. It is very interesting from a foundational point of view and allows one to explore exactly what mathematical ingredients are required to carry out certain quantum protocols. This has also led to work on a categorical quantum logic.

The study of quantum communication protocols has led to formalizations based on process algebras and to proposals to use model checking for verifying quantum protocols. A survey and a complete list of references on this subject up to two thousand five is available.

These ideas have proven to be of great utility in the world of classical computation. The use of logics, type systems, operational semantics, denotational semantics and semantic-based inference mechanisms have led to notable advances such as: the use of model checking for verification, reasoning compositionally about security protocols, refinement-based programming methodology and flow analysis.

The present paper applies this paradigm to a very recent development: measurement-based quantum computation. None of the cited research on quantum programming languages is aimed at measurement-based computation. On the other hand, the work in the physics literature does not clearly separate the conceptual layers of the subject from implementation issues. A formal treatment is necessary to analyze the foundations of measurement-based computation.

So far the main framework to explore quantum computation has been the circuit model, based on unitary evolution. This is very useful for algorithmic development and complexity analysis. There are other models such as quantum Turing machines and quantum cellular automata. Although they are all proved to be equivalent from the point of view of expressive power, there is no agreement on what is the canonical model for exposing the key aspects of quantum computation.

Recently physicists have introduced novel ideas based on the use of measurement and entanglement to perform computation. This is very different from the circuit model where measurement is done only at the end to extract classical output. In measurement-based computation the main operation to manipulate information and control computation is measurement. This is surprising because measurement creates indeterminacy, yet it is used to express deterministic computation defined by a unitary evolution.

The idea of computing based on measurements emerged from the teleportation protocol. The goal of this protocol is for an agent to transmit an unknown qubit to a remote agent without actually sending the qubit. This protocol works by having the two parties share a maximally entangled state called a Bell pair. The parties perform local operations - measurements and unitaries - and communicate only classical bits. Remarkably, from this classical information the second party can reconstruct the unknown quantum state. In fact one can actually use this to compute via teleportation by choosing an appropriate measurement. This is the key idea of measurement-based computation.

It turns out that the above method of computing is actually universal. This was first shown by Gottesman and Chuang who used two-qubit measurements and given Bell pairs. Later Nielsen showed that one could do this with only four-qubit measurements with no prior Bell pairs, however this works only probabilistically. Leung improved this to two qubits, but her method also works only probabilistically. Later Perdrix and Jorrand gave the minimal set measurements to perform universal quantum computing - but still in the probabilistic setting - and introduced the state-transfer and measurement-based quantum Turing machine. Finally the one-way computer was invented by Raussendorf and Briegel which used only single-qubit measurements with a particular multi-party entangled state, the cluster state.

More precisely, a computation consists of a phase in which a collection of qubits are set up in a standard entangled state. Then measurements are applied to individual qubits and the outcomes of the measurements may be used to determine further measurements. Finally - again depending on measurement outcomes - local unitary operators, called corrections, are applied to some qubits; this allows the elimination of the indeterminacy introduced by measurements. The phrase "one-way" is used to emphasize that the computation is driven by irreversible measurements.

There are at least two reasons to take measurement-based models seriously: one conceptual and one pragmatic. The main pragmatic reason is that the one-way model is believed by physicists to lend itself to easier implementations. Physicists have investigated various properties of the cluster state and have accrued evidence that the physical implementation is scalable and robust against decoherence. Conceptually the measurement-based model highlights the role of entanglement and separates the quantum and classical aspects of computation; thus it clarifies, in particular, the interplay between classical control and the quantum evolution process.

Our approach to understanding the structural features of measurement-based computation is to develop a formal calculus. One can think of this as an "assembly language" for measurement-based computation. Ours is the first programming framework specifically based on the one-way model. We first develop a notation for such classically correlated sequences of entanglements, measurements, and local corrections. Computations are organized in patterns, and we give a careful treatment of the composition and tensor product (parallel composition) of patterns. We show next that such pattern combinations reflect the corresponding combinations of unitary operators. An easy proof of universality follows.

So far, this is primarily a clarification of what was already known from the series of papers introducing and investigating the properties of the one-way model. However, we work here with an extended notion of pattern, where inputs and outputs may overlap in any way one wants them to, and this results in more efficient - in the sense of using fewer qubits - implementations of unitaries. Specifically, our universal set consists of patterns using only two qubits. From it we obtain a three-qubit realization of the Rz rotations and a fourteen-qubit realization for the controlled-U family: a significant reduction over the hitherto known implementations.

The main point of this paper is to introduce a calculus of local equations over patterns that exploits some special algebraic properties of the entanglement, measurement and correction operators. More precisely, we use the fact that that one-qubit XY measurements are closed under conjugation by Pauli operators and the entanglement command belongs to the normalizer of the Pauli group; these terms are explained in the appendix. We show that this calculus is sound in that it preserves the interpretation of patterns. Most importantly, we derive from it a simple algorithm by which any general pattern can be put into a standard form where entanglement is done first, then measurements, then corrections. We call this standardization.

The consequences of the existence of such a procedure are far-reaching. Since entangling comes first, one can prepare the entire entangled state needed during the computation right at the start: one never has to do "on the fly" entanglements. Furthermore, the rewriting of a pattern to standard form reveals parallelism in the pattern computation. In a general pattern, one is forced to compute sequentially and to strictly obey the command sequence, whereas, after standardization, the dependency structure is relaxed, resulting in lower computational depth complexity. Last, the existence of a standard form for any pattern also has interesting corollaries beyond implementation and complexity matters, as it follows from it that patterns using no dependencies, or using only the restricted class of Pauli measurements, can only realize a unitary belonging to the Clifford group, and hence can be efficiently simulated by a classical computer.

As we have noted before, there are other methods for measurement-based quantum computing: the teleportation technique based on two-qubit measurements and the state-transfer approach based on single qubit measurements and incomplete two-qubit measurements. We will analyze the teleportation model and its relation to the one-way model. We will show how our calculus can be smoothly extended to cover this case as well as new models that we introduce in this paper. We get several benefits from our treatment. We get a workable syntax for handling the dependencies of operators on previous measurement outcomes just by mimicking the one obtained in the one-way model. This has never been done before for the teleportation model. Furthermore, we can use this embedding to obtain a standardization procedure for the models. Finally these extended calculi can be compositionally embedded back in the original one-way model. This clarifies the relation between different measurement-based models and shows that the one-way model of Raussendorf and Briegel is the canonical one.

This paper develops the one-way model ab initio but certain concepts that the reader may be unfamiliar with: qubits, unitaries, measurements, Pauli operators and the Clifford group are in an appendix. These are also readily accessible through the very thorough book of Nielsen and Chuang.

In the next section we define the basic model, followed by its operational and denotational semantics, for completeness a simple proof of universality is given in section four, this has appeared earlier in the physics literature, in section five we develop the rewrite theory and prove the fundamental standardization theorem. In section six we develop several examples that illustrate the use of our calculus in designing efficient patterns. In section seven we prove some theorems about the expressive power of the calculus in the absence of adaptive measurements. In section eight we discuss other measurement-based models and their compositional embedding to and from the one-way model. In section nine we discuss further directions and some more related work. In the appendix we review basic notions of quantum mechanics and quantum computation.