Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model

Abstract

In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid typing rules, without giving preference to any subset of those. In this paper, we introduce a valid subset of typing rules, defining an expressive enough quantum calculus. Then, we propose a categorical semantics for it. Such a semantics consists of an adjunction between the category of distributive-action spaces of value distributions (that is, linear combinations of values in the lambda calculus), and the category of sets of value distributions.

References in corpus (6)

• Quipper: A Scalable Quantum Programming Language
• A functional quantum programming language
• Lineal: A linear-algebraic Lambda-calculus
• Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
• Two linearities for quantum computing in the lambda calculus
• A concrete model for a typed linear algebraic lambda calculus

Cited by in corpus (6)

• A New Connective in Natural Deduction, and its Application to Quantum Computing
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• The Vectorial Lambda Calculus Revisited
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation