Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

TL;DR

This paper introduces an untyped lambda calculus integrating quantum data with classical control, analyzing its syntax, properties, and demonstrating its computational equivalence to certain quantum circuit families.

Contribution

It presents a new quantum lambda calculus with classical control, establishing key properties and proving its computational equivalence to quantum circuits.

Findings

Proves subject reduction, confluence, and standardization.

Shows computational equivalence with quantum circuit families.

Abstract

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.