一句话：为量子λ演算 Lambda-S1 选取有效类型规则，并用值分布范畴与集合范畴的伴随给出范畴语义。
本文研究量子λ演算的类型规则选择与语义刻画。此前的可实现性技术能为量子λ演算提供语义，但会导出无限多条合法类型规则，且不对任何子集有所偏好。本文从中选取一组有效的类型规则，定义了一个表达能力足够的量子演算 Lambda-S1。随后，作者为其提出范畴语义：在值分布的 distributive-action 空间范畴与值分布集合范畴之间建立伴随。该语义以线性组合表示 λ 演算中的值分布，将类型规则与范畴结构联系起来。摘要未报告实现或实验评估，工作属于量子编程语言的理论基础。
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.
@article{paperbot1654,
title = {Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model},
author = {Alejandro Díaz-Caro and Octavio Malherbe},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:32)2022}
}