Margherita Zorzi

9. December 2015

On quantum lambda calculi: a foundational perspective

We propose an approach to quantum functional calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus called Q, we will explain standard properties and some good quantum properties.

We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator to Q. On the resulting calculus, called Q∗, we will show a confluence both for finite and infinite reduction sequences. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also sketch the essential features of a sub-calculus of Q, called SQ, which captures the three classes of quantum polytime complexity. We will conclude with some considerations about the challenging task of moving from calculi for computable functions to the definition of a paradigmatic quantum programming language.