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.
翻译：在最近的一篇论文中,采用了一种可变性技术来给一个量子 ambda 微积分的语义。 这样一种技术产生了无限数量的有效的打字规则, 而不偏重其中的任何子集。 在本文中, 我们引入了一个有效的打字规则子集, 定义一个表达式的量子微积分。 然后, 我们为它提出一个绝对的语义。 这种语义包括数值分布分布分布的分布- 动作空间类别( 即, 羊羔微积分中数值的线性组合) 和数值分布组的类别之间的连接 。
相关内容
微信扫码咨询专知VIP会员