On quantum lambda calculi: a foundational perspective

Abstract

In this paper, we propose an approach to quantum λ-calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus called Q, we will study standard properties such as confluence and subject reduction, 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 propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.