A Lambda Calculus for Quantum Computation

Paper information (2004, SIAM Journal on Computing) — André van Tonder. DOI; arXiv

Work

The paper treats the lambda calculus both as a programming language and as an algebra for reasoning about programs, then proposes a quantum lambda calculus. The model combines some benefits of quantum circuits and quantum Turing machines, uses a calculus related to linear logic to handle quantum resources, and supplies both a computational model and an equational proof system. It also argues for a correspondence with the quantum Turing-machine model.

Contributions

• A quantum lambda calculus for expressing quantum algorithms and reasoning about their terms.
• A computational model and equational proof system that make program equivalence a syntactic question.
• A close relationship with quantum Turing machines, together with a linear-calculus perspective that avoids unrestricted copying of quantum resources.

Limits

The calculus and its equations are theoretical models; they do not specify how a hardware backend compiles or executes every term. Noise, measurement cost, device connectivity, and an engineering language interface require separate definitions. A correspondence with a quantum Turing machine is a model-level result, not a performance or correctness proof for every implementation.

Connections

Like Selinger's QPL language, the paper studies quantum data and program semantics, but it centers the lambda calculus, linear resources, and equational reasoning, while QPL describes a language with explicit control structures. It can also be compared with the guarded-command approach in Quantum Programming. Abramsky and Coecke's categorical semantics takes a more abstract route through compositional protocol structure.

Original paper

André van Tonder, A Lambda Calculus for Quantum Computation, SIAM Journal on Computing 33 (2004), 1109–1135, DOI: 10.1137/S0097539703432165. arXiv:quant-ph/0307150