A lambda calculus for quantum computation

The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose...

Full description

Saved in:
Bibliographic Details
Published in:SIAM journal on computing 2004, Vol.33 (5), p.1109-1135
Main Author: VAN TONDER, André
Format: Article
Language:English
Subjects:
Algebra
Algorithmics. Computability. Computer arithmetics
Algorithms
Applied mathematics
Applied sciences
Calculus
Circuits
Classical and quantum physics: mechanics and fields
Computer science
control theory
systems
Exact sciences and technology
General logic
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Physics
Programming languages
Quantum computation
Quantum information
Sciences and techniques of general use
Semantics
Software
Syntax
Theoretical computing
Variables
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of linear logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.
ISSN:0097-5397
1095-7111
DOI:10.1137/S0097539703432165