ALGEBRAIC AND LOGICAL METHODS IN QUANTUM COMPUTATION
ALGEBRAIC AND LOGICAL METHODS IN QUANTUM COMPUTATION
复制标题
量子计算中的代数和逻辑方法
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
N. J. Ross
中科院分区：
文献类型：
--
作者：
N. J. Ross
本论文包含对量子计算理论的贡献。
我们首先定义一种新方法来有效地近似特殊酉算子。具体来说，给定一个特殊的酉 U 和精度 {epsilon} > 0，我们展示了如何有效地找到 Clifford+V 或 Clifford+T 运算符的序列，其乘积在运算符范数中将 U 近似到 {epsilon}。一般情况下，逼近序列的长度是渐近最优的。如果要近似的酉是对角线，那么我们的方法是最佳的：它产生近似 U 到 {epsilon} 的最短序列。
接下来，我们介绍 Quipper 量子编程语言片段的数学形式化。我们定义了一个名为 Proto-Quipper 的类型化 lambda 演算，它形式化了 Quipper 的受限制但富有表现力的片段。 Proto-Quipper 的类型系统基于直觉线性逻辑，并禁止量子数据的复制，符合量子计算的不可克隆特性。我们证明 Proto-Quipper 是类型安全的，因为它具有主题减少和进度属性。
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.