Quantum Computation Logic
Origin. Emerged from quantum computing semantics (1990s-2000s). Selinger's QPL (2004). Abramsky and Coecke's categorical quantum mechanics. ZX-calculus (Coecke & Duncan, 2008). Quantum lambda calculi. Bridges quantum physics and programming language theory.
Models. Logic of quantum programs. Classical computation: bits, Boolean operations. Quantum computation: qubits, unitary operations, measurement. Linear type systems: no cloning, no deleting. Mixed states: probabilistic outcomes from measurement. Categorical semantics: †-categories.
Formalism.
Quantum lambda calculus (QLC): Types: qbit, A ⊗ B, A ⊸ B, !A Terms: standard λ-terms + quantum operations
Key rules:
- No duplication: Γ ⊢ t : qbit doesn't allow using t twice
- Measurement: meas : qbit ⊸ bit
- Unitaries: U : qbit^⊗n ⊸ qbit^⊗n
ZX-calculus: Graphical language for quantum computation.
- Green spiders: Z-rotations
- Red spiders: X-rotations
- Edges: qubits
- Rewrite rules: completeness for Clifford+T
Categorical semantics: †-symmetric monoidal categories:
- Objects: quantum systems
- Morphisms: quantum operations (completely positive maps)
- †: Hermitian adjoint
FHilb: finite-dimensional Hilbert spaces. CPM(C): completely positive maps on C.
Quantum effects: Effect: E with 0 ≤ E ≤ I Partial measurement: generalized Born rule ρ ↦ (tr(Eρ), E^{1/2}ρE^{1/2}/tr(Eρ))
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊗ | U+2297 | Tensor | Parallel composition |
| ⊸ | U+22B8 | Lollipop | Linear function |
| ! | — | Bang | Classical/duplicable |
| † | U+2020 | Dagger | Adjoint |
| qbit | — | Qubit | Quantum bit type |
| meas | — | Measure | Measurement |
| ρ | U+03C1 | Rho | Density matrix |
| U | — | Unitary | Reversible operation |
| ⊢ | U+22A2 | Turnstile / Typing judgment | Γ ⊢ t : A |
| Γ | U+0393 | Gamma | Typing context |
| ≤ | U+2264 | Less-than or equal / Löwner order | Constraint 0 ≤ E ≤ I on effects |
| ↦ | U+21A6 | Maps to | Post-measurement state update |
| × | U+00D7 | Multiplication sign | Matrix dimensions, as in 2^n × 2^n |
| E | — | Effect | Positive operator with 0 ≤ E ≤ I |
| I | — | Identity operator | Upper bound of the effects |
| tr | — | Trace | Born-rule probability |
| FHilb | — | Category of finite-dimensional Hilbert spaces | Standard model |
| CPM | — | Completely positive maps construction | Passage from pure to mixed |
Metatheory. Selinger (2004) showed that the partial density operators under the Löwner order form a CPO on which quantum superoperators are Scott-continuous, which gives loops a denotational semantics as least fixed points and underwrites the predicate-transformer approach. Selinger and Valiron's quantum lambda calculus has an affine intuitionistic-linear type system with subject reduction and progress, and Pagani, Selinger, and Valiron (2014) gave a fully abstract denotational model for it in completely positive maps. On the categorical side, Selinger proved that finite-dimensional Hilbert spaces are complete for dagger compact closed categories: an equation between morphisms of the free dagger compact category holds in FHilb iff it holds in all such categories, so the string-diagram calculus is sound and complete for the finite-dimensional theory. No-cloning is structural rather than physical here — Abramsky showed that a compact closed category carrying a natural uniform copying map collapses, so linearity of the type system is forced by the model, not stipulated. For the graphical fragment, the ZX-calculus is complete for stabilizer quantum mechanics (Backens 2014) and for the Clifford+T fragment (Jeandel, Perdrix, and Vilmart 2018).
Applies to. Quantum programming languages (Quipper, Silq, Q#). Quantum compiler verification. Quantum circuit optimization. Quantum cryptography proofs. Quantum error correction. Formal verification of quantum protocols.
Limitations. Compactness forces finite dimension: infinite-dimensional Hilbert spaces have no duals, so cups and caps do not exist and continuous-variable systems, unbounded observables, and von Neumann algebras fall outside the dagger compact model. Linear types enforce no-cloning but do not track entanglement, so a type system cannot certify that two qubits are separable — deciding separability is NP-hard (Gurvits 2003). Measurement breaks the pure-state semantics: the model must move to density operators and completely positive maps, at which point equational reasoning about branch probabilities is quantitative rather than logical. The completeness results are fragment-by-fragment and qubit-specific; qudit, mixed-state, and continuous-variable calculi each need their own axiomatizations. Denotations live in 2^n × 2^n matrices, so proof obligations are exponential in the number of qubits, and the semantics builds in the Born rule and a particular account of state update rather than deriving them.
© 2026 Lingenic LLC