PaperlayerView exact revision on arXiv

Source-linked AI summary

A quantum let within the lambda calculus

Alejandro Díaz-Caro, Tomás Miguez

arXiv:2608.29380v1cs.LOquant-ph

TL;DR

The paper addresses the lack of tensor elimination in state-as-term quantum lambda calculi, which prevents independent qubit access and discard. It uses Pauli and spectral decompositions to add a compositional let construct, then formalizes and analyzes the extension. The result restores compositionality and expressiveness while interpreting unused variables exactly as partial traces.

  • Problem

    λ_ρ^◦ embeds quantum states in terms but lacks tensor elimination, so compound states cannot be decomposed for independent qubit access or discard.

  • Method

    The paper combines Pauli and spectral decompositions to add let x^⊗n = ρ in t, supported by rewrite, affine typing, and denotational semantics.

  • Results

    Discard coincides exactly with partial trace, and the extended calculus satisfies Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy.

  • Takeaways & Limitations

    The construct restores compositional programming over states-as-constants and supports quantum teleportation and the three-qubit bit-flip code.

  • Takeaways & Limitations

    The decomposition may contain up to 8^n summands in the worst case, reflecting the existing representation size of n-qubit density matrices.

Abstract

from arXiv · show

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.

1 Introduction

Quantum lambda calculi commonly keep quantum state external, while λ_ρ^◦ embeds states in terms for verification but lacks tensor elimination. This paper introduces a decomposition-based let construct that enables compositional qubit access and physically principled discard.

  • Background: External-register designs manipulate pointers, whereas λ_ρ^◦ represents density matrices directly within terms for reasoning about computation states.The internal-state approach is especially appealing for program verification because equivalences can be established within the calculus.
  • Problem: Without tensor elimination, λ_ρ^◦ cannot decompose compound states or address their individual qubits independently.Operations can still be encoded at matrix level, but this loses the modularity associated with lambda-calculus functions.
  • Problem: The same missing decomposition mechanism prevents λ_ρ^◦ from discarding qubits, making some quantum computations impossible to encode directly.Borgna showed that this limitation affects the calculus’s expressiveness.
  • Contribution: The paper extends λ_ρ^◦ with let x^⊗n = ρ in t, binding each variable to single-qubit density matrices from a decomposition of ρ.The decomposition combines Pauli and spectral decompositions, expressing any n-qubit state as a real linear combination of tensor products of single-qubit states.
  • Results: The extension supplies rewrite, type, and denotational semantics and proves Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy.It also proves that discard coincides with partial trace and illustrates compositional programming through teleportation and the three-qubit bit-flip code.

2 Preliminaries

The preliminaries introduce density matrices, quantum operations, and the base calculus λ_ρ^◦. They explain its affine typing and probabilistic control, while highlighting that composite states have a constructor but no tensor-elimination rule.

  • Quantum computing: Composite systems are formed as tensor products, including entangled states that cannot generally be written as products of single-qubit density matrices.The Bell-state example serves as a running example of this distinction.
  • The calculus: The base calculus represents quantum data with density matrices, uses deterministic rewriting with probabilistic mixtures for measurement, and eliminates measurement results through letcase◦.Terms include unitary application, measurement, tensor formation, probabilistic mixtures, and probabilistic control.
  • Limitation: Although λ_ρ^◦ constructs composite systems through ⊗, it has no corresponding elimination construct for manipulating their individual components.This absence is the central limitation addressed by the paper’s extension.
  • Rewriting: The rewrite system is deterministic and relates syntactic terms to the underlying mathematical model, with convergence written t ↓ r when both reduce to a common term.Measurements reduce through letcase◦ rather than by themselves.
  • Typing: Its affine type system prevents variable duplication, while types distinguish n-qubit states, measurement results, and linear functions.Contexts combined by function application and tensor formation must be disjoint, enforcing linearity.

3 The Compositional Extension

The paper derives a decomposition of every n-qubit density matrix into real linear combinations of tensor products of single-qubit density matrices, then uses it to add compositional tensor elimination to λ◦ρ.

  • 3.1–3.3 Pauli and spectral decompositions: Pauli and spectral decompositions express any n-qubit density matrix as a real linear combination of tensor products of single-qubit density matrices.Each single-qubit factor is a valid density matrix, while potentially negative coefficients encode non-classical correlations.
  • 3.3 Combined Decomposition: Every density matrix ρ ∈ Dn admits the combined decomposition required by the new tensor-elimination construct.The decomposition follows by expanding each Pauli factor into rank-one eigenprojectors and substituting into the Pauli expansion.
  • 3.3 Combined Decomposition: The expanded decomposition may contain up to 8^n summands, reflecting the existing exponential representation of n-qubit states rather than an additional cost introduced by let.For the Bell state, four non-zero Pauli pairs produce 16 expanded terms.
  • 3.4 Extended Grammar, Rewrite System, and Type System: The construct let x^⊗n = ρ in t binds n variables to the single-qubit components arising from ρ’s decomposition.The body is evaluated for each tensor-product component, and results are recombined using the decomposition coefficients.
  • 3.4 Extended Grammar, Rewrite System, and Type System: The calculus generalizes probabilistic mixtures to finite real linear combinations whose coefficients sum to one, allowing negative coefficients from the decomposition.This generalization is required because the combined decomposition is generally not a convex combination.
  • 3.4 Extended Grammar, Rewrite System, and Type System: The type rule assigns each bound variable type 1 and splits contexts to preserve the affine discipline.The source term must have type n, while the body is typed under assumptions for the n single-qubit components.

4 Denotational Semantics

The denotational semantics interprets types as density-matrix spaces and linear functions as completely positive maps, with interpretations defined relative to typing judgements and valuations.

  • 4 Denotational Semantics: Types are interpreted as density-matrix spaces, while function types A ⊸ B are interpreted as completely positive maps from JAK to JBK.Completely positive maps preserve positivity under extension by arbitrary ancillary systems.
  • 4 Denotational Semantics: The interpretation is defined for a typing judgement Γ ⊢ t : A and a valuation assigning each variable a value in its interpreted type.The let interpretation uses the decomposition established in Proposition 3.1.
  • 4 Denotational Semantics: The denotational interpretation is well defined because every density matrix admits the required single-qubit decomposition.

5 Properties

The extended calculus establishes formal metatheoretic properties and shows that affine discard computes the physically correct partial trace. Its semantics also supports observational reasoning: denotationally equal programs cannot be distinguished by ground-type experiments.

  • Discard as Partial Trace: For a Bell state, discarding the first qubit yields the maximally mixed state I/2.The let reduction produces 1/2|0⟩⟨0| + 1/2|1⟩⟨1|, matching the partial-trace calculation.
  • Discard as Partial Trace: Discarding an unused qubit through the affine let construct is equivalent to applying the corresponding partial trace.The result extends to any discarded qubit position by relabeling, and to subsets of qubits because partial traces over disjoint subsystems commute.
  • Metatheoretic Properties: The calculus satisfies Subject Reduction, Progress, and Strong Normalisation for closed well-typed terms.Subject Reduction preserves typing across reduction, Progress guarantees a value or reduction, and Strong Normalisation rules out infinite reduction sequences.
  • Soundness and Adequacy: Soundness makes denotations invariant under reduction, while Adequacy shows that denotational equality implies observational equivalence.The adequacy result means no ground-type context can distinguish two denotationally equal programs.
  • Soundness and Adequacy: The operational and denotational let rules share the same state decomposition, enabling the soundness proof through semantic substitution and linearity.The proof relies on the decomposition used by both semantics and reduction, together with the semantic substitution lemma.

6 Examples

The let construct makes teleportation and bit-flip correction compositional by exposing individual qubits, enabling local corrections, ancilla management, and physically faithful output types.

  • Teleportation: Teleportation separates Alice’s preparation and measurement from Bob’s correction using the let construct.Bob binds all three qubits, uses only q3, and discards Alice’s qubits.
  • Teleportation: The teleportation function has type 1 ⊸1, returning only Bob’s corrected qubit after Alice’s qubits are discarded.Corrections apply to a single-qubit variable rather than a global three-qubit operator.
  • Teleportation: Unused variables q1 and q2 implement Alice’s discard, which computes the partial trace over those qubits.This follows from the affine type system and Proposition 5.1.
  • Bit-Flip Error Correction: The bit-flip example uses let to discard syndrome ancillas, correct only the affected code qubit, and recombine the three code qubits.After syndrome extraction, the first two qubits carry syndrome information and the last three contain the encoded state.
  • Bit-Flip Error Correction: The recovered bit-flip protocol has type 1 ⊸1, unlike the original calculus’s bitflip0 : 1 ⊸5.The new type reflects encoding, protection, and recovery of a single logical qubit.

7 Conclusion

The paper shows that embedded multi-qubit states can be decomposed into single-qubit components and used compositionally in an extended λρ◦ calculus. The calculus receives formal metatheory, physically faithful discard semantics, and protocol examples with types matching their behavior.

  • Conclusion: Pauli and spectral decompositions express any n-qubit density matrix as a real linear combination of tensor products of single-qubit states.This decomposition enables splitting a multi-qubit state embedded inside a term.
  • Conclusion: The extended calculus adds a compositional let construct, rewrite system, affine type system, and completely positive-map denotational semantics.The authors prove Subject Reduction, Progress, Strong Normalisation, Soundness, and Adequacy.
  • Conclusion: Discarding an unused qubit computes exactly the partial trace, in accordance with the no-deleting theorem.Teleportation and bit-flip examples use this semantics to produce types reflecting the physical protocols.
  • Conclusion: The teleportation and bit-flip examples support compositional programming over states-as-constants and the viability of keeping quantum states inside the language.The paper presents this design as suited to reasoning about programs.

B.1 Pauli Decomposition Coefficients (Example 3.1)

The appendix computes Pauli-pair coefficients and expands nonzero terms through spectral decompositions, illustrating how density matrices become weighted sums of single-qubit products. It then applies let reduction and coefficient collection to obtain the partial trace result.

  • Pauli coefficients: The appendix evaluates ⟨β00|(M1 ⊗M2)|β00⟩ for all sixteen Pauli pairs M1, M2 ∈{I, X, Y, Z}.The calculations use the Pauli actions on the Bell state.
  • Spectral expansion: Each nonzero Pauli pair is expanded using the spectral decomposition into tensor products of eigenstate density matrices with signed coefficients.The displayed terms include coefficients such as 1/4 and −1/4 for the eigenstate products.
  • Let reduction: Applying let reduction to let x⊗2 = β00 in x2 drops the vacuous substitution on x1 and retains the second component.The resulting terms are grouped and coefficients of equal density matrices are collected.
  • Let reduction: The collected result equals I/2 = tr1(β00), demonstrating that unused-component elimination yields the partial trace.The appendix identifies the reduced state as the maximally mixed single-qubit state.

C Detailed Proofs

The detailed proofs establish typing and reduction properties for the extended calculus by induction over terms and decomposition cases. They repeatedly use substitution, weakening, strengthening, and affine let typing to preserve types through reductions.

  • Structural lemmas: The appendix assumes standard weakening and strengthening properties for the affine type system.These structural properties support the subsequent substitution and preservation arguments.
  • Structural lemmas: The substitution lemma proves that replacing x with a term of the same type preserves typing.The proof proceeds by induction on the structure of t.
  • Substitution proof: The induction handles variables, abstractions, applications, quantum states, unitary operations, measurements, tensor products, sums, and letcase constructs.Each case applies the induction hypothesis followed by the corresponding typing rule.
  • Substitution proof: For tensor elimination, the proof splits according to whether the substituted variable occurs in the state expression or the body.Affine contexts ensure the variable is absent from the other component, allowing the let typing rule to be reapplied.
  • Let reduction: The let-reduction proof types each decomposed single-qubit state and then applies the substitution lemma repeatedly to the body.The decomposition coefficients preserve trace, completing the typing argument for the weighted result.

C.3 Progress (Theorem 5.2)

The progress theorem classifies every well-typed term: it is a value, can rewrite, or contains a free variable and is stuck. The proof checks this classification construct by construct, including tensor elimination and measurement case analysis.

  • Every well-typed open term is either a value, has a rewrite step, or contains a free variable and does not rewrite.
  • Applications reduce through either operand, or perform beta-reduction when a lambda meets a non-rewriting argument.
  • Unitary operations reduce on concrete density matrices, while measurements and letcase terms follow their respective reduction rules or remain stuck on free variables.
  • Tensor terms reduce in either component, collapse concrete density matrices, or remain stuck when a free variable is present.
  • The tensor-elimination construct either reduces its bound term, propagates a free variable, or remains ready for its main rule when given a density matrix.

C.4 Strong Normalisation (Theorem 5.3)

Strong normalisation is proved using Girard’s reducibility candidates, extended with projection rules used only in the proof. A fundamental substitution lemma then yields strong normalisation for every closed well-typed term under the original reduction relation.

  • Girard’s reducibility-candidates method defines typed sets SN(A), proves forward closure for neutral terms, and establishes closure for each calculus construct.
  • Projection rules are added solely for the strong-normalisation argument; normalisation under the extended relation implies normalisation under the original relation.
  • The closure lemmas cover sums, abstraction, application, unitary operations, measurement, tensor, letcase, and tensor elimination.
  • The fundamental lemma states that valid substitutions map every well-typed term into its corresponding reducibility set.
  • Every closed well-typed term is strongly normalising under the extended relation and therefore also under the original relation.

C.6 Soundness (Theorem 5.4)

Soundness establishes that rewriting preserves denotational semantics. The proof handles contextual reductions, unitary and tensor reductions, measurement branching, and tensor elimination by linearity and semantic substitution.

  • Unitary reduction maps a concrete state to its conjugated state, while tensor reduction interprets a tensor of density matrices as their tensor product.
  • Measurement soundness follows by linearity: branch probabilities multiplied by branch denotations reconstruct the interpretation of the measured state.
  • Every rewrite step preserves the denotation of the term.
  • The tensor-elimination case uses semantic substitution repeatedly to show that decomposition-based evaluation agrees with the interpretation of the original state.
  • Contextual reductions preserve semantics because interpretation is compositional across application, unitary operations, measurement, tensor, sums, letcase, and tensor elimination.

C.7 Compositionality and Adequacy

Compositionality shows that denotationally equal terms remain interchangeable in every context. Combined with normalisation and soundness, this yields adequacy: contextually equivalent closed ground-type terms reduce to the same density matrix.

  • If two closed terms have equal denotations, substituting either into any well-typed context produces equal denotations.
  • Compositionality is preserved through measurement because probabilities and post-measurement states depend only on the denotation supplied by the context.
  • Tensor elimination remains compositional because equal denotations yield identical Pauli coefficients, weights, and eigenprojectors.
  • Every closed well-typed ground-type term reduces to a density matrix.
  • Adequacy identifies the normal forms of contextually related terms, showing that both reduce to the same density matrix.
Loading 2608.29380v1…