Two linearities for quantum computing in the lambda calculus

Abstract

We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.

Long journal version of TPNC'17 paper (doi:10.1007/978-3-319-71069-3_22) extended with third author's "Licenciatura"'s thesis

References in corpus (3)

• Quipper: A Scalable Quantum Programming Language
• The Vectorial $\lambda$-Calculus
• A lambda calculus for density matrices with classical and probabilistic controls

Cited by in corpus (15)

• The Vectorial $\lambda$-Calculus
• A New Connective in Natural Deduction, and its Application to Quantum Computing
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• A linear linear lambda-calculus
• A categorical construction for the computational definition of vector spaces
• The Sup Connective in IMALL: A Categorical Semantics
• Automating Equational Proofs in Dirac Notation
• A concrete model for a typed linear algebraic lambda calculus
• A linear proof language for second-order intuitionistic linear logic
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• The Vectorial Lambda Calculus Revisited
• IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• An Algebraic Extension of Intuitionistic Linear Logic: The $L_{!}^S$-Calculus and Its Categorical Model
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus