The measurement calculus

TLDR

Measurement‑based quantum computation uses measurement as the primary computational resource, contrasting with the traditional circuit model, and the one‑way quantum computer introduced by Raussendorf and Briegel is a foundational example. The authors aim to construct a rigorous mathematical framework for the one‑way quantum computer, defining a concrete syntax and operational semantics for pattern programs. They develop an algebra of patterns derived from a denotational semantics, introduce a local, compositional calculus, prove a general standardization theorem via a rewrite theory, and embed other measurement‑based models such as teleportation, phase, and Pauli into this framework. Standardization enables a new architecture that performs all entanglement upfront, exposes measurement dependencies for parallelization, and yields expressiveness theorems, while the framework’s transferability to other models demonstrates its broad impact on measurement‑based computation.

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 that is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer [Raussendorf and Briegel 2001] 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, for example, 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.