© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

Mathematical Structures in Computer Science

On quantum lambda calculi: a foundational perspective

Margherita Zorzi

Published Nov 17, 2014• 30 citations

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 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.

DOI: 10.1017/s0960129514000425

Related papers

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We prove subject reduction, confluence and a standardization theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

arXiv:cs/0703152•Mar 30, 2007•0 citations

On a measurement-free quantum lambda calculus with classical control

Ugo Dal Lago, Andrea Masini, Margherita Zorzi

We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

Mathematical Structures in Computer Science•Feb 16, 2009•20 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

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

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

Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits

Alejandro Díaz-Caro, Pablo J. Arrighi, Manuel Gadella +1 more

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.

arXiv:0806.2447•Electronic Notes in Theoretical Computer Science•Feb 1, 2011•15 citations

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.

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.