A quantum let within the lambda calculus
Abstract
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 λρ∘ 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 λρ∘ with a construct let x⊗ n = ρ in t, which binds each xi 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.
Related
- Observation of quantum entanglement in Λ Λ̅ pair production via electron-positron annihilation
- Evaluation-efficient quantum architecture search with ZX-calculus-based topological reuse
- A density calculus for quantum field theory
- Quantum many-body scars with tunable entanglement and Hamiltonian inverse design from ZX-calculus
- Λ(1520) as a probe of resonance-driven deuteron formation at the LHC
BibTeX
@misc{diazcaro2026quantum,
title = {{A quantum let within the lambda calculus}},
author = {Alejandro Díaz-Caro and Tomás Miguez},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2608.29380},
eprint = {2608.29380},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.29380},
}
RIS
TY - UNPB
TI - A quantum let within the lambda calculus
AU - Alejandro Díaz-Caro
AU - Tomás Miguez
PY - 2026
DA - 2026/08/29
PB - arXiv
DO - 10.48550/arxiv.2608.29380
UR - https://arxiv.org/abs/2608.29380
AB - 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 λ_ρ^∘ 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 λ_ρ^∘ with a construct let x^⊗ n = ρ 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.
ER -