λ演算中的量子let
A quantum let within the lambda calculus
- Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、Inria、LORIA）
- InCo, FIng, Universidad de la República（乌拉圭共和国大学工程与计算机学院）
- DC, FCEN, Universidad de Buenos Aires（布宜诺斯艾利斯大学理学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
针对λ_ρ^∘量子λ演算因缺乏张量消除结构而表达能力受限的问题，本文利用泡利分解与谱分解提出量子let结构扩展该演算，证明其多项理论性质，以符合物理原理的方式恢复了量子比特丢弃能力与表达能力。
AI中文摘要：
自Selinger和Valiron的开创性工作以来，量子λ演算的标准设计一直将量子状态置于程序之外：项操作的是指向外部寄存器的指针。这在很大程度上是因为难以消除张量积。例如，λ_ρ^∘演算将密度矩阵直接嵌入项中，项承载整个计算状态，这一特性对程序验证尤其有吸引力。然而，由于缺乏张量消除结构，它既无法访问复合态的单个量子比特，也无法丢弃它们。Borgna证明，这种无法丢弃量子比特的特性使得该演算的表达能力严格弱于Selinger和Valiron的量子λ演算。\n 在本文中，我们证明了在这种设定下张量消除是可行的。关键观察是，泡利分解结合泡利矩阵的谱分解，使得任意n量子比特密度矩阵都可以表示为单量子比特密度矩阵张量积的实线性组合。利用这一事实，我们用结构let x^(⊗n) = ρ in t扩展了λ_ρ^∘，该结构将每个x_i绑定到由ρ分解得到的单量子比特密度矩阵。\n 我们为扩展后的演算配备了重写系统、类型系统和指称语义，并证明了主题归约、进展性、强规范化、可靠性和恰当性。这一新结构还恢复了缺失的丢弃量子比特的能力，从而恢复了表达能力。此外，我们证明这是通过符合物理原理的方式实现的：根据不可删除定理，t中未使用的变量恰好被解释为被偏迹化。我们通过量子隐形传态和三量子比特比特翻转码说明了由此产生的组合性。
英文摘要：
Since the seminal work of Selinger and Valiron, the standard design for quantum lambda calculi has kept the quantum state outside the program: terms manipulate pointers to an external register. This is largely due to the difficulty of eliminating tensor products. For example, the calculus $λ_ρ^\circ$ embeds density matrices directly within terms, where terms carry the entire computation state, a feature particularly appealing for program verification. However, lacking a tensor elimination construct, it can neither access the individual qubits of a compound state nor discard them. Borgna showed that this inability to discard qubits makes the calculus strictly less expressive than the quantum lambda calculus of Selinger and Valiron. In this paper we show that tensor elimination is possible in this setting. The key observation is that the Pauli decomposition, combined with the spectral decomposition of the Pauli matrices, allows any $n$-qubit density matrix to be expressed as a real linear combination of tensor products of single-qubit density matrices. Exploiting this fact, we extend $λ_ρ^\circ$ with a construct $\mathrm{let}\ x^{\otimes n} = ρ \mathrm{in}\ t$, which binds each $x_i$ to a single-qubit density matrix arising from the decomposition of $ρ$. We equip the extended calculus with a rewrite system, a type system, and a denotational semantics, and prove Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy. The new construct also recovers the missing ability to discard qubits, thereby restoring expressiveness. Moreover, we show that this is achieved in a physically principled way: a variable unused in $t$ is interpreted exactly as being partial-traced out, as dictated by the no-deleting theorem. We illustrate the resulting compositionality through quantum teleportation and the three-qubit bit-flip code.
