Quantum Lambda Calculus

We discuss the design of a typed lambda calculus for quantum computation. After a brief discussion of the role of higher-order functions in quantum information theory, we define the quantum lambda calculus and its operational semantics. Safety invariants, such as the no-cloning property, are enforced by a static type system that is based on intuitionistic linear logic. We also describe a type inference algorithm and a categorical semantics. 4.1 Introduction The lambda calculus, developed in the 1930s by Church and Curry, is a formalism for expressing higher-order functions. In a nutshell, a higher-order function is a function that inputs or outputs a “black box,” which is itself a (possibly higher-order) function. Higher-order functions are a computationally powerful tool. Indeed, the pure untyped lambda calculus has the same computational power as Turing machines (Turing 1937). At the same time, higher-order functions are a useful abstraction for programmers. They form the basis of functional programming languages such as LISP (McCarthy 1960), Scheme (Sussman and Steele 1975), ML (Milner 1978), and Haskell (Hudak et al. 2007). In this chapter, we discuss how to combine higher-order functions with quantum computation. We believe that this is an interesting question for a number of reasons. First, the combination of higher-order functions with quantum phenomena raises the prospect of entangled functions . Certain well-known quantum phenomena can be naturally described in terms of entangled functions, and we give some examples of this in Section 4.2.