Lambda calculi and logics for quantum computing

In questa tesi proponiamo diversi risultati originali riguardo i lambda calcoli e le logiche per le computazioni quantistiche. Il lavoro `e diviso in tre parti. Nella prima parte richiamiamo alcune nozioni fondamentali di algebra lineare, logica e computazione quantistica. La seconda parte volge l’attenzione ai lambda calcoli quantistici. Introdurremo dapprima Q, un lambda calcolo quantistico con controllo classico. Studieremo le sue proprie`a classiche, come la confluenza e la Subject Reduction, proseguendo poi con un’importante propriet`a quantistica, chiamata standardizzazione. In seguito sar`a studiato il potere espressivo di Q, attraverso la provata equivalenza con il formalismo delle famiglie di circuiti quantistici. A partire da Q, sar`a poi definito e studiato il sottolinguaggio SQ, ispirato alla Soft Linear Logic ed intrinsecamente polytime. Sia Q sia SQ non hanno nella sintassi un operatore di misurazione, e quindi un’implicita misurazione viene assunta alla fine delle computazioni. I problemi relativi alla misura sono studiati in un terzo lambda calcolo chiamato Q*, che estende Q con un operatore di misura. Partendo dall’osservazione che un esplicito operatore di misura interrompe l’evoluzione altrimenti deterministica del calcolo, importando un comportamento probabilistico, sono stati definiti dei nuovi strumenti tecnici quali le computazioni probabilistiche e gli stati misti. Proveremo un forte teorema di confluenza, valido anche nell’importante caso delle computazioni infinite. Nella terza parte della tesi studieremo invece due sistemi modali etichettati, chiamati rispettivamente MSQS e MSpQS, che permettono di ragionare qualitativamente sulle computazioni quantistiche. I due sistemi rappresentano un possibile punto di partenza verso un nuovo modello per ragionare qualitativamente sulle trasformazioni computazionali degli stati quantistici, viste come modelli di Kripke. 1

In this thesis we propose several original results about lambda calculi and logics for quantum computing. The work is divided into three parts. The first one is devoted to recall the main notions about linear algebra, logics and quantum computing. The second and main part focalizes on quantum lambda calculi. We start with Q, a quantum lambda calculus with classical control. We study its classical properties, such as confluence and Subject Reduction. We go on with an important quantum property of Q, called standardization, and successively, we study the expressive power of the proposed calculus, by proving the equivalence with the computational model of quantum circuit families. From the calculus Q, subsequently a sublanguage of Q called SQ is defined and studied: SQ is inspired to the Soft Linear Logic and it is a quantum lambda calculus intrinsically poly-time. Since Q and SQ have not an explicit measurement operator in the syntax, an implicit measurement at the end of the computations is assumed. Measurement problems are explicitly studied in a third quantum lambda calculus called Q*, an extension of Q with a measurement operator. Starting from the observation that an explicit measurement operator breaks the deterministic evolution of the computation by importing a probabilistic behavior, new technical instruments, such as the probabilistic computations and the mixed states are defined. We prove a confluence result for the calculus, also for the relevant case of infinite computations. In the last part of the thesis, we propose two labeled modal deduction systems able to describe quantum computations from a qualitative point of view. The two systems, called respectively MSQS and MSpQS, represent a starting point toward a new model to deal (in a qualitative way) with computational quantum structures, seen as Kripke models. 1