A Lambda Calculus for Quantum Computation with Classical Control
A Lambda Calculus for Quantum Computation with Classical Control
Selinger and Valiron use an affine linear lambda calculus to express quantum data, classical control, and safety properties.
Paper information (TLCA 2005, LNCS 3461, pp. 354–368; expanded MSCS version 2006) — Peter Selinger and Benoît Valiron. Conference DOI; journal DOI; arXiv:cs/0404056
Work
The paper extends the simply typed lambda calculus with quantum types and operations, following the “quantum data, classical control” paradigm. It gives a call-by-value operational semantics, uses affine intuitionistic linear logic for the type system, and studies how quantum types and operations compose in a functional program. Its main theoretical results concern safety properties and a type-inference algorithm.
Contributions
- A functional-language design with quantum types and quantum operations.
- A call-by-value operational semantics that makes execution and measurement control explicit.
- An affine-linear type discipline that restricts repeated use of quantum resources while permitting appropriate disposal.
- Safety results and a design for type inference.
Limits
This is a language, type, and semantics result, rather than a complete compiler for a particular hardware target. Affine typing enforces resource-use discipline but does not prove an algorithm's postcondition, measurement probabilities, termination, or behavior under noise. Higher-order quantum computation, dynamic resources, and hardware constraints require richer models.
Connections
The paper is a functional extension of the typed and classical-control direction in QPL and shares linear-resource and categorical motivations with QML. Compared with van Tonder's quantum lambda calculus, it gives a more explicit account of classical control, operational semantics, and type inference. These language designs can be contrasted with the concurrent communication model of Communicating Quantum Processes.
Original paper
Peter Selinger and Benoît Valiron, A Lambda Calculus for Quantum Computation with Classical Control, TLCA 2005, LNCS 3461, 354–368 (2005), expanded in Mathematical Structures in Computer Science 16(3), 527–552 (2006), conference DOI: 10.1007/11417170_26, journal DOI: 10.1017/S0960129506005238. arXiv:cs/0404056