A lambda calculus for density matrices with classical and probabilistic controls

Abstract

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, ${\lambda }_{\rho }$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, ${\lambda }_{\rho }^{\circ }$, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.

This version includes a 11-pages appendix with proofs, and a small fix in the definition of property P(b,A)

References in corpus (6)

• A Lambda Calculus for Quantum Computation
• Quipper: A Scalable Quantum Programming Language
• The Vectorial $\lambda$-Calculus
• Quantum Alternation: Prospects and Problems
• Confluence in Probabilistic Rewriting
• A lambda calculus for density matrices with classical and probabilistic controls

Cited by in corpus (3)

• Two linearities for quantum computing in the lambda calculus
• A lambda calculus for density matrices with classical and probabilistic controls
• A Note on Confluence in Typed Probabilistic Lambda Calculi