A quantum let within the lambda calculus

• URL: http://arxiv.org/abs/2608.29380v1
• Date: Sat, 29 Aug 2026 17:38:37 GMT
• Title: A quantum let within the lambda calculus
• Abstract summary: Since the work of Selinger and Valiron, the standard design for quantum calculi has kept the quantum state outside the program.<n>We show that tensor elimination is possible in this setting.<n>We illustrate the resulting compositionality through quantum teleportation and the three-qubit bit-flip code.
• Score: 45.88028371034407
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 $λ_ρ^\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.

Related papers

• Two-Tower Quantum Matrix Chain Multiplication: Trading Qubits for Depth [73.08853228981701]
  Matrix chain multiplication is a problem in scientific computing, machine learning, and graph analysis.<n>We present emphTwo-Tower Matrix, a quantum subroutine that encodes the product $mathcalW$ of the $K$ matrices into a quantum state in circuit depth.
  arXiv  Detail & Related papers  (2026-07-14T18:42:40Z)
• From Hilbert's Tenth Problem to Quantum Speedup: Explicit Oracles for Bounded Diophantine Systems [0.0]
  We introduce a fully reversible algorithmic framework to solve Diophantine equations over bounded integer domains.<n>By moving beyond abstract black-box assumptions, this explicit architectural synthesis guarantees that the necessary quantum arithmetic acts as a bounded overhead.
  arXiv  Detail & Related papers  (2026-05-13T18:01:01Z)
• Explicit Quantum Circuits for Simulating Linear Differential Equations via Dilation [0.0]
  We present a concrete pipeline that connects the dilation formalism with explicit quantum circuit constructions.<n>On the analytical side, we introduce a discretization of the continuous dilation operator that is tailored for quantum implementation.<n>We prove that the resulting scheme achieves a global error bound of order $O(M-3/2)$, up to exponentially small boundary effects.
  arXiv  Detail & Related papers  (2025-09-20T18:54:49Z)
• BELT: Block Encoding of Linear Transformation on Density Matrices [6.803593864509459]
  We introduce Block.<n>$ of Linear Transformation (BELT), a systematic protocol that simulates arbitrary linear maps.<n>BELT allows the manipulation and extraction of information about $mathcalN(rho)$ through coherent quantum evolution.<n>BELT finds applications in entanglement detection, quantum channel inversion, and pseudo-differential operators.
  arXiv  Detail & Related papers  (2025-08-18T11:54:40Z)
• Learning finitely correlated states: stability of the spectral reconstruction [1.9573380763700716]
  We consider the task of learning a realization of minimal dimension from copies of an unknown state.<n>For finitely correlated translation-invariant states on an infinite chain, a realization of minimal dimension can be reconstructed.
  arXiv  Detail & Related papers  (2023-12-12T18:47:12Z)
• The $\mathfrak S_k$-circular limit of random tensor flattenings [1.2891210250935143]
  We show the convergence toward an operator-valued circular system with amalgamation on permutation group algebras. As an application we describe the law of large random density matrix of bosonic quantum states.
  arXiv  Detail & Related papers  (2023-07-21T08:59:33Z)
• Vectorization of the density matrix and quantum simulation of the von Neumann equation of time-dependent Hamiltonians [65.268245109828]
  We develop a general framework to linearize the von-Neumann equation rendering it in a suitable form for quantum simulations. We show that one of these linearizations of the von-Neumann equation corresponds to the standard case in which the state vector becomes the column stacked elements of the density matrix. A quantum algorithm to simulate the dynamics of the density matrix is proposed.
  arXiv  Detail & Related papers  (2023-06-14T23:08:51Z)
• Quantifying nonstabilizerness of matrix product states [0.0]
  We show that nonstabilizerness, as quantified by the recently introduced Stabilizer R'enyi Entropies (SREs), can be computed efficiently for matrix product states (MPSs) We exploit this observation to revisit the study of ground-state nonstabilizerness in the quantum Ising chain, providing accurate numerical results up to large system sizes.
  arXiv  Detail & Related papers  (2022-07-26T17:50:32Z)
• A lower bound on the space overhead of fault-tolerant quantum computation [51.723084600243716]
  The threshold theorem is a fundamental result in the theory of fault-tolerant quantum computation. We prove an exponential upper bound on the maximal length of fault-tolerant quantum computation with amplitude noise.
  arXiv  Detail & Related papers  (2022-01-31T22:19:49Z)
• Sub-bosonic (deformed) ladder operators [62.997667081978825]
  We present a class of deformed creation and annihilation operators that originates from a rigorous notion of fuzziness. This leads to deformed, sub-bosonic commutation relations inducing a simple algebraic structure with modified eigenenergies and Fock states. In addition, we investigate possible consequences of the introduced formalism in quantum field theories, as for instance, deviations from linearity in the dispersion relation for free quasibosons.
  arXiv  Detail & Related papers  (2020-09-10T20:53:58Z)
• Quantum Gram-Schmidt Processes and Their Application to Efficient State Read-out for Quantum Algorithms [87.04438831673063]
  We present an efficient read-out protocol that yields the classical vector form of the generated state. Our protocol suits the case that the output state lies in the row space of the input matrix. One of our technical tools is an efficient quantum algorithm for performing the Gram-Schmidt orthonormal procedure.
  arXiv  Detail & Related papers  (2020-04-14T11:05:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.