© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:0806.2447 · Electronic Notes in Theoretical Computer Science

Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits

Alejandro Díaz-Caro, Pablo J. Arrighi, Manuel Gadella, Jonathan Grattage

Published Feb 1, 2011• 15 citations

Abstract

This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML [Grattage, J. and T. Altenkirch, A functional quantum programming language, in: LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258] or Lineal [Arrighi, P. and G. Dowek, A computational definition of the notion of vectorial space, Electronic Notes in Theoretical Computer Science 117 (2005), pp. 249–261; Arrighi, P. and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence, in: B. Buchberger, editor, Term Rewriting and Applications, 19th International Conference, RTA-08, To appear in LNCS (2008), eprint available at arXiv:quant-ph/0612199], which is the subject of further research.

DOI: 10.1016/j.entcs.2011.01.006

Related papers

Linear-algebraic Lambda-calculus: higher-order, encodings and confluence

Pablo J. Arrighi, Gilles Dowek B

We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.

•Dec 22, 2006•30 citations

On quantum lambda calculi: a foundational perspective

Margherita Zorzi

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 calledQ, 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 toQ. On the resulting calculus, calledQ*, 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.

Mathematical Structures in Computer Science•Nov 17, 2014•30 citations

Linear-algebraic lambda-calculus

Pablo J. Arrighi, Gilles Dowek B

With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus, $λ$-calculus, quantum logics.

arXiv:quant-ph/0501150•Jan 25, 2005•7 citations

Confluence Results for a Quantum Lambda Calculus with Measurements

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

A strong confluence result for Q*, a quantum λ-calculus with measurements, is proved. More precisely, confluence is shown to hold both for finite and infinite computations. The technique used in the confluence proof is syntactical but innovative. This makes Q* different from similar quantum lambda calculi, which are either measurement-free or provided with a reduction strategy.

Electronic Notes in Theoretical Computer Science•Feb 1, 2011•16 citations

Confluence Results for a Quantum Lambda Calculus with Measurements

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

A strong confluence result for Q*, a quantum lambda-calculus with measurements, is proved. More precisely, confluence is shown to hold both for finite and infinite computations. The technique used in the confluence proof is syntactical but innovative. This makes Q* different from similar quantum lambda calculi, which are either measurement-free or provided with a reduction strategy.

arXiv:0905.4567•May 28, 2009•0 citations

A Quick Overview on the Quantum Control Approach to the Lambda Calculus

Alejandro Díaz-Caro

In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrighi and Dowek's seminal work until today.

arXiv:2204.03885•Electronic Proceedings in Theoretical Computer Science•Apr 7, 2022•1 citation

This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML [Grattage, J. and T. Altenkirch, A functional quantum programming language, in: LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258] or Lineal [Arrighi, P. and G. Dowek, A computational definition of the notion of vectorial space, Electronic Notes in Theoretical Computer Science 117 (2005), pp. 249–261; Arrighi, P. and G. Dowek, Linear-algebraic lambda-calculus: higher-order, encodings and confluence, in: B. Buchberger, editor, Term Rewriting and Applications, 19th International Conference, RTA-08, To appear in LNCS (2008), eprint available at arXiv:quant-ph/0612199], which is the subject of further research.

We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.

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 calledQ, 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 toQ. On the resulting calculus, calledQ*, 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.

With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus,

λ

-calculus, quantum logics.