Algebraic and Logical Methods in Quantum Computation

TL;DR

This thesis advances quantum computation theory by introducing an efficient approximation method for special unitary operators and formalizing a typed lambda calculus for a fragment of the Quipper language, ensuring type safety.

Contribution

It presents a new optimal approximation technique for unitaries and formalizes Proto-Quipper, a type-safe quantum programming language fragment based on linear logic.

Findings

Efficient approximation sequences for special unitaries are asymptotically optimal.

Proto-Quipper formalizes a fragment of Quipper with proven type safety.

The approximation method is optimal for diagonal unitaries.

Abstract

This thesis contains contributions to the theory of quantum computation. We first define a new method to efficiently approximate special unitary operators. Specifically, given a special unitary U and a precision {\epsilon} > 0, we show how to efficiently find a sequence of Clifford+V or Clifford+T operators whose product approximates U up to {\epsilon} in the operator norm. In the general case, the length of the approximating sequence is asymptotically optimal. If the unitary to approximate is diagonal then our method is optimal: it yields the shortest sequence approximating U up to {\epsilon}. Next, we introduce a mathematical formalization of a fragment of the Quipper quantum programming language. We define a typed lambda calculus called Proto-Quipper which formalizes a restricted but expressive fragment of Quipper. The type system of Proto-Quipper is based on intuitionistic linear logic and prohibits the duplication of quantum data, in accordance with the no-cloning property of quantum computation. We prove that Proto-Quipper is type-safe in the sense that it enjoys the subject reduction and progress properties.