# The Measurement Calculus

## TL;DR

This paper develops a rigorous mathematical framework for measurement-based quantum computation, especially the one-way quantum computer, enabling formal reasoning, standardization, and embedding of related models.

## Contribution

It introduces a formal calculus and semantics for measurement patterns, proving standardization and embedding results that unify various measurement-based quantum computation models.

## Key findings

- Established a rewrite theory and standardization theorem for measurement patterns.
- Demonstrated embeddings of teleportation, phase, and Pauli models into the one-way model.
- Enabled transfer of theoretical results across different measurement-based quantum computation models.

## 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: 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.