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

TL;DR

This paper introduces a new quantum lambda calculus with a specific subset of typing rules and provides a categorical semantics for it, advancing the theoretical understanding of quantum programming languages.

Contribution

It defines an expressive quantum calculus with a selected set of typing rules and develops a categorical semantics using an adjunction between relevant categories.

Findings

Categorical semantics for the quantum calculus established

A valid subset of typing rules identified and formalized

Advances the theoretical framework for quantum programming languages

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.