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.
A previous attempt to construct a lambda calculus for quantum computation is described by Maymin in @cite_27 . However, his calculus appears to be strictly stronger than the quantum Turing machine @cite_19 . It seems to go beyond quantum mechanics in that it does not appear to have a unitary and reversible operational model, instead relying on a more general class of transformations. It is an open question whether the calculus is physically realizable.
@cite_19 @cite_27
1668464107 1676498955
We show that the lambda-q calculus can efficiently simulate quantum Turing machines by showing how the lambda-q calculus can efficiently simulate a class of quantum cellular automaton that are equivalent to quantum Turing machines. We conclude by noting that the lambda-q calculus may be strictly stronger than quantum computers because NP-complete problems such as satisfiability are efficiently solvable in the lambda-q calculus but there is a widespread doubt that they are efficiently solvable by quantum computers. This paper introduces a formal met alanguage called the lambda-q calculus for the specification of quantum programming languages. This met alanguage is an extension of the lambda calculus, which provides a formal setting for the specification of classical programming languages. As an intermediary step, we introduce a formal met alanguage called the lambda-p calculus for the specification of programming languages that allow true random number generation. We demonstrate how selected randomized algorithms can be programmed directly in the lambda-p calculus. We also demonstrate how satisfiability can be solved in the lambda-q calculus.