Basis-Sensitive Quantum Typing via Realisability

TL;DR

The paper addresses basis sensitivity in quantum programming by introducing λ_B, a higher-order quantum λ-calculus where abstractions are decorated with respect to arbitrary bases, including entangled ones. It develops a realizability semantics that tightly links reduction and typing, yielding unitary-type semantics and a principled characterization of unitary operators as values in $\llbracket \sharp \flat_X \Rightarrow \sharp \flat_Y \rrbracket$. A representative core typing system is derived and proven sound, enabling safe reasoning about quantum data and basis changes. The approach is demonstrated through Deutsch's algorithm and quantum teleportation, showing how basis-aware typing captures determinism and deferred-measurement behavior within a uniform framework. Overall, the work provides a robust syntactic and semantic foundation for a basis-aware, type-safe quantum programming language with higher-order control over multiple bases.

Abstract

We present $λ_B$, a quantum-control $λ$-calculus that refines previous basis-sensitive systems by allowing abstractions to be expressed with respect to arbitrary -- possibly entangled -- bases. Each abstraction and let construct is annotated with a basis, and a new basis-dependent substitution governs the decomposition of value distributions. These extensions preserve the expressive power of earlier calculi while enabling finer reasoning about programs under basis changes. A realisability semantics connects the reduction system with the type system, yielding a direct characterisation of unitary operators and ensuring safety by construction. From this semantics we derive a validated family of typing rules, forming the foundation of a type-safe quantum programming language. We illustrate the expressive benefits of $λ_B$ through examples such as Deutsch's algorithm and quantum teleportation, where basis-aware typing captures classical determinism and deferred-measurement behaviour within a uniform framework.

Theorems & Definitions (54)

• definition 1: Qubits
• definition 2: Basis
• theorem 1: Unique decomposition
• corollary 1: Preservation under congruence
• definition 3: Basis-dependent substitution
• lemma 1: Distributivity over linear combinations
• lemma 2: Compatibility with congruence
• theorem 2: Reduction preserves equivalence
• remark 1
• definition 4: Unitary value distribution