A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
Alejandro Díaz-Caro, Nicolas A. Monzon
TL;DR
This work introduces Lambda-SX, a typed quantum lambda-calculus that explicitly tracks duplicability relative to multiple measurement bases, advancing beyond fixed-basis approaches. By integrating bases such as the computational basis $\mathbb B$ and the Hadamard basis $\mathbb X$ into the type system via a span modality $S(A)$ and a rich subtyping relation, it enables basis-aware reasoning about measurements and linearity. The authors formalise syntax, typing, subtyping, and operational semantics, and prove key results: subject reduction, progress, linear casting, and strong normalization, establishing a coherent foundation for multi-base quantum programming. They also outline extensions to an arbitrary number of bases, including subspace generators $\mathbb Q_{|\\psi\\rangle}$ and overlapping-base subtyping, setting the stage for robust, basis-aware composition of quantum procedures. The work thus provides a proof-of-concept for incorporating multiple measurement bases directly into a quantum lambda-calculus, with potential implications for modular quantum algorithms and future categorical semantics.
Abstract
We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.