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

Metatheory. No-cloning theorem: qubits can't be copied. Measurement collapses superposition. ZX-calculus complete for stabilizer circuits, Clifford+T. Linear types enforce physical constraints. Denotational semantics in †-categories. Quantum lambda calculi type-safe.

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. Quantum hardware is noisy — idealized model. Measurement semantics subtle (non-determinism vs probabilism). Tool support early stage. Connecting to actual quantum devices requires more. Error correction adds complexity not fully captured. Scalability of verification limited.