QUANTUM CONTROL IN THE UNITARY SPHERE: LAMBDA-S1 AND ITS CATEGORICAL MODEL

DÍAZ-CARO, ALEJANDRO; MALHERBE, OCTAVIO

LOGICAL METHODS IN COMPUTER SCIENCE (LMCS)

TECH UNIV BRAUNSCHWEIG

Año: 2022 vol. 18 p. 1 - 36

1860-5974

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.