Algebraic and Logical Methods in Quantum Computation
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 ε > 0, we show how to efficiently
find a sequence of Clifford+V or Clifford+T operators whose product approximates
U up to ε 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 ε.
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.