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.
Abramsky and Coecke describe a realization of a model of multiplicative linear logic via the quantum processes of entangling and de-entangling by means of typed projectors. They briefly discuss how these processes can be represented as terms of an affine lambda calculus @cite_15 .
@cite_15
1958788572
Abstract Within the Geometry of Interaction (GoI) paradigm, we present a setting that enables qualitative differences between classical and quantum processes to be explored. The key construction is the physical interpretation realization of the traced monoidal categories of finite dimensional vector spaces with tensor product as monoidal structure and of finite sets and relations with Cartesian product as monoidal structure, both of them providing a so-called wave-style GoI. The developments in this paper reveal that envisioning state update due to quantum measurement as a process provides a powerful tool for developing high-level approaches to quantum information processing.